Модели разработаны командами Project Numina и Kimi и распространяются в формате GGUF. В набор входят варианты Kimina-Prover-Distill и Kimina-Prover-RL размером 0,6B, 1,7B и 8B параметров; базовыми моделями указаны Kimina-Prover-Distill-1.7B, Kimina-Prover-RL-1.7B, Kimina-Prover-RL-0.6B, Kimina-Prover-Distill-0.6B и Kimina-Prover-Distill-8B. Заявленный язык — английский, тип конвейера — генерация текста.

Модели предназначены для строгого математического рассуждения и автоматической генерации формальных доказательств в Lean 4, в частности для задач соревновательного уровня. Distill-варианты дистиллированы из более крупной Kimina-Prover-72B и ориентированы на эффективную работу при меньшем размере. RL-варианты дополнительно дообучены с использованием обучения с подкреплением. В README приведены результаты на MiniF2F-test: до 68,85% Pass@32 для Distill-0.6B, 72,95% для Distill-1.7B, 71,3% для RL-0.6B и 76,63% для RL-1.7B.

Сильными сторонами являются специализация на формальной математике, поддержка Lean 4 и наличие нескольких размеров и уровней GGUF-квантизации, позволяющих выбирать баланс между качеством и требованиями к памяти. Ограничения README не раскрывает архитектуру, размер контекста, точные характеристики варианта 8B, требования к оборудованию и подробности использования; заявленные показатели относятся к конкретным вариантам и метрике Pass@32. Модели распространяются по лицензии Apache-2.0.