Mistral выпустили Leanstral — ИИ-модель для математически идеального кода
В обычной разработке нейросети галлюцинируют, и нам приходится проверять их код руками. Новая модель Leanstral решает эту проблему: она пишет на языке программирования Lean 4, который математически доказывает отсутствие логических багов.
Сразу оговорюсь — это инструмент не для Telegram-ботов или обычных сайтов. Формальная верификация нужна в смарт-контрактах, криптографии, авиации или космонавтике — там, где ошибка стоит миллионы долларов или человеческие жизни, и обычных юнит-тестов недостаточно.
Работает это так: вы не пишете код сами, а только задаёте строгие математические законы (спецификацию). Модель пишет код и пытается доказать его корректность. Бездушный компилятор Lean выступает абсолютным судьей: если есть хоть одна нестыковка, код просто не скомпилируется. Агент Leanstral будет автономно переписывать решение до тех пор, пока компилятор его не примет. Человек в отладке не участвует вообще.
Раньше писать такие сложные математические доказательства умели только гигантские и дорогие модели вроде Claude Opus 4.6. Mistral же сделала узкоспециализированную и лёгкую модель (активны всего 6B параметров). В итоге, чтобы ИИ методом проб и ошибок сам написал и доказал сложный код, на Leanstral вы потратите около $36, а на Claude Opus — $1650 (в 92 раза больше) при сопоставимом качестве успешных решений.
Модель полностью открыта по лицензии Apache 2.0. Потестировать агента можно прямо в браузере через Mistral Vibe или API.
