LeanCopilot: LLM-Taktikvorschläge direkt im Lean-4-Editor
LLMs as Copilots for Theorem Proving in Lean
Auf einen Blick
- Was ist das?
- LeanCopilot bindet Sprachmodelle als Taktik- und Premisesuche in Lean 4 ein, mit CTranslate2 im Kern und vier Modellen von Hugging Face. Der Nutzen liegt bei mittelgroßen Beweisschritten, nicht bei automatischem Beweisen ganzer Sätze.
- Für wen ist es gedacht?
- Sinnvoll ist LeanCopilot für Lean-4-Nutzer, die bereits mit lake und mathlib arbeiten und wiederkehrende Beweisschritte abkürzen wollen, ohne den Editor zu verlassen. Wer einen vollautomatischen Beweiser für offene Forschungsprobleme sucht oder keine Git-LFS-Abhängigkeit in seiner Toolchain dulden will, sollte es nicht einführen.
- Darf ich es kommerziell nutzen?
- Ja. MIT ist eine freizügige Lizenz: Sie dürfen darauf aufbauende Software nutzen, verändern und verkaufen, solange Sie die Urheberrechts- und Lizenzhinweise beibehalten.
- Wird es noch gepflegt?
- Ja. Die letzten Commits kamen vor 1 Tag.
- In welcher Sprache ist es geschrieben?
- Hauptsächlich C++, laut der Sprachstatistik von GitHub.
Die Antworten beruhen auf den GitHub-Daten des Projekts (zuletzt abgeglichen am 15. September 2026) und auf unserer Analyse. Sie sind keine Rechtsberatung.
TIEFGEHENDE OPEN-SOURCE-ANALYSE
Welche Lücke im Beweisalltag das Projekt schließt
In Lean 4 ist der teure Teil selten der eine große Gedanke, sondern die Kette kleiner Schritte dazwischen. Man weiß ungefähr, dass eine Induktion nötig ist, aber nicht, welche der verfügbaren Lemmata den Induktionsschritt schließen. LeanCopilot setzt genau dort an: Es bringt Sprachmodellvorschläge in den Editor, ohne dass der Beweis den Kontext verlässt. Die Zielgruppe sind laut README Nutzer, die proof automation betreiben, also Taktikvorschläge, Premisesuche und die Suche nach mehrschrittigen Beweisen. Das Projekt richtet sich ausdrücklich an Personen, die bereits ein Lean-Projekt mit lake verwalten. Wer Lean nur gelegentlich in einer Web-IDE öffnet, gehört nicht dazu, weil die Einrichtung einen Eintrag in lakefile.lean oder lakefile.toml verlangt und Modelle heruntergeladen werden müssen.
Drei Taktiken und ein Inferenzpfad durch CTranslate2
Der sichtbare Teil sind drei Taktiken. `suggest_tactics` erzeugt Taktikvorschläge, die sich im Editor anklicken und übernehmen lassen, optional mit einem Präfix wie `simp`, um die Vorschläge auf eine Familie einzugrenzen. `search_proof` kombiniert LLM-Taktiken mit aesop zu einer Suche nach mehrschrittigen Beweisen und fügt einen gefundenen Beweis auf Klick ein. `select_premises` liefert eine Liste möglicher Premises. Der technische Kern ist CTranslate2: Der Linker-Eintrag `-lctranslate2` in `moreLinkArgs` verweist auf die Bibliothek, die die eigentliche Inferenz ausführt. Die Modelle kommen als CTranslate2-Konvertierungen von Hugging Face, darunter ct2-leandojo-lean4-tacgen-byt5-small für die Taktikerzeugung, ct2-leandojo-lean4-retriever-byt5-small für die Suche und premise-embeddings-leandojo-lean4-retriever-byt5-small für Premise-Embeddings. Dass die Inferenz als C++-Bibliothek im Lean-Prozess landet, erklärt, warum die Plattformanforderungen so konkret sind: Linux und macOS werden priorisiert, Windows und WSL unterstützt, CUDA und cuDNN sind optional, aber empfohlen, wenn eine NVIDIA-GPU vorhanden ist.
Einrichtung über lakefile und Modelldownload
Die Einrichtung läuft in sechs Schritten, die das README vorgibt. Zuerst kommt in lakefile.lean der Eintrag `moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]` in die Paketdefinition; bei lakefile.toml lautet die Entsprechung `moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]`. Dann folgt die Abhängigkeit, im Lean-Format `require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION"`, in TOML als `[[require]]`-Block mit `rev = "LEAN_COPILOT_VERSION"`. Für stabile Lean-Versionen setzt man dort die Versionsnummer, im Beispiel `v4.33.0`; für instabile Versionen wie `v4.34.0-rc1` steht dort `main`. Auf nativem Windows muss zusätzlich `<path_to_your_project>/.lake/packages/LeanCopilot/.lake/build/lib` in die Path-Variable unter Systemvariablen aufgenommen werden. Danach folgen `lake update LeanCopilot`, `lake exe LeanCopilot/download` und `lake build`. Der Download legt die Modelle unter ~/.cache/lean_copilot/ ab. Wer das umgehen will, lädt die vier genannten Repositories manuell von Hugging Face. Bemerkenswert ist der Hinweis, dass ein Downstream-Paket normalerweise ein vorgebautes Release herunterlädt und CMake sowie einen C++17-Compiler nur dann braucht, wenn für die Plattform kein Release veröffentlicht ist, etwa bei Intel-macOS.
Der Premise-Snapshot ist der wundeste Punkt
`select_premises` greift laut README auf einen festen Snapshot von Lean und mathlib4 zurück, konkret auf den Commit 3ce43c18f614b76e161f911b75a3e1ef641620ff. Das ist eine bewusste Einschränkung: Der Retriever kann nur Premises finden, die in diesem Snapshot enthalten sind. Ein Projekt, das auf einer neueren mathlib-Version arbeitet oder eigene Lemmata definiert, bekommt für diese Namen keine Treffer. Die Taktik bleibt nützlich, aber ihr Suchraum ist nicht das eigene Projekt. Für Taktikvorschläge und Beweissuche gilt diese Grenze nicht in derselben Form, weil dort das Modell aus dem aktuellen Beweisziel generiert. Wer den Retriever auf eigene Premises richten will, muss den Weg über die Model APIs gehen, den das README unter Advanced Usage beschreibt, und ein eigenes Modell einbinden. Das ist kein Konfigurationsschalter, sondern Arbeit.
Versionskopplung und Buildkosten
LeanCopilot verlangt mindestens `lean4:v4.3.0-rc2` und empfiehlt, die Version mit anderen Abhängigkeiten wie mathlib abzustimmen. Die Release-Historie zeigt, wie eng diese Kopplung ist: v4.31.0 erschien am 20. Juni 2026, v4.32.0 und v4.33.0 folgten am 19. August 2026 im Abstand von rund zehn Stunden. Solche Nachschübe deuten auf Anpassungen an neue Lean-Versionen hin, nicht auf Funktionssprünge. Praktisch heißt das: Wer `main` als Revision pinnt, um eine instabile Lean-Version zu nutzen, bindet sich an einen beweglichen Zweig. Wer eine feste Version pinnt, muss bei jedem Lean- oder mathlib-Sprung prüfen, ob ein passendes Release existiert. Dazu kommt der Modell-Cache unter ~/.cache/lean_copilot/, der bei jedem Entwickler und in jeder CI-Umgebung erneut gefüllt werden muss, sofern er nicht im Image liegt. Die Lizenz ist MIT, was die Weitergabe im Quelltext und in Binärform erlaubt, solange Copyright-Hinweis und Lizenztext beiliegen. Das betrifft den Code von LeanCopilot. Die heruntergeladenen Modelle stammen von Hugging Face und haben eigene Bedingungen, die das README nicht aufführt; wer sie in ein Produkt einbettet, muss das dort selbst klären. Rechtsberatung ist das nicht.
Wo aesop allein die bessere Wahl bleibt
Der naheliegende Vergleich ist aesop, das LeanCopilot für `search_proof` ohnehin einbindet. aesop arbeitet mit einer Regelmenge und einem Suchverfahren, das keine Modellgewichte, keinen Modelldownload und keine CTranslate2-Bibliothek braucht. Es ist deterministisch, offline lauffähig und liefert bei Aufgaben, die seine Regeln abdecken, sofort Ergebnisse. LeanCopilot unterscheidet sich im Ansatz: Statt aus einem festen Regelvorrat zu schließen, schlägt ein Sprachmodell Taktiken vor, die aesop dann durchsucht. Das erweitert den Raum möglicher Züge, macht das Ergebnis aber von Modell und Sampling abhängig. Für Beweisziele, die eine bekannte Taktik wie `ring`, `linarith` oder `simp` in einem Schritt lösen, ist aesop allein schneller, weil der Modellaufruf entfällt. Der LLM-Pfad lohnt sich dort, wo der nächste Schritt nicht aus der Regelmenge fällt und ein Vorschlag den Beweis in eine bearbeitbare Richtung schiebt.
Wann das Projekt das falsche Werkzeug ist
LeanCopilot ist kein Beweiser für offene Probleme. `search_proof` sucht mehrschrittige Beweise, aber die Qualität hängt an den vorgeschlagenen Taktiken, und das README macht keine Aussage über Erfolgsquoten. Wer eine Garantie braucht, dass ein Satz bewiesen wird, bekommt sie hier nicht. Ein zweiter Ausschlussgrund ist die Toolchain: Git LFS ist Pflicht, und wer keine externen Binärartefakte im Build haben will, muss den Modelldownload und die CTranslate2-Bibliothek in seine Buildumgebung aufnehmen. Das ist in abgeschotteten Netzen ein echtes Hindernis, weil `lake exe LeanCopilot/download` auf Hugging Face zugreift. Drittens die Plattform: Intel-macOS fällt laut README aus dem Release-Raster und baut aus dem Quelltext, was CMake und einen C++17-Compiler voraussetzt. Wer dort arbeitet, zahlt den vollen Buildpreis.
Für wen sich die Einrichtung rechnet
Der Nutzen zeigt sich bei Nutzern, die täglich in Lean 4 arbeiten und wiederkehrende Beweisschritte abkürzen wollen. Die Taktikvorschläge mit Präfix, etwa `suggest_tactics` mit `simp`, sind ein niedrigschwelliger Einstieg, der die vorhandene Arbeitsweise nicht umbaut. Wer eigene Modelle braucht, findet unter Model APIs und Bring Your Own Model den Weg, Modelle lokal ohne GPU, lokal mit GPU oder in der Cloud zu betreiben; das README nennt diese drei Betriebsarten ausdrücklich. Bevor man das in ein Team rollt, sind drei Dinge zu verifizieren: die Lean-Version gegen die Mindestanforderung, die Verfügbarkeit eines passenden Releases für die eigene Plattform und die Frage, ob der Premise-Snapshot die im Projekt verwendeten Lemmanamen überhaupt enthält. Diese drei Prüfungen entscheiden, ob LeanCopilot hilft oder nur Buildzeit kostet.
Redaktionelles Fazit
Sinnvoll ist LeanCopilot für Lean-4-Nutzer, die bereits mit lake und mathlib arbeiten und wiederkehrende Beweisschritte abkürzen wollen, ohne den Editor zu verlassen. Wer einen vollautomatischen Beweiser für offene Forschungsprobleme sucht oder keine Git-LFS-Abhängigkeit in seiner Toolchain dulden will, sollte es nicht einführen. Vor dem ersten Einsatz ist zu prüfen, ob die eigene Lean-Version mindestens lean4:v4.3.0-rc2 entspricht, ob der Premise-Snapshot zu den verwendeten mathlib-Namen passt und ob `lake exe LeanCopilot/download` die vier Modelle tatsächlich nach ~/.cache/lean_copilot/ schreibt.
Community-Notizen