Обзор

MathCode — терминальный AI-ассистент для написания кода со встроенным движком математической формализации. Задача формулируется на обычном языке, а инструмент автоматически преобразует её в теорему на Lean 4 и пытается построить формальное доказательство. Для этого используются постоянно работающий Lean REPL, переиспользуемые библиотеки теорем и аксиом, агентный режим доказательства и граф знаний в Obsidian.

Демонстрация MathCode

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

Требуется 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

Скрипт setup.sh подготавливает релизную сборку, загружает встроенный рантайм и набор инструментов Lean, а также устанавливает пользовательский лаунчер mathcode. Проверить работу можно так:

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

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

Возможности

Постоянный Lean REPL

Постоянно работающий языковой сервер Lean сокращает время проверки компиляции до ~0,4 секунды после однократного прогрева — вместо обычных ~30 секунд.

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

Каждая доказанная теорема автоматически получает имя, сохраняется и становится импортируемой, так что доказыватель и планировщик могут использовать её повторно.

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

Допущения, сформулированные в диалоге, сохраняются как постоянные декларации Lean — с проверкой компиляции и анализом непротиворечивости.

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

Инструмент ищет проверенные леммы Mathlib через leansearch.net и Loogle, а для исправления ошибок использует структурированные диагностики LSP.

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

Формируется хранилище Obsidian, визуализирующее зависимости между теоремами и леммами в виде графа знаний.

Доказательство в агентном режиме

Каждое доказательство превращается в интерактивную сессию: агент предлагает варианты, читает ошибки компиляции и пересобирает код.

Дерево подцелей

Сложные теоремы разбиваются на независимые подцели, которые доказываются параллельно, а затем собираются воедино.

Мультипланировщик

Несколько планировщиков запускаются параллельно для проработки разных стратегий доказательства, а доказыватель выбирает наиболее удачный подход.

Цитирование

При использовании MathCode в исследованиях рекомендуется ссылаться на проект следующим образом:

@misc{mathcode2026,
  title   = {MathCode: A Frontier Mathematical Coding Agent},
  author  = {Team Math-AI},
  journal = {math-ai-org.github.io},
  year    = {2026},
  month   = {April},
  url     = {https://github.com/math-ai-org/mathcode}
}

Конвейер математической формализации и доказательства построен на основе проекта AUTOLEAN.