Wat doet de “Lean LSP MCP”-server?

Lean LSP MCP is een Model Context Protocol (MCP)-server die AI-assistenten verbindt met Lean Theorem Prover-projecten via het Language Server Protocol (LSP) met behulp van de leanclient. Hiermee kunnen agents en LLM’s interacteren met Lean-projecten, met toegang tot diagnostiek, doelstatussen, terminformatie, hoverdocumentatie en meer. Deze integratie stroomlijnt ontwikkelworkflows voor Lean-gebruikers door een rijk agentgericht pakket aan tools te bieden, waaronder stellingzoekfunctie, code-aanvulling en projectbuild-functionaliteit. De server is bedoeld om de ervaring van ontwikkelaars, onderzoekers en AI-agents die met Lean werken te verbeteren door Lean’s tooling toegankelijk te maken in zowel geautomatiseerde als interactieve contexten.

Lijst van Prompts

Er is geen informatie over prompt-templates gevonden in de repository.

Lijst van Resources

Er is geen informatie over beschikbare MCP-resources gevonden in de repository.

Lijst van Tools

• Lean Theorem Search: Hiermee kunnen agents zoeken naar stellingen via integratie met leansearch.net.
• Code-aanvulling: Biedt suggesties voor code-aanvulling in Lean-bestanden.
• Projectbuild: Maakt projectbuilds mogelijk via het Lean-buildsysteem.
• Diagnostiek: Biedt toegang tot diagnostiek binnen Lean-projecten.
• Doelstatussen & terminformatie: Geeft doelstatus en terminformatie weer voor diepgaande projectanalyse.
• Hoverdocumentatie: Geeft documentatie terug bij hoveren over Lean-code-elementen.

Gebruikstoepassingen van deze MCP-server

• Lean-projectdiagnostiek: Direct toegang krijgen tot en tonen van diagnostiek voor codecorrectheid en debugging binnen Lean-projecten.
• Doelstatusverkenning: Huidige doelstatussen ophalen en weergeven voor bewijsontwikkeling en strategieplanning.
• Stellingzoekfunctie: Zoeken naar relevante stellingen van leansearch.net ter ondersteuning bij bewijsconstructie.
• Code-aanvulling voor Lean: Intelligente code-aanvulling en suggesties bieden voor Lean, waardoor de productiviteit toeneemt.
• Geautomatiseerde projectbuilds: Lean-projectbuilds starten en monitoren als onderdeel van geautomatiseerde workflows of agentische code-review.

Hoe stel je het in

Windsurf

1. Zorg dat uv geïnstalleerd is.
2. Bouw je Lean-project door lake build uit te voeren in de hoofdmap van je project.
3. Zoek het Windsurf-configuratiebestand.
4. Voeg de Lean LSP MCP-server toe met het volgende JSON-fragment:

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

5. Sla op en herstart Windsurf, en controleer vervolgens of de MCP-server draait.

Claude

1. Installeer uv en voer lake build uit in je Lean-project.
2. Open het configuratiebestand van Claude.
3. Voeg de MCP-serverconfiguratie toe:

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

4. Sla op en herstart Claude, en bevestig dat de server beschikbaar is.

Cursor

1. Installeer uv en voer lake build uit.
2. Open het configbestand van Cursor.
3. Voeg de Lean LSP MCP-server toe:

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

4. Sla de wijzigingen op en herstart Cursor.

Cline

1. Zorg dat uv geïnstalleerd is en voer lake build uit.
2. Zoek en bewerk het configuratiebestand van Cline.
3. Voeg de server toe:

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

4. Sla op en herstart Cline.

API-sleutels beveiligen

Als je setup API-sleutels vereist, gebruik dan omgevingsvariabelen om ze veilig te bewaren. Voorbeeld:

{
  "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}"
      }
    }
  }
}

Hoe gebruik je deze MCP in flows

MCP gebruiken in FlowHunt

Om MCP-servers te integreren in je FlowHunt-workflow, voeg je het MCP-component toe aan je flow en verbind je het met je AI-agent:

Klik op het MCP-component om het configuratiepaneel te openen. Voeg in het systeem-MCP-configuratiegedeelte je MCP-servergegevens toe met dit JSON-formaat:

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

Eenmaal geconfigureerd, kan de AI-agent deze MCP nu als tool gebruiken met toegang tot alle functies en mogelijkheden. Vergeet niet “lean-lsp-mcp” te vervangen door de daadwerkelijke naam van je MCP-server en de URL aan te passen naar jouw eigen MCP-server URL.

Overzicht

Op basis van de beschikbare documentatie en code biedt Lean LSP MCP sterke toolingondersteuning voor Lean-projecten, maar ontbreken expliciete prompt-templates of MCP-resourcedefinities. Sampling- en root-ondersteuning worden niet genoemd. Over het algemeen is de server praktisch voor Lean-gebruikers, maar biedt nog niet het volledige spectrum aan geavanceerde MCP-functionaliteiten.

MCP-score