Mistral выпустил Leanstral 1.5, модель для автоматического доказательства теорем
Mistral AI выпустила 30 июня 2026 года Leanstral 1.5, обновленную модель для формальной верификации и автоматического доказательства теорем (automated theorem proving и autoformalization) в экосистеме Lean 4. Модель построена на архитектуре mixture-of-experts с 119 млрд полных параметров и 6,5 млрд активных параметров, поддерживает контекстное окно в 256k токенов.
Это специализированная модель, отличающаяся от универсальных языковых моделей сфокусированностью на задачах формальной математики и логического доказательства. Помимо базовых возможностей (chat completions, function calling), модель поддерживает структурированный вывод, вложения (embeddings), OCR и функцию заполнения пробелов в коде (Fill-In-the-Middle). Модель распространяется на условиях Labs (v1.5) и доступна бесплатно. Одновременно с релизом появился OpenATP, открытый Python-фреймворк для работы с моделью в задачах автоматического доказательства теорем.
Дискуссия в сообществе HackerNews отметила узкую специализацию модели (работает только с Lean 4, а не Coq или другими системами), поставила вопросы о её практическом преимуществе над альтернативами, а также выявила проблемы с доступностью, пользователи сообщили о сложностях с активацией labs-функций и поддержкой при попытке использовать новую модель.
Ключевые факты
- Mistral выпустила специализированную модель Leanstral 1.5 для автоматического доказательства теорем и формализации математических доказательств в Lean 4
- Архитектура mixture-of-experts: 119B полных параметров, 6.5B активных; контекстное окно 256k токенов; модель доступна бесплатно
- Модель поддерживает function calling, структурированный вывод, embeddings, OCR и Fill-In-the-Middle, полный набор современных способностей
- Параллельно выпущен открытый фреймворк OpenATP для интеграции модели в системы автоматического доказательства теорем
- Сообщество обсуждает узкую специализацию модели (только Lean 4), вопросы о конкурентном преимуществе, и проблемы с доступностью labs-функций в платформе Mistral
Почему это важно
Formal proof engineering, инструмент для верификации корректности математических доказательств и компьютерных систем. Автоматизация такой верификации может ускорить как саму разработку, так и обнаружение ошибок в критичных системах (компиляторы, криптография, протоколы). Mistral позиционирует Leanstral как ответ на растущий интерес к формализации математики в Lean 4, экосистеме, где работают исследователи и разработчики, ищущие способы убедиться в корректности сложных алгоритмов и доказательств.
Кому это важно
Модель предназначена для математиков, формальных верификаторов, исследователей в области искусственного интеллекта и компьютерных систем, которые работают с Lean 4. Она может быть полезна в академических кругах (для помощи в доказательстве лемм), в разработке критичных систем, где требуется формальная верификация, и в исследовательских командах, занимающихся автоматизацией математического рассуждения.
Как это применить
Разработчики и исследователи могут интегрировать Leanstral 1.5 через API Mistral или использовать её через новый открытый фреймворк OpenATP. Модель может быть применена для автозаполнения доказательств, поиска ошибок в формальных разработках, или как ассистент при работе с Lean 4-кодом. Поскольку модель бесплатна, её можно экспериментировать без начальных затрат.
Можно ли доверять
Модель обучена специально на задачах формального доказательства, что подразумевает хорошую точность в этой узкой области. Однако её способности проверены пока только в рамках Lean 4-экосистемы; заявления о преимуществах перед конкурентами (например, Claude, GPT-4 с fine-tuning) требуют независимой оценки. Пользователи сообщают о возможности доверять формальным логическим выводам, но мотивы Mistral (конкурентное давление, инвестирования в нишевые модели) стоит учитывать.
Риски и подводные камни
Модель доступна только для экосистемы Lean 4, что ограничивает её применимость для работы с Coq, Isabelle или другими системами формальной верификации. Пользователи сообщали о проблемах с включением labs-функций в платформе Mistral и слабой поддержкой, это может затруднить внедрение для организаций с требованиями к reliability. Кроме того, узкая специализация модели означает, что для других задач (кодирование, аналитика текста) она не будет лучше универсальных моделей и может даже уступить.
«Специализированная модель для формальной верификации и автоматического доказательства теорем, оптимизированная для Lean 4, с 119 млрд полных параметров и 6,5 млрд активных параметров.»
— Документация Mistral (docs.mistral.ai)