MathCode：一个使用Lean 4形式化的数学编码智能体

MathCode — это терминальный ИИ-ассистент для разработки, который формализует и доказывает математические задачи с помощью Lean 4. Вам не нужно писать код на Lean самостоятельно: вы даете ему задачу на простом английском, а он генерирует теорему и пытается провести доказательство, с постоянной REPL и библиотекой переиспользуемых теорем.

Основные возможности

• Постоянная REPL для Lean: После однократной настройки время проверки компиляции снижается до ~0.4 с (с ~30 с).
• Библиотека теорем: Каждая доказанная теорема автоматически получает имя, сохраняется и может быть импортирована для повторного использования.
• Библиотека аксиом: Сохраняет предположения из диалога как постоянные объявления Lean, проверяемые компилятором.
• Интеграция с LSP для Lean: Ищет проверенные леммы Mathlib на leansearch.net и Loogle, использует структурированную диагностику LSP для исправлений.
• Граф теорем в Obsidian: Создает визуальный граф зависимостей теорем и лемм в Obsidian.
• Доказательство в режиме агента: Интерактивные сессии, в которых агент итеративно уточняет кандидатов в доказательства на основе ошибок.
• Дерево подцелей: Разбивает сложные теоремы на независимые подцели, доказывает их параллельно, а затем собирает воедино.
• Множественное планирование: Запускает несколько планировщиков параллельно для различных стратегий доказательства; инструмент выбирает лучший подход.

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

Требуется macOS (arm64) или Linux (x86_64), а также CLI codex для бэкенда по умолчанию.

git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login

Попробуйте так:

mathcode -p "докажите, что квадрат четного числа четен"

Результаты сохраняются в LeanFormalizations/. Веб-интерфейс доступен через ./run webui.

Этот инструмент предназначен для математиков, исследователей и разработчиков, работающих с формальной верификацией или доказательством теорем с помощью ИИ.