- Der erste Open-Source-Code-Agent, der für Lean 4 entwickelt wurde und die Formal-Proof-Automatisierung zum Ziel hat, um den Aufwand menschlicher Verifikation zu reduzieren
- Veröffentlichung der Modellgewichte unter der Apache-2.0-Lizenz, sofort nutzbar über die Mistral Vibe-Umgebung und einen kostenlosen API-Endpunkt
- Nutzt eine sparse Architektur mit 6B aktiven Parametern, um Effizienz und geringere Kosten zu erreichen, und unterstützt MCP-Integrationen wie lean-lsp-mcp
- Erzielte im FLTEval-Benchmark höhere Werte als große Open-Source-Modelle wie Qwen3.5, GLM5 und Kimi-K2.5 und bietet bei über 15-fach geringeren Kosten eine ähnliche Leistung wie Claude Sonnet
- Zeigt mit einem neuen Ansatz, der Formal-Proof-Automatisierung und höhere Code-Zuverlässigkeit verbindet, Potenzial sowohl für Forschungsmathematik als auch für die Entwicklung mission-kritischer Software
Überblick über Leanstral
- Leanstral ist der erste Open-Source-Code-Agent für Lean 4 und arbeitet in einer Umgebung für Proof Assistants
- Lean 4 kann komplexe mathematische Objekte (z. B. perfectoid spaces) und Softwarespezifikationen ausdrücken
- Während bestehende Proof-Systeme sich auf allgemeine Model-Wrapper oder einzelne Probleme konzentrieren, wurde Leanstral dafür trainiert, effizient in realistischen formalen Repositories zu arbeiten
- Verwendet eine sparse Architektur mit 6B aktiven Parametern und kombiniert parallel inference mit den Verifikationsfunktionen von Lean
- Unterstützt MCP-Integration und ist dadurch mit häufig genutzten Protokollen wie lean-lsp-mcp kompatibel
Veröffentlichung und Zugänglichkeit
- Die Modellgewichte werden unter der Apache-2.0-Lizenz veröffentlicht und im Agent-Modus innerhalb von Mistral Vibe bereitgestellt
- Über den kostenlosen API-Endpunkt (
labs-leanstral-2603) für alle zugänglich; Nutzerfeedback soll zur Verbesserung des nächsten Modells genutzt werden
- Zusammen mit dem technischen Bericht und dem Evaluierungstool FLTEval veröffentlicht, um über bestehende mathematikzentrierte Bewertungen hinaus die tatsächliche Leistung im Proof Engineering zu messen
Leistungsbewertung (Evaluation)
- Bewertet anhand der Fähigkeit, auf Pull-Request-Ebene im FLT-Projekt alle Formal Proofs und die Definition neuer mathematischer Konzepte abzuschließen
- Vergleichsmodelle: Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B
Leanstral vs. Open-Source-Modelle
- Leanstral-120B-A6B erreichte 26,3 Punkte (pass@2) und lag damit vor GLM5 (16,6 Punkte) und Kimi-K2.5 (20,1 Punkte)
- Während Qwen3.5 bei vier Ausführungen (pass@4) 25,4 Punkte erzielte, erreichte Leanstral mit halb so vielen Durchläufen einen höheren Wert
- Skalierte bei gleichem Kostenniveau linear auf 29,3 Punkte (pass@4)
Leanstral vs. Claude-Produktfamilie
- 2,6 Punkte vor Sonnet (26,3 vs. 23,7) bei Ausführungskosten von 36 $ vs. 549 $, also mehr als 15-mal günstiger
- Erreichte bei pass@16 31,9 Punkte und lag damit 8 Punkte vor Sonnet
- Das leistungsstärkste Modell Claude Opus 4.6 erzielte 39,6 Punkte, kostete mit 1.650 $ jedoch 92-mal so viel wie Leanstral
- Alle Benchmarks wurden in der Mistral Vibe-Umgebung ohne Modifikationen durchgeführt
| Modell |
Kosten ($) |
Punkte |
| Haiku |
184 |
23.0 |
| Sonnet |
549 |
23.7 |
| Opus |
1,650 |
39.6 |
| Leanstral |
18 |
21.9 |
| Leanstral pass@2 |
36 |
26.3 |
| Leanstral pass@4 |
72 |
29.3 |
| Leanstral pass@8 |
145 |
31.0 |
| Leanstral pass@16 |
290 |
31.9 |
Fallstudien
Umgang mit Lean-Versionsänderungen
- Eingabe einer StackExchange-Frage zu einem Fehler bei Typaliasen in Lean 4.29.0-rc6
- Leanstral reproduzierte die Problemumgebung und diagnostizierte präzise ein Problem mit definitional equality
- Schlug vor, statt
def abbrev zu verwenden, sodass die rw-Taktik wieder korrekt funktionierte
- Erklärte dem Nutzer klar die Ursache des Problems und warum die Lösung funktioniert
Programmbeweis und Transformation
- Konvertierte eine Programmdefinition aus Rocq nach Lean und implementierte sogar benutzerdefinierte Notation
- Bewies am Beispiel, dass der Befehl
plus2 die Variable X um 2 erhöht
- Vervollständigte und bewies das Theorem in Lean allein auf Basis der gegebenen Rocq-Spezifikation
Verwendung
- Mistral-Vibe-Integration: sofort nutzbar mit dem Befehl
/leanstall
- Labs API: kostenlos oder zu niedrigen Kosten zugänglich
- Model-Download: dank Apache-2.0-Lizenz direkt selbst ausführbar
Bedeutung
- Leanstral ist der erste Open-Source-Versuch, Codegenerierung und Formal-Proof-Automatisierung zu verbinden
- Zeigt Anwendungspotenzial in Forschungsmathematik, verifizierbarer Softwareentwicklung und dem Entwurf hochzuverlässiger Systeme
- Wird als neue Infrastruktur für Codeverifikation bewertet, die Kosteneffizienz und Offenheit zugleich bietet
1 Kommentare
Hacker-News-Kommentare
Es ist interessant, dass die Leute nun beginnen, das Muster zu erkennen, bei dem man das gewünschte Verhalten für den Agenten spezifiziert und dann Code schreiben lässt, der dieser Spezifikation entspricht
Egal ob mit TDD, Verifikationswerkzeugen oder anderen Methoden: Mit der Zeit sammeln sich solche Verifikations-Suites als ausführbares Dokumenten-Repository an, das zeigt, „wie es funktionieren soll“
Dieser Ansatz ist viel mächtiger als eine einfache Markdown-Spezifikation, weil er nicht nur Absichten, sondern konkretes Detailverhalten in Code festhält
Je komplexer Software wird, desto weniger trägt eine mündliche Tradition nach dem Muster „Frag Jim“
Feinheiten und Kontext gehen bei einem Wechsel der Auflösung verloren
Ich stimme TDD oder verifikationszentrierter Entwicklung zu, aber das Ziel ist nicht, es unbedingt als Code zu schreiben
Es gibt bereits Millionen Zeilen an Tests, daher ist es realistisch, darauf aufzubauen
Ich frage mich, wobei Lean konkret hilft.
Geht es zum Beispiel darum, mit Lean eine Zustandsmaschine zu beweisen und das dann nach Dart zu übertragen?
Ich kenne Lean nicht gut genug, um einzuschätzen, ob das ein realistischer Ansatz ist
Wie kürzlich auch im Podcast von Jack Clark (Anthropic-Mitgründer) und Ezra Klein erwähnt wurde, gibt es viele Diskussionen darüber, dass Model Alignment relativ ist und Vielfalt wichtig bleibt
Manche halten Mistrals Modell im Vergleich zu anderen Frontier-Modellen für unterlegen, aber es ist wichtig für das Ökosystem, mit unterschiedlichen Alignment-Methoden und Unternehmen zu experimentieren
Der reale Erfolg erinnert mich an Simon Willisons Red Green TDD
Beeindruckend war, wie Leanstral Testcode erzeugte, der die Fehlerumgebung reproduzierte, und dabei Probleme mit definitional equality fand
Das Modell wurde zwar für bestimmte Aufgaben trainiert, leistet aber weniger als Opus
Opus ist sechsmal teurer, scheint das aber wert zu sein
Ich verstehe, warum ein kapitalärmeres europäisches Startup auf so eine Nische zielt, aber es dürfte schwer sein, daraus große Umsätze zu machen
Ein Vergleich mit Modellen wie Codex wäre wohl interessanter
Das Konzept von „vertrauenswürdigem Code“ gefällt mir
Aber die Vergleichsbasis ist verwirrend. Es wird betont, dass es billiger als Haiku ist, aber Haiku ist für diese Aufgabe selbst schon schwach, und Leanstral ist noch schwächer
Wenn Genauigkeit das Ziel ist, verstehe ich nicht, warum „billig, aber nicht gut“ relevant sein soll
Trotzdem ist auch Opus nicht perfekt, also könnte es mit größerem Maßstab bessere Ergebnisse geben
Bei 2 Durchläufen ist es besser als Haiku und Sonnet, und bei 16 Durchläufen kommt es an Opus heran, bleibt dabei aber kosteneffizient
Aus Sicht von jemandem, der Lean nicht kennt, frage ich mich, ob das einen direkten Wert hat
Werden Beweise automatisch an Code in Sprachen wie Go angehängt, oder soll man einfach nur die Vielfalt offener Modelle begrüßen?
Aber am Ende wird diese Lean4-Spezifikation selbst zu einem Software-Artefakt
Dann landet man wieder bei der Frage, wie man überprüft, ob diese Spezifikation korrekt ist — letztlich braucht es also menschliche Prüfung
Ich hatte diese Entwicklung schon vor ein paar Wochen erwartet und freue mich, dass es tatsächlich so gekommen ist
Im LLM-Zeitalter könnten menschliche Lesbarkeit von Code und Beweisbarkeit sowie Token-Effizienz wichtiger werden
Vielleicht erleben wir eine Welt, in der Lean und Rust kombiniert werden und „nur bewiesener Code kompiliert wird“
Eine entsprechende Diskussion habe ich in einem früheren Kommentar zusammengefasst
Es garantiert nur, dass er logisch gültig ist
Vollständig zu verstehen, was ein Beweis beweist, ist fast so schwer wie ein Programm zu verstehen — aber dieser Prozess hat den Vorteil, dass er das Denken vertieft
Es ist erfreulich, dass „Open Source“ nicht nur behauptet wird, sondern die Gewichte tatsächlich unter einer Apache-2.0-Lizenz veröffentlicht wurden
Laut Mistrals offizieller Meldung
erzielt Claude Opus bei Kosten von 1.650 US-Dollar einen Wert von 39,6,
Leanstral pass@8 bei 145 US-Dollar 31,0 und pass@16 bei 290 US-Dollar 31,9,
womit die Kosten-Leistungs-Effizienz ziemlich hoch ist