oOo0oOo/lean-lsp-mcp

해결하는 문제

이 프로젝트는 LLM 에이전트와 Lean 정리 증명기 사이의 다리를 놓습니다. AI 에이전트가 Lean 프로젝트를 프로그래밍 방식으로 상호작용할 수 있게 하여, 코드 분석, 증명 상태 확인, 관련 수학 정리 및 정의 검색이 인간이 증명기와 LLM 사이에서 정보를 수동으로 복사-붙여넣기 할 필요 없이 가능하게 합니다.

작동 방식

leanclient 라이브러리를 사용하여 Language Server Protocol (LSP) 를 통해 Lean과 통신하는 Model Context Protocol (MCP) 서버를 구현합니다. 이 서버는 MCP 호환 에이전트(예: Claude Code, Cursor, VSCode 등)가 호출할 수 있는 일련의 도구를 공개합니다. 구체적으로는:

• Lean 프로젝트 검사: 진단 정보, 목표 상태, 항목 정보, 툴팁 문서에 접근.
• 정리 검색: Loogle, Lean Search, Lean Hammer 등의 외부 검색 도구를 사용하여 기존 증명 및 정의를 검색.
• 코드 실행: Lean 코드 조각 실행. 빠른 REPL 모드를 선택적으로 사용하여 반복 작업을 빠르게 수행 가능.
• 파일 관리: 프로젝트 범위 내 Lean 파일의 읽기 및 쓰기.

대상 사용자

형식 수학, 자동 형식화, 자동 정리 증명을 위한 에이전트 기반 추론 시스템을 개발하는 연구자 및 개발자에게 적합합니다.

주요 특징

• 다양한 도구 세트: 목표 상태 검사, 로컬 소스 스캔(ripgrep를 통해), 여러 리모트/로컬 검색 백엔드 포함.
• LSP 통합: 기존 Lean Language Server를 활용하여 프로젝트에 대한 깊이 있는 분석 가능.
• 유연한 배포: stdio, HTTP 스트리밍, SSE 등 다양한 전송 방식을 지원하며, Docker 컨테이너에서 실행 가능하여 더 나은 격리가 가능.
• 로컬 Loogle 지원: 원격 API의 레이트 제한을 회피하기 위해 로컬에서 Loogle 검색 엔진을 실행할 수 있음.