Was ist Lean LSP MCP?
Lean LSP MCP von Oliver Dressler verbindet einen MCP-Client über Leans Language Server mit dem Beweisassistenten Lean. Der Agent liest Diagnosen und Zielzustände, fragt Typen per Hover ab, probiert mehrere Taktiken auf einmal, prüft, auf welchen Axiomen ein fertiger Beweis beruht, und durchsucht Mathlib lokal oder über LeanSearch, Loogle, Lean Finder und Lean Hammer.
Es steht unter MIT-Lizenz, ist in Python geschrieben, hat rund 548 GitHub-Sterne und 28 Mitwirkende und veröffentlichte am 3. November 2026 v0.33.0. Mehrere Forschungssysteme für automatisierte formale Mathematik, darunter Numina-Lean-Agent und Ax-Prover, nennen es als ihre Schnittstelle zu Lean.
Lean LSP MCP installieren
uvx lean-lsp-mcpLohnt sich Lean LSP MCP?
Lean LSP MCP ist der Standardweg, einen Agenten an Lean 4 zu setzen. Ein Sprachmodell, das Beweise aus dem Gedächtnis rät, erzeugt Text, der richtig aussieht und nicht kompiliert; dieser Server lässt es nach jeder Taktik den aktuellen Zielzustand lesen, den genauen Fehler sehen und es erneut versuchen. Seine 22 Tools decken den Ablauf ab, den eine Mathematikerin im Editor durchläuft: lean_goal und lean_diagnostic_messages zeigen, wo ein Beweis steht, lean_multi_attempt testet mehrere Taktiken an einer Stelle, lean_verify listet die Axiome auf, von denen ein Satz abhängt (alles jenseits der üblichen drei, etwa sorryAx, heißt, der Beweis ist nicht stichhaltig), und lean_build baut das ganze Projekt.
Bei den Suchwerkzeugen sparen Agenten am meisten Zeit, denn das richtige Mathlib-Lemma zu finden ist die halbe formale Beweisarbeit. Die meisten entfernten Dienste, LeanSearch, Loogle, Lean Finder und die Prämissensuche von Lean Hammer, sind jeweils auf 3 Anfragen pro 30 Sekunden begrenzt, und die Dokumentation bittet darum, diese kostenlosen Dienste nicht zu überlasten. Lokales Loogle hebt die Grenze auf, hat aber seinen Preis: Der erste Mathlib-Index erreichte in den Messungen des Entwicklers einen Spitzenwert von etwa 13 GiB Speicher, ein warmer Start braucht etwa 7 GiB.
Der Haken: Es ist ein Forschungswerkzeug im Beta-Stadium, und das README benennt die Risiken direkt. Build- und Ausführungstools führen Lean-Code aus, der Dateien lesen und schreiben kann, und die entfernten Suchwerkzeuge schicken deine Anfragen an Dienste Dritter. Datei-Tools sind auf das Projekt, seine Abhängigkeiten und die Lean-Standardbibliothek beschränkt, und das mitgelieferte Docker-Image schaltet lean_run_code standardmäßig ab. Der HTTP-Transport nutzt standardmäßig 127.0.0.1, und HTTP und SSE akzeptieren ein Bearer-Token über LEAN_LSP_MCP_TOKEN, doch das ist ein einziges gemeinsames Geheimnis, keine Zugriffskontrolle pro Nutzer.
Unser Fazit: Wer mit einem Agenten formale Beweise führt, braucht das als Grundausstattung, nicht als Wahl, bei rund 14.700 PyPI-Downloads in einer Woche und veröffentlichter Forschung, die darauf aufbaut. Die eigentliche Arbeit liegt bei dir: Lass vorher lake build laufen, damit der Client nicht in ein Timeout läuft, ergänze das REPL für mehr Tempo und plane Speicher ein, wenn du Loogle lokal betreibst.
Wo es sich lohnt
Eine Doktorandin, die eine Kombinatorik-Arbeit in Mathlib formalisiert
Routinelemmata schließen, ohne jeden Mathlib-Namen zu suchen
Der Agent liest das Ziel, sucht in Loogle und LeanSearch nach passenden Lemmata, probiert mit lean_multi_attempt mehrere Taktiken und prüft das Ergebnis mit lean_verify. Kostenlos; die Grenze von 3 Anfragen pro 30 Sekunden für die entfernte Suche bestimmt das Tempo.
Ein Verifikationsingenieur in einem Fintech-Start-up
Maschinengeprüfte Beweise zentraler Invarianten aktuell halten, wenn sich der Code ändert
Nach jeder Änderung baut der Agent das Lean-Projekt neu, liest die Diagnosen, repariert kaputte Beweise und bestätigt mit lean_verify, dass sich kein sorry eingeschlichen hat. Betreibe ihn im mitgelieferten Docker-Image mit schreibgeschützt eingebundenem Quellcode.
Ein KI-Labor, das einen Agenten zum Beweisen von Sätzen baut
Dem Agenten eine verlässliche Lean-Schnittstelle geben, ohne sie selbst zu schreiben
Betreibe ihn über Streamable HTTP auf 127.0.0.1 mit Bearer-Token, schalte das REPL für schnelle Snippet-Läufe ein und hoste Loogle oder Lean Hammer selbst, um den öffentlichen Grenzen zu entgehen. Numina-Lean-Agent und Ax-Prover nennen ihn beide als ihre Lean-Schnittstelle.
Bevor du dich festlegst
- Einrichtung
- uv installieren, lake build im Lean-Projekt ausführen, dann uvx lean-lsp-mcp im Client eintragen (Ein-Klick-Buttons für VS Code; claude mcp add lean-lsp uvx lean-lsp-mcp für Claude Code). Optional ripgrep für die lokale Suche und das REPL für schnellere Läufe. Nix wird ebenfalls unterstützt.
- Integrationen
- 22 Tools über Leans Language Server via leanclient; LeanSearch, Loogle, Lean Finder und die Prämissensuche von Lean Hammer; optional das REPL von leanprover-community und lokales Loogle. Funktioniert mit VS Code, Cursor, Claude Code und Mistral Vibe; OpenAI Secure MCP Tunnel für ChatGPT und Codex.
- Daten und Datenschutz
- Läuft lokal. Beweiscode und Ziele gehen an deinen Modellanbieter; Suchanfragen gehen an die entfernten Suchdienste, sofern du sie nicht selbst hostest oder diese Tools abschaltest. Zurückgegebene Pfade werden relativ gemacht, um Verzeichnisse des Rechners zu verbergen.
- Kosten im großen Maßstab
- Kostenlos unter MIT. Intensive Nutzung heißt, Loogle oder Lean Hammer selbst zu hosten, um Grenzen zu umgehen, und genug Speicher für lokales Loogle (etwa 7 GiB warm) und jedes REPL (standardmäßig 16384 MiB Budget).
- Grenzen
- Die meisten entfernten Suchtools sind auf 3 Anfragen pro 30 Sekunden begrenzt. HTTP und SSE bedienen nur ein Projekt. Die Speichergrenze des REPL wird unter Windows nicht durchgesetzt, und lokales Loogle läuft nur unter Linux und macOS.
Was gut ist
- Aktuelle Zielzustände und Diagnosen nach jeder Taktik
- lean_verify markiert Beweise, die auf sorry oder zusätzlichen Axiomen beruhen
- Vier Mathlib-Suchdienste plus lokale Suche
- Läuft über stdio, HTTP oder SSE; Docker-Image enthalten
Was nicht
- Entfernte Suche auf 3 Anfragen pro 30 Sekunden begrenzt
- Lokales Loogle braucht etwa 13 GiB für den Index
- Führt Lean-Code des Projekts aus; nach eigener Angabe Beta
- Clients können ohne vorheriges lake build in ein Timeout laufen
Am besten für
Mathematiker, Ingenieure für formale Methoden und Forschende, die Agenten in Claude Code, Cursor oder VS Code Lean-4-Beweise schreiben und prüfen lassen wollen.
Alternativen zu Lean LSP MCP
Lean LSP MCP: häufige Fragen
- Lohnt sich Lean LSP MCP?
- Wenn ein Agent Lean-Beweise schreiben soll, dann durch diesen Server, denn er zeigt dem Modell genau das, was der Beweisprüfer sieht. Wir bewerten es mit 4.5 von 5.
- Was kostet Lean LSP MCP?
- Kostenlos und Open Source (MIT). Die entfernten Suchdienste, die es aufruft, sind kostenlose Community-Dienste.
- Welche Nachteile hat Lean LSP MCP?
- Entfernte Suche auf 3 Anfragen pro 30 Sekunden begrenzt; Lokales Loogle braucht etwa 13 GiB für den Index; Führt Lean-Code des Projekts aus; nach eigener Angabe Beta; Clients können ohne vorheriges lake build in ein Timeout laufen.
- Für wen eignet sich Lean LSP MCP?
- Mathematiker, Ingenieure für formale Methoden und Forschende, die Agenten in Claude Code, Cursor oder VS Code Lean-4-Beweise schreiben und prüfen lassen wollen.
- Was kostet Lean LSP MCP für ein Team oder im Produktivbetrieb?
- Kostenlos unter MIT. Intensive Nutzung heißt, Loogle oder Lean Hammer selbst zu hosten, um Grenzen zu umgehen, und genug Speicher für lokales Loogle (etwa 7 GiB warm) und jedes REPL (standardmäßig 16384 MiB Budget).
- Ist Lean LSP MCP sicher für Firmendaten?
- Läuft lokal. Beweiscode und Ziele gehen an deinen Modellanbieter; Suchanfragen gehen an die entfernten Suchdienste, sofern du sie nicht selbst hostest oder diese Tools abschaltest. Zurückgegebene Pfade werden relativ gemacht, um Verzeichnisse des Rechners zu verbergen.
- Was sind die besten Alternativen zu Lean LSP MCP?
- Die nächsten Alternativen, die wir getestet haben, sind MCP Solver und Serena.
Antworten geprüft am 7. Nov. 2026.
Du entwickelst Lean LSP MCP? Zeig diese Bewertung auf deiner Website
