MathCode — терминальный AI-агент для формальных доказательств в Lean 4

MathCode — терминальный AI-кодинг-агент со встроенным движком математической формализации. Задайте математическую задачу обычным языком — агент автоматически преобразует её в теорему на Lean 4 и попытается построить формальное доказательство. Пайплайн формализации и доказательства основан на open-source проекте AUTOLEAN, а дефолтный сценарий использования рассчитан на Codex CLI в качестве бэкенда.

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

Как это работает

Базовый сценарий сводится к одной команде:

mathcode -p "prove that the square of an even number is even"

Агент формализует утверждение в Lean 4, планирует стратегию доказательства, ищет подходящие леммы в Mathlib и компилирует доказательство до полного избавления от sorry. Результаты записываются в каталог LeanFormalizations/. Помимо CLI есть браузерный интерфейс: ./run webui поднимает локальный демон и печатает URL аутентификации.

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

Персистентный Lean REPL

При MATHCODE_LEAN_REPL=1 агент поднимает постоянный Lean-сервер: после разового прогрева (~90 секунд на импорт Mathlib) каждая проверка компиляции занимает ~0.4 секунды вместо ~30. Именно это делает интерактивный цикл «докажи — проверь — исправь» практически мгновенным. REPL автоматически импортирует библиотеку теорем и библиотеку аксиом пользователя.

Библиотека теорем

Каждая доказанная теорема автоматически именуется, дописывается в TheoremLib/Stored.lean и становится импортируемой в будущих доказательствах. Планировщик и прувер переиспользуют накопленные результаты вместо повторного вывода.

/theorem-store on     # enable (writes to .env)
/theorem-store off    # disable
/theorem-store sync   # backfill all proved-but-unstored theorems
/theorem-store status # show stored count and vault info

Библиотека аксиом

Команда /axiomatize формализует разговорные допущения («A быстрее, чем B») в декларации Lean, проверяет их компиляцией и на консистентность, хранит в vault и автоматически инжектит в промпты формализации и доказательства. Поддерживается любой домен: математика, физика, химия, нарратив.

/axiomatize "A is faster than B"     # formalize + store
/axiomatize list                     # show all active axioms
/axiomatize check                    # consistency review
/axiomatize remove <name>            # remove a declaration

Интеграция с Lean LSP

При MATHCODE_USE_LSP=1 прувер перед планированием ищет проверенные имена лемм Mathlib через leansearch.net и Loogle, использует структурированные LSP-диагностики (строка, колонка, серьёзность) вместо сырого stderr и извлекает цель доказательства в месте ошибки для точечных исправлений. LSP встроен — отдельная установка не требуется.

Граф теорем в Obsidian

MathCode генерирует Obsidian-vault, визуализирующий зависимости между теоремами как граф знаний. Каждая формализация и доказательство автоматически обновляют vault, а заглушки лемм включают полные определения из Mathlib, полученные через #print.

/obsidian on       # enable + generate from existing formalizations
/obsidian generate # regenerate now

Агентный режим доказательства

При MATHCODE_AGENT_PROVE=1 сессия доказательства превращается в полноценный интерактивный чат. Агент ищет релевантные леммы Mathlib в vault, пишет кандидатов и компилирует их через персистентный REPL, читает ошибки, ищет исправления и перекомпилирует — до 10 итераций за сессию, стримя рассуждения и вызовы инструментов в реальном времени.

Tree-of-Subgoals и мультипланировщик

MATHCODE_TREE_PROVE=1 раскладывает сложную теорему на независимые подцели: декомпозер генерирует скелет с заглушками have ... := by sorry, каждая подцель доказывается отдельно (с кооперативной отменой при неудаче), а доказанные тела сшиваются обратно и проверяются компиляцией. Глубину рекурсии задаёт MATHCODE_MAX_TREE_DEPTH.

MATHCODE_NUM_PLANNERS=3 запускает несколько планировщиков параллельно — каждый предлагает свою стратегию, все найденные леммы сохраняются в vault, а прувер видит все планы и выбирает лучший.

Управление сессиями

В интерактивных сессиях доступна команда /goal с токен-бюджетом: /goal <token-budget> <objective>, с паузой, возобновлением и статусом. Уровень усилий модели настраивается через --effort low|medium|high|max или /effort. Повторяющиеся задачи планируются циклами:

/loop 10m check the deploy
/loop 1h /standup 1

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

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

setup.sh скачивает и верифицирует рантайм-архив (SHA256), восстанавливает бинарники при повреждении, ставит локальный лаунчер в ~/.local/bin/, создаёт .env и каталоги расширений, а также разворачивает bundle-локальный Lean-тулчейн через elan, не трогая системный. Обслуживание установки:

bash setup.sh --status   # check whether the binary/tooling look healthy
bash setup.sh --clean    # remove install artifacts, keep proofs/vault data

Требования: macOS (arm64) или Linux (x86_64), curl, shasum/sha256sum, Codex CLI для дефолтного сценария. Python 3.12+ нужен только для опциональных аналитических инструментов.

Решение типичных проблем

Если команда mathcode не находится сразу после установки, откройте новый шелл (source ~/.zshrc) или используйте bundle-локальный фолбэк ./run до перезагрузки профиля. Ошибка exec format error или Bad CPU type in executable означает, что скачан бинарник не для той платформы — достаточно перезапустить bash setup.sh или вручную взять нужный ассет из GitHub Releases: архив самодостаточен, а setup.sh докачивает файлы из сети только когда они отсутствуют, устарели или не проходят проверку. Клонирование репозитория вообще не обязательно — можно просто распаковать .tar.gz из Releases.

Расширяемость

Из коробки поставляются 4 инструмента анализа: axiom_checker, sorry_analyzer, proof_stats, lib_search. Плагины можно ставить прямо из Git-репозиториев командой /plugin.

Бэкенды

Дефолтный путь — Codex/OpenAI без правок .env. Альтернативы: Anthropic-совместимый бэкенд (ANTHROPIC_API_KEY, ANTHROPIC_MODEL), роут OpenAI-совместимых API через OpenRouter, а также Atlas Cloud. Переменные окружения шелла переопределяют значения из .env.

Ссылки

• Репозиторий: https://github.com/math-ai-org/mathcode
• Базовый проект AUTOLEAN: https://github.com/T3S1AMAX/autolean
• Discord-сообщество: discord.gg/f2AFP9W5