Leanstral 1.5 — открытая специализированная модель для разработки формальных доказательств и autoformalization в Lean 4. Архитектура содержит 119B параметров, но использует около 6,5B активных параметров.
Релиз хорошо показывает новую логику локального стека: вместо одной универсальной модели организация может держать несколько профилей под разные задачи — документы, код, доказательства, OCR и оркестрацию.
Для BunkerAI это кандидат в специализированные инженерные контуры, где важны воспроизводимость, проверяемый результат и возможность работать с закрытым исходным кодом без внешнего API.