модель Leanstral
https://mistral.ai/news/leanstral
Mistral AI представляє Leanstral — відкритий код-агент для мови програмування Lean 4 (яка ще interactive theorem prover). Модель з 6B активних параметрів у розрідженій архітектурі навчається не лише виконувати завдання, а й формально доводити правильність реалізацій. Це робить її потужним інструментом для перевірки коду.

Доступна безкоштовно в Mistral Vibe https://mistral.ai/products/vibe (через API labs-leanstral-2603) та для завантаження на власне обладнання та інтеграції з lean-lsp-mcp. Це перший внесок у майбутнє, де формальна верифікація стане повсякденною, а людський ревью перестане бути вузьким місцем.

Реакція ХН
https://news.ycombinator.com/item?id=47404796
Ентузіасти бачать майбутнє в «executable specs» коли агент пише код + докази, і регресії стають неможливими. Скептики нагадують що докази гарантують лише валідність, а не що ти довів саме те, що хотів і для звичайних проєктів (не математика/критичне ПЗ) це поки «overkill».

#mistral #newllmmodel