Mistral AI bringt Leanstral Open-Source Beweis-Agent für Lean 4 auf den Markt
Zach Anderson 16.03.2026 19:13
Mistral veröffentlicht Leanstral, einen 6B Parameter AI Agent für Lean 4 formale Verifizierung, der größere Modelle bei 1/15 der Kosten unter Apache 2.0 Lizenz übertrifft.
Mistral AI veröffentlichte Leanstral am 16.03.2026—den ersten Open-Source AI Agent, der speziell für Lean 4 formale Verifizierung entwickelt wurde. Das 120B-Parameter-Modell läuft mit nur 6B aktiven Parametern und wird unter Apache 2.0 Lizenzierung ausgeliefert, wodurch Theorembeweis auf Produktionsniveau ohne Unternehmensbudgets zugänglich wird.
Warum ist das für Krypto wichtig? Formale Verifizierung—mathematischer Beweis, dass Code genau das tut, was er behauptet—ist zum Goldstandard für die Absicherung von Smart Contracts und Blockchain-Protokollen geworden. Fehler im DeFi-Code haben Milliarden gekostet. Leanstral könnte die Hürde für Projekte, die verifizierte Sicherheit suchen, drastisch senken.
Leistung vs. Kosten-Kompromisse
Mistral hat Leanstral gegen proprietäre und Open-Source-Konkurrenten mit FLTEval getestet, einer neuen Evaluierungssuite, die echte Beweis-Engineering-Aufgaben aus dem Fermat's Last Theorem Formalisierungsprojekt testet.
Die Zahlen sind beeindruckend. Leanstral erzielte bei pass@2 26,3 Punkte für 36 $ Rechenkosten. Claude Sonnet 4.6 erreichte 23,7 Punkte, verursachte aber eine Rechnung von 549 $—über das 15-fache der Kosten bei schlechterer Leistung. Selbst bei pass@16, wo Leanstral 31,9 Punkte für 290 $ erreicht, kostet es immer noch weniger als ein Fünftel von Claude Opus 4.6's 1.650 $ Preisschild (obwohl Opus bei der Qualität mit 39,6 führt).
Gegenüber Open-Source-Alternativen vergrößert sich die Effizienzlücke weiter. GLM5-744B-A40B und Kimi-K2.5-1T-A32B stagnieren bei etwa 16-20 Punkten, obwohl sie 6-8x mehr aktive Parameter haben. Qwen3.5-397B-A17B benötigt vier Durchgänge, um 25,4 Punkte zu erreichen—Leanstral übertrifft das mit zwei.
Technische Architektur
Leanstral verwendet eine spärliche Mixture-of-Experts-Architektur, die für Beweis-Engineering-Workflows optimiert ist. Das Modell integriert sich über MCP (Model Context Protocol) mit Lean's Language Server Protocol und wurde speziell für maximale Leistung mit lean-lsp-mcp-Tooling trainiert.
Lean 4 selbst wurde im September 2023 stabil veröffentlicht und hat eine schnelle Akzeptanz für die Formalisierung von Mathematik erfahren. Die Mathlib-Bibliothek—eine umfangreiche Sammlung mathematischer Beweise—wurde im selben Jahr erfolgreich auf Lean 4 portiert. Projekte wie der formale Beweis von Fermat's Last Theorem demonstrieren die Fähigkeit der Plattform für ernsthafte mathematische Arbeit.
Praxisanwendungen
Mistral zeigte Leanstral bei der Bearbeitung einer echten Stack Exchange Debugging-Frage zu Breaking Changes in Lean 4.29.0-rc6. Der Agent diagnostizierte ein Problem der definitorischen Gleichheit mit Typ-Aliasen und identifizierte korrekt, dass das Austauschen von def durch abbrev das Taktik-Matching wiederherstellen würde.
Das Modell demonstrierte auch sprachübergreifende Übersetzung, indem es Rocq (ehemals Coq) Definitionen in Lean 4 konvertierte, während es Beweis-Semantik beibehielt und benutzerdefinierte Notation implementierte.
Zugriffsoptionen
Es gibt drei Bereitstellungspfade: direkte Integration in Mistral Vibe (verwenden Sie /leanstall zum Starten), einen kostenlosen API-Endpunkt bei labs-leanstral-2603 für zeitlich begrenzte Feedback-Sammlung oder selbst gehostete Bereitstellung mit den Apache 2.0 Gewichtungen.
Für Blockchain-Projekte ist die Rechnung einfach. Formale Verifizierung erforderte traditionell entweder teure Prüfungsgesellschaften oder tiefes internes Fachwissen. Ein Open-Source-Agent, der Code-Korrektheit für 36-290 $ pro Aufgabe beweisen kann, könnte die Art und Weise verändern, wie Protokolle Sicherheit angehen—vorausgesetzt, die Beweise halten unter Produktionsbedingungen stand.
Bildquelle: Shutterstock- mistral ai
- leanstral
- lean 4
- formale Verifizierung
- open source
