oOo0oOo/lean-lsp-mcp

lean-lsp-mcp – Lean 정리 증명기를 위한 MCP 서버

소개 – Lean 4 언어 서버 위에서 작동하는 Python 기반 Model Context Protocol (MCP) 서버입니다. Lean의 진단 정보, 목표, 호버 정보 및 일련의 검색 도구 (LeanSearch, Loogle, Lean Finder, Lean Hammer)를 tools로 노출하여 LLM 에이전트 (Claude Code, Cursor, Mistral Vibe 등)가 호출할 수 있도록 합니다. 간단히 말해, LLM이 코드 어시스턴트처럼 Lean 프로젝트와 대화할 수 있게 해줍니다.

주요 기능

• Lean 진단 정보, 현재 증명 목표, 용어 정의 및 호버 문서 쿼리.
• 외부 검색 서비스 (LeanSearch, Loogle, Lean Finder, Lean Hammer)를 실행하여 관련 정리 찾기.
• 빠른 코드 실행을 위한 선택적 REPL 기반 lean_run_code 지원.
• 환경 변수 또는 MCP 클라이언트 JSON (VS Code, Cursor, Claude Code, Mistral Vibe)을 통해 구성 가능.
• 세 가지 전송 방식 지원: stdio (기본값), streamable-http, 레거시 sse.
• 안전한 원격 액세스를 위한 OpenAI의 Secure MCP Tunnel 지원.

시작하기

1. uv Python 패키지 관리자를 설치합니다 (또는 Nix 사용).
2. Lean 프로젝트가 빌드 가능한지 확인합니다 (lake build).
3. 선택적 도구를 설치합니다 – 로컬 검색을 위한 ripgrep, 빠른 코드 실행을 위한 repl 패키지, 그리고 선택적으로 로컬 Loogle 바이너리.
4. MCP 호환 IDE (VS Code, Cursor, Claude Code, Mistral Vibe)에 서버 항목을 추가합니다 – 대부분의 예제는 uvx lean-lsp-mcp를 실행하는 한 줄 명령어로 충분합니다.
5. (선택 사항) 환경 변수를 설정하여 로깅 조정, 특정 도구 비활성화, 타임아웃 조정 또는 인증 활성화를 수행합니다.

일반적인 워크플로우

• LLM이 *“MyProof.lean의 현재 목표는 무엇인가요?”*와 같은 요청을 보냅니다.
• MCP 서버가 Lean LSP를 호출하여 목표 상태를 추출하고 간결한 텍스트 블록을 반환합니다.
• 보조 정리가 없는 경우, LLM은 lean_loogle 또는 lean_search를 호출하여 원격 또는 로컬 인덱스를 쿼리하고 일치하는 정리를 반환합니다.
• LLM이 증명 단계를 시도하고 싶다면 lean_run_code (REPL 모드) 또는 lean_multi_attempt를 호출하여 코드 스니펫을 테스트할 수 있습니다.

보안 참고 사항

• 이 서버는 프로젝트 내의 모든 파일을 읽고, 빌드를 실행하며, 검색 도구를 위해 네트워크에 접근할 수 있으므로 신뢰할 수 있는 환경에서 실행하거나 컨테이너화(Docker 이미지 제공)해야 합니다.
• HTTP를 통해 노출할 경우 LEAN_LSP_MCP_TOKEN을 설정하여 베어러 토큰 인증을 수행하거나 OpenAI의 Secure MCP Tunnel을 사용하십시오.

사용자

• 에이전트 기반 정리 증명 시스템을 구축하는 연구자들 (예: Ax-Prover, Numina-Lean-Agent, MerLean, M2F)이 이 도구를 인용합니다.
• Lean Together 2026과 같은 컨퍼런스에서 발표되었습니다.

추가 정보

• PyPI 패키지: lean-lsp-mcp
• 소스 코드 및 문서: https://github.com/oOo0oOo/lean-lsp-mcp
• 전체 도구 목록은 docs/tools.md 참조
• 새로운 도구 추가 방법은 docs/adding-a-tool.md에 문서화되어 있습니다.

라이선스 – MIT (인용을 권장하지만 필수는 아닙니다).