lean-dojo/LeanCopilot

Что это?

Ключевые возможности

• 01Предлагает тактики для текущего состояния доказательства; при необходимости список можно ограничить заданным префиксом.
• 02Ищет доказательства из нескольких тактик, сочетая тактики LLM с aesop.
• 03Находит релевантные предпосылки в Lean и mathlib4 с помощью ретривера LeanDojo.
• 04Запускает встроенные или пользовательские модели локально через CTranslate2 либо удалённо через внешний API.
• 05Предоставляет универсальный интерфейс для инференса LLM, применимый не только к теоремному доказательству.

Сценарии использования

• Получать подсказки по следующей тактике при написании доказательства в Lean.
• Автоматически искать короткие многошаговые доказательства простых целей.
• Находить подходящие леммы в mathlib4, даже если их названия неизвестны.
• Создавать в Lean собственные приложения для автоматизации доказательств с помощью LLM и другие инструменты.

Быстрый старт

1. 1

   Добавьте строку require для LeanCopilot в lakefile

2. 2

   Загрузите пакет LeanCopilot

   lake update LeanCopilot
3. 3

   Скачайте встроенные модели с Hugging Face

   lake exe LeanCopilot/download
4. 4

   Соберите проект

   lake build

Что важно знать

• !Требуется Lean версии не ниже lean4:v4.3.0-rc2.
• !В Linux для сборки цели lean_exe требуется дополнительная настройка компоновщика.
• !search_proof иногда может создавать ошибочные доказательства.
• !select_premises охватывает только фиксированный снимок Lean и mathlib4.

В подборках

Темы

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

Что такое LeanCopilot?

Автоматизация доказательств в Lean с помощью LLM: подсказки по тактикам, поиск доказательств и подбор лемм. Lean Copilot позволяет запускать большие языковые модели прямо внутри теоремного доказателя Lean 4 и автоматизировать отдельные этапы написания формальных доказательств. В пакет входят тактики suggest_tactics, предлагающая следующий шаг доказательства, search_proof, которая сочетает тактики, сгенерированные LLM, и aesop для поиска многошаговых доказательств, а также select_premises, находящая потенциально полезные леммы в Lean и mathlib4.

LeanCopilot можно использовать бесплатно? Какая у него лицензия?

LeanCopilot распространяется с открытым исходным кодом под лицензией MIT. Перед использованием в коммерческих продуктах проверьте условия лицензии.

LeanCopilot всё ещё поддерживается?

Активно поддерживается. Последний коммит в LeanCopilot — 13 окт. 2026 г..

Для чего можно использовать LeanCopilot?

Получать подсказки по следующей тактике при написании доказательства в Lean. Автоматически искать короткие многошаговые доказательства простых целей. Находить подходящие леммы в mathlib4, даже если их названия неизвестны. Создавать в Lean собственные приложения для автоматизации доказательств с помощью LLM и другие инструменты.

Как установить LeanCopilot?

Добавьте строку require для LeanCopilot в lakefile Загрузите пакет LeanCopilot: lake update LeanCopilot Скачайте встроенные модели с Hugging Face: lake exe LeanCopilot/download Соберите проект: lake build

Где скачать LeanCopilot?

Исходный код и инструкции по установке — на GitHub: https://github.com/lean-dojo/LeanCopilot