Математика и рассужденияКод

Kimina-Prover

Модели для формальных доказательств в Lean 4 от Moonshot AI (Kimi) и Numina. Есть маленькие версии от 0.6B, которые запускаются на ноутбуке.

Разработчик: Moonshot AI и Project Numina, Китай, Франция
Первый выпуск: апр 2025
Последний выпуск: авг 2025
Размеры: 0.6B – 72B
Лицензия: Можно в коммерциюKimina-Prover-72B — MIT, остальные — Apache 2.0
Русский язык: Нет
Готовые сборки: GGUF
Запуск: Через свой серверРаботает и без видеокарты
Сферы: Наука, Образование, Разработка ПО

Поставить на свой сервер Hugging Face GitHub

Какие задачи решает

Формальная проверка математических выкладок
Перевод задачи с обычного языка на Lean
Обучение и олимпиадная подготовка

Где применяется

Исследовательские группыОбразованиеРазработка критичного ПО

Требования к железу

НоутбукНоутбук или обычный ПК, до 8 ГБ видеопамяти — младшие версии

подходит

1 видеокартаОдна видеокарта на 16–80 ГБ — средние версии

подходит

КластерСервер с несколькими видеокартами — флагманские версии

нет версий

Версии

авг 2025Kimina-Prover-RL 0.6B и 1.7B
июл 2025Kimina-Prover-72B и Distill 1.7B, 8B
апр 2025Kimina-Prover-Preview-Distill и Autoformalizer

Как запустить

На своём сервереВеса скачиваются с Hugging Face, запуск — через vLLM (нагрузка и API) или llama.cpp (скромное железо). Так модель работает в закрытом контуре, без оплаты за запросы.Hugging Face

Сколько нужно железаПосчитайте видеопамять под нужный размер модели, контекст и число одновременных запросов.Открыть калькулятор железа

Ставлю и настраиваю под ключ: подберу размер модели, разверну на вашем сервере, подключу к вашим системам. Квантование — сжатие модели: она занимает меньше видеопамяти и работает на более скромном железе. Отвечает при этом чуть иначе, поэтому качество проверяют на своих примерах.

Частые вопросы

Можно ли использовать Kimina-Prover в коммерческом проекте?

Да. Лицензия: Kimina-Prover-72B — MIT, остальные — Apache 2.0. Это разрешает коммерческое использование, но перед запуском лицензию всё равно стоит показать юристу.

Какое железо нужно для Kimina-Prover?

Минимум: Ноутбук или обычный ПК, до 8 ГБ видеопамяти — младшие версии. Есть версии, которые работают и без видеокарты, на обычном процессоре. Точный объём видеопамяти под ваш размер модели и контекст можно посчитать в калькуляторе железа.

Поддерживает ли Kimina-Prover русский язык?

Нет. В документации разработчика языки перечислены, русского среди них нет. Для русских задач лучше взять модель из подборки «Открытые ИИ-модели с русским языком».

Где скачать Kimina-Prover и сколько это стоит?

Веса Kimina-Prover лежат в открытом доступе и скачиваются бесплатно. Платить нужно только за железо, на котором модель работает, и за настройку. Ссылки на первоисточник — в конце страницы.

Как внедряю у заказчика

ПодборВыбираю размер модели под задачу и ваше железо, проверяю на ваших примерах.
УстановкаРазворачиваю на вашем сервере или в закрытом контуре, отдаю API.
ДообучениеДообучаю на ваших данных (LoRA) или подключаю базу знаний — что дешевле для задачи.
ВстраиваниеПодключаю к CRM, 1С, боту, сайту или рабочему чату, настраиваю мониторинг.