2026-03-17 11:53:27

Author: danvoronov

eng_2026/03/2026-03-17-09-38.md

@@ -0,0 +1,11 @@
+**Leanstral Model** 
+https://mistral.ai/news/leanstral
+Mistral AI introduces Leanstral — an open-source code agent for the Lean 4 programming language (which is also an interactive theorem prover). This model, with 6B active parameters in a sparse architecture, is trained not only to perform tasks but also to formally **prove** the correctness of implementations. This makes it a powerful tool for code verification.
+
+Available for free in Mistral Vibe https://mistral.ai/products/vibe (via API labs-leanstral-2603) and for download for on-premise hosting and integration with lean-lsp-mcp. This is the first contribution to a future where formal verification becomes commonplace and human review is no longer a bottleneck.
+
+HN Reaction
+https://news.ycombinator.com/item?id=47404796
+Enthusiasts see a future in "executable specs" where an agent writes code + proofs, making regressions impossible. Skeptics remind that proofs only guarantee validity, not that you proved exactly what you intended, and for ordinary projects (non-mathematical/critical software), this is currently "overkill".
+
+#mistral #newllmmodel 

ukr_2026/03/2026-03-17-11-38.md

@@ -0,0 +1,12 @@
+**модель 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