Mistral AI Lansează Leanstral, Agent Open-Source de Demonstrație pentru Lean 4

Zach Anderson 16 mar. 2026 19:13

Mistral lansează Leanstral, un agent AI cu 6B parametri pentru verificarea formală Lean 4, depășind modele mai mari la 1/15 din cost sub licență Apache 2.0.

Mistral AI a lansat Leanstral pe 16 martie 2026—primul agent AI open-source construit special pentru verificarea formală Lean 4. Modelul cu 120B parametri rulează pe doar 6B parametri activi și vine sub licență Apache 2.0, făcând demonstrarea teoremelor de nivel production accesibilă fără bugete enterprise.

De ce contează acest lucru pentru crypto? Verificarea formală—dovada matematică că codul face exact ceea ce pretinde—a devenit standardul de aur pentru securizarea contractelor inteligente și protocoalelor blockchain. Bug-urile din codul DeFi au costat miliarde. Leanstral ar putea reduce dramatic bariera pentru proiectele care caută securitate verificată.

Compromisuri între Performanță și Cost

Mistral a comparat Leanstral cu competitori atât proprietari, cât și open-source folosind FLTEval, o nouă suită de evaluare care testează sarcini reale de inginerie a demonstrațiilor din proiectul de formalizare a Ultimei Teoreme a lui Fermat.

Cifrele sunt impresionante. Leanstral la pass@2 a obținut 26,3 puncte pentru costuri de calcul de 36 USD. Claude Sonnet 4.6 a reușit 23,7 puncte, dar a acumulat o factură de 549 USD—peste de 15 ori costul pentru performanță mai slabă. Chiar și la pass@16, unde Leanstral atinge 31,9 puncte pentru 290 USD, costă încă mai puțin de o cincime din prețul de 1.650 USD al Claude Opus 4.6 (deși Opus conduce la calitate cu 39,6).

Față de alternativele open-source, decalajul de eficiență se lărgește și mai mult. GLM5-744B-A40B și Kimi-K2.5-1T-A32B plafonează în jurul valorii de 16-20 puncte, în ciuda faptului că au de 6-8 ori mai mulți parametri activi. Qwen3.5-397B-A17B are nevoie de patru încercări pentru a atinge 25,4 puncte—Leanstral depășește asta cu două.

Arhitectură Tehnică

Leanstral folosește o arhitectură sparse mixture-of-experts optimizată pentru fluxurile de lucru de inginerie a demonstrațiilor. Modelul se integrează cu protocolul de server de limbaj al Lean prin MCP (Model Context Protocol), antrenat specific pentru performanță maximă cu instrumentele lean-lsp-mcp.

Lean 4 în sine a fost lansat stabil în septembrie 2023 și a văzut o adopție rapidă pentru formalizarea matematicii. Biblioteca Mathlib—o colecție masivă de demonstrații matematice—a fost portată cu succes la Lean 4 în același an. Proiecte precum demonstrația formală a Ultimei Teoreme a lui Fermat arată capacitatea platformei pentru munca matematică serioasă.

Aplicații din Lumea Reală

Mistral a prezentat Leanstral gestionând o întrebare reală de depanare Stack Exchange despre modificări disruptive în Lean 4.29.0-rc6. Agentul a diagnosticat o problemă de egalitate definițională cu aliasurile de tip și a identificat corect că schimbarea def cu abbrev ar restaura potrivirea tacticii.

Modelul a demonstrat, de asemenea, traducere între limbaje, convertind definițiile Rocq (fostul Coq) în Lean 4, păstrând în același timp semantica demonstrației și implementând notație personalizată.

Opțiuni de Acces

Există trei căi de implementare: integrare directă în Mistral Vibe (folosiți /leanstall pentru a începe), un punct final API gratuit la labs-leanstral-2603 pentru colectarea de feedback pe timp limitat sau implementare self-hosted cu ponderile Apache 2.0.

Pentru proiectele blockchain, calculul este simplu. Verificarea formală a necesitat în mod tradițional fie firme de audit scumpe, fie expertiză internă profundă. Un agent open-source care poate dovedi corectitudinea codului la 36-290 USD per sarcină ar putea remodela modul în care protocoalele abordează securitatea—presupunând că demonstrațiile rezistă în condiții de producție.

• mistral ai
• leanstral
• lean 4
• verificare formală
• open source