Mistral AI uruchamia Leanstral – Open-Source'owy Agent Dowodowy dla Lean 4
Zach Anderson 16 mar 2026 19:13
Mistral wydaje Leanstral, agenta AI z 6B parametrami do formalnej weryfikacji Lean 4, pokonując większe modele przy 1/15 kosztu na licencji Apache 2.0.
Mistral AI wypuścił Leanstral 16 marca 2026 roku – pierwszego open-source'owego agenta AI zbudowanego specjalnie do formalnej weryfikacji Lean 4. Model z 120B parametrami działa na zaledwie 6B aktywnych parametrach i jest dostępny na licencji Apache 2.0, czyniąc dowodzenie twierdzeń na poziomie produkcyjnym dostępnym bez budżetów korporacyjnych.
Dlaczego to ma znaczenie dla krypto? Formalna weryfikacja – matematyczny dowód, że kod robi dokładnie to, co deklaruje – stała się złotym standardem zabezpieczania smart kontraktów i protokołów blockchain. Błędy w kodzie DeFi kosztowały miliardy. Leanstral może dramatycznie obniżyć barierę dla projektów poszukujących zweryfikowanego bezpieczeństwa.
Wydajność kontra kompromisy kosztowe
Mistral porównał Leanstral z własnościowymi i open-source'owymi konkurentami używając FLTEval, nowego zestawu ewaluacyjnego testującego rzeczywiste zadania inżynierii dowodów z projektu formalizacji Wielkiego Twierdzenia Fermata.
Liczby są uderzające. Leanstral przy pass@2 zdobył 26,3 punktów za 36 USD kosztów obliczeniowych. Claude Sonnet 4.6 uzyskał 23,7 punktów, ale wygenerował rachunek 549 USD – ponad 15x koszt przy gorszej wydajności. Nawet przy pass@16, gdzie Leanstral osiąga 31,9 punktów za 290 USD, wciąż kosztuje mniej niż jedną piątą ceny Claude Opus 4.6 wynoszącej 1 650 USD (chociaż Opus prowadzi w jakości z 39,6).
W porównaniu z alternatywami open-source, różnica w wydajności pogłębia się. GLM5-744B-A40B i Kimi-K2.5-1T-A32B osiągają plateau około 16-20 punktów pomimo posiadania 6-8x więcej aktywnych parametrów. Qwen3.5-397B-A17B potrzebuje czterech przejść, aby osiągnąć 25,4 punktów – Leanstral pokonuje to dwoma.
Architektura techniczna
Leanstral używa rzadkiej architektury mixture-of-experts zoptymalizowanej dla przepływów pracy inżynierii dowodów. Model integruje się z protokołem serwera języka Lean poprzez MCP (Model Context Protocol), specjalnie wytrenowany dla maksymalnej wydajności z narzędziami lean-lsp-mcp.
Sam Lean 4 uruchomił stabilną wersję we wrześniu 2023 roku i odnotował szybkie przyjęcie do formalizowania matematyki. Biblioteka Mathlib – masywna kolekcja dowodów matematycznych – została pomyślnie przeniesiona do Lean 4 w tym samym roku. Projekty takie jak formalny dowód Wielkiego Twierdzenia Fermata demonstrują możliwości platformy w poważnej pracy matematycznej.
Zastosowania praktyczne
Mistral zaprezentował Leanstral obsługującego autentyczne pytanie debugowania Stack Exchange dotyczące zmian łamiących w Lean 4.29.0-rc6. Agent zdiagnozował problem równości definicyjnej z aliasami typów i poprawnie zidentyfikował, że zamiana def na abbrev przywróci dopasowanie taktyk.
Model również zademonstrował tłumaczenie międzyjęzykowe, konwertując definicje Rocq (dawniej Coq) do Lean 4, zachowując semantykę dowodu i implementując niestandardową notację.
Opcje dostępu
Istnieją trzy ścieżki wdrożenia: bezpośrednia integracja w Mistral Vibe (użyj /leanstall aby rozpocząć), darmowy endpoint API pod labs-leanstral-2603 do zbierania opinii przez ograniczony czas, lub samodzielne wdrożenie z wagami Apache 2.0.
Dla projektów blockchain rachunek jest prosty. Formalna weryfikacja tradycyjnie wymagała albo drogich firm audytorskich, albo głębokiej wewnętrznej ekspertyzy. Open-source'owy agent, który może udowodnić poprawność kodu za 36-290 USD za zadanie, może przekształcić sposób, w jaki protokoły podchodzą do bezpieczeństwa – zakładając, że dowody utrzymają się w warunkach produkcyjnych.
Źródło obrazu: Shutterstock- mistral ai
- leanstral
- lean 4
- formalna weryfikacja
- open source
