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

Goedel-Prover

Открытые модели для формальных доказательств в Lean 4 из Принстона. Свежая Goedel-Code-Prover доказывает корректность программ.

Разработчик
Принстонский университет, США
Первый выпуск
янв 2025
Последний выпуск
мар 2026
Размеры
7B – 32B
Лицензия
Можно в коммерциюПервая версия — MIT, V2 и Code-Prover — Apache 2.0
Русский язык
Не заявлен
Готовые сборки
GGUF
Запуск
Через свой серверНужна видеокарта
Сферы
Наука, Разработка ПО, Образование
Поставить на свой сервер Hugging Face GitHub

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

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

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

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

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

НоутбукНоутбук или обычный ПК, до 8 ГБ видеопамяти — младшие версии
подходит
1 видеокартаОдна видеокарта на 16–80 ГБ — средние версии
подходит
КластерСервер с несколькими видеокартами — флагманские версии
нет версий

Версии

  1. Goedel-Code-Prover-8B
  2. Goedel-Prover-V2 8B и 32B
  3. Goedel-Prover-DPO
  4. Goedel-Prover-SFT

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

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

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

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

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

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

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

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

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

В карточке модели языки не перечислены, поэтому поддержку русского обещать нельзя — её нужно проверять на ваших примерах.

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

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

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

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

Похожие модели

Математика и рассужденияDeepSeek-ProverDeepSeek · КитайКоммерция с условиями

Модели DeepSeek для формальных доказательств на языке Lean 4: доказательство проверяет программа, а не человек. Узкий инструмент для математиков и инженеров.

ПодробнееМатематика и рассужденияKimina-ProverMoonshot AI и Project Numina · Китай, ФранцияМожно в коммерцию

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

Подробнее

Источник: huggingface.co/Goedel-LM/Goedel-Code-Prover-8B. Данные сверены с карточкой модели 22.09.2026. Лицензию перед коммерческим запуском проверьте с юристом.