Lean LSP MCP 서버

“Lean LSP MCP” 서버는 무엇을 하나요?

Lean LSP MCP는 모델 컨텍스트 프로토콜(MCP) 서버로, leanclient를 활용해 AI 어시스턴트와 Lean Theorem Prover 프로젝트를 Language Server Protocol(LSP)로 연결합니다. 이 서버는 에이전트와 LLM이 Lean 프로젝트와 상호작용할 수 있도록 하여, 진단, 목표 상태, 용어 정보, 호버 문서 등 다양한 정보에 접근할 수 있게 합니다. 통합을 통해 Lean 사용자는 정리 검색, 코드 자동완성, 프로젝트 빌드 등 에이전트 중심의 풍부한 도구를 활용할 수 있어 개발 워크플로우가 한층 간소화됩니다. 개발자, 연구자, AI 에이전트가 Lean을 보다 쉽게 자동화·대화형으로 사용할 수 있도록 Lean의 다양한 도구 접근성을 제공합니다.

프롬프트 목록

저장소에서 프롬프트 템플릿에 대한 정보를 찾을 수 없습니다.

리소스 목록

저장소에서 노출된 MCP 리소스에 대한 정보를 찾을 수 없습니다.

도구 목록

• Lean 정리 검색: leansearch.net 통합을 통해 에이전트가 정리를 검색할 수 있습니다.
• 코드 자동완성: Lean 파일에 대한 코드 자동완성 제안을 제공합니다.
• 프로젝트 빌드: Lean 빌드 시스템을 통한 프로젝트 빌드를 지원합니다.
• 진단: Lean 프로젝트 내 진단 정보를 제공합니다.
• 목표 상태 & 용어 정보: 프로젝트 분석을 위해 목표 상태와 용어 정보를 노출합니다.
• 호버 문서: Lean 코드 요소 위에 마우스를 올릴 때 문서를 반환합니다.

이 MCP 서버의 활용 사례

• Lean 프로젝트 진단: Lean 프로젝트 내 코드의 정확성 및 디버깅을 위한 진단 정보를 즉시 확인할 수 있습니다.
• 목표 상태 탐색: 증명 개발 및 전략 수립을 위한 현재 목표 상태를 불러와 표시합니다.
• 정리 검색: leansearch.net에서 관련 정리를 검색하여 증명 작성에 도움을 줍니다.
• Lean 코드 자동완성: Lean을 위한 지능적인 코드 자동완성 및 추천으로 생산성을 높입니다.
• 자동화된 프로젝트 빌드: 자동화된 워크플로우나 에이전트 기반 코드 리뷰에 Lean 프로젝트 빌드를 트리거하고 모니터링합니다.

설정 방법

Windsurf

1. uv가 설치되어 있는지 확인하세요.
2. 프로젝트 루트에서 lake build를 실행하여 Lean 프로젝트를 빌드합니다.
3. Windsurf 설정 파일을 찾으세요.
4. 아래 JSON 스니펫을 사용하여 Lean LSP MCP 서버를 추가합니다:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

5. 저장 후 Windsurf를 재시작하고 MCP 서버가 실행 중인지 확인하세요.

Claude

1. uv를 설치하고 Lean 프로젝트에서 lake build를 실행하세요.
2. Claude의 설정 파일을 여세요.
3. MCP 서버 설정을 삽입합니다:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. 저장 후 Claude를 재시작하고 서버가 사용 가능한지 확인하세요.

Cursor

1. uv를 설치하고 lake build를 실행하세요.
2. Cursor의 설정 파일을 여세요.
3. Lean LSP MCP 서버를 추가합니다:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. 변경사항을 저장하고 Cursor를 재시작하세요.

Cline

1. uv가 설치되어 있는지 확인하고 lake build를 실행하세요.
2. Cline 설정 파일을 찾아 수정하세요.
3. 서버를 추가합니다:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. 저장 후 Cline을 재시작하세요.

API 키 보안 설정

설정에 API 키가 필요하다면, 환경 변수를 사용하여 안전하게 관리하세요. 예시:

{
  "mcpServers": {
    "lean-lsp-mcp": {
      "command": "lean-lsp-mcp",
      "args": [],
      "env": {
        "API_KEY": "${env:LEAN_LSP_MCP_API_KEY}"
      },
      "inputs": {
        "api_key": "${env:LEAN_LSP_MCP_API_KEY}"
      }
    }
  }
}

플로우에서 MCP를 사용하는 방법

FlowHunt에서 MCP 사용하기

FlowHunt 워크플로우에 MCP 서버를 통합하려면 플로우에 MCP 컴포넌트를 추가한 뒤 AI 에이전트와 연결하세요:

MCP 컴포넌트를 클릭해 설정 패널을 엽니다. 시스템 MCP 설정 섹션에 아래와 같은 JSON 형식으로 MCP 서버 정보를 입력하세요:

{
  "lean-lsp-mcp": {
    "transport": "streamable_http",
    "url": "https://yourmcpserver.example/pathtothemcp/url"
  }
}

설정이 완료되면, AI 에이전트가 이 MCP의 모든 기능과 도구를 사용할 수 있게 됩니다. “lean-lsp-mcp"는 실제 MCP 서버 이름으로, URL도 본인 MCP 서버 주소로 변경해야 합니다.

개요

공식 문서와 코드를 바탕으로 Lean LSP MCP는 Lean 프로젝트에 대한 강력한 도구 지원을 제공하지만, 명시적인 프롬프트 템플릿이나 MCP 리소스 정의는 없습니다. 샘플링 및 roots 지원도 언급되지 않았습니다. 전반적으로 Lean 사용자에게 실용적이지만, 아직 고급 MCP 기능 전체를 노출하지는 않습니다.

MCP 점수