ИИтог

MathCode: ИИ-агент доказывает теоремы в Lean 4 и запоминает решения

инструментыРедакция ИИтогHacker News🔥62Рейтинг ИИтог62Влияние55Новизна65Релевантность100Неожиданность50Участники20Достоверность85

MathCode, терминальный ИИ-агент для программирования со встроенным движком математической формализации. Пользователь описывает задачу на обычном языке, а MathCode автоматически переводит её в теорему на языке Lean 4 и пытается построить формальное доказательство.

В основе, постоянный (persistent) языковой сервер Lean: после однократного «прогрева» он проверяет компиляцию доказательства примерно за 0,4 секунды вместо примерно 30 секунд без такого сервера. Каждая доказанная теорема автоматически именуется, сохраняется и становится доступной для повторного использования планировщиком и модулем доказательства. Разговорные предположения тоже можно сохранять как постоянные Lean-декларации, которые проверяются компилятором на непротиворечивость.

При поиске нужных утверждений MathCode обращается к сервисам leansearch.net и Loogle за уже проверенными леммами библиотеки Mathlib, а для исправления ошибок использует структурированную диагностику LSP. Сложные теоремы система разбивает на независимые подзадачи, доказывает их параллельно и затем «сшивает» результат; отдельно MathCode параллельно запускает несколько планировщиков с разными стратегиями доказательства, а модуль доказательства выбирает лучший из полученных вариантов. Каждое доказательство оформлено как интерактивная сессия: агент пишет кандидатов, читает сообщения об ошибках компилятора и пересобирает код. Дополнительно инструмент генерирует хранилище Obsidian, которое визуализирует граф зависимостей между теоремами и леммами в виде базы знаний.

Для запуска нужен macOS (arm64) или Linux (x86_64) и CLI Codex как бэкенд по умолчанию; установка, клонированием репозитория с GitHub и запуском скрипта setup.sh, после чего команда mathcode -p "..." формализует и пытается доказать заданную задачу, а результаты сохраняются в папку LeanFormalizations. Есть и веб-интерфейс, запускаемый отдельной командой. Конвейер формализации и доказательства построен на основе проекта AUTOLEAN.

Ключевые факты

  • MathCode переводит математическую задачу с обычного языка в теорему Lean 4 и пытается построить формальное доказательство
  • Постоянный языковой сервер Lean ускоряет проверку компиляции доказательства с ~30 секунд до ~0,4 секунды после прогрева
  • Ищет проверенные леммы библиотеки Mathlib через leansearch.net и Loogle, чинит ошибки по диагностике LSP
  • Разбивает сложные теоремы на подзадачи и доказывает их параллельно; параллельно запускает несколько планировщиков с разными стратегиями доказательства
  • Генерирует граф зависимостей теорем и лемм в Obsidian; работает на macOS (arm64) или Linux (x86_64) с CLI Codex в качестве бэкенда

Почему это важно

Формальная верификация в Lean традиционно требует ручного перевода математической идеи в формальный язык, трудоёмкий шаг, который останавливает многих. MathCode берёт этот перевод на себя и ускоряет цикл проверки: компиляция доказательства после прогрева языкового сервера занимает около 0,4 секунды вместо около 30 секунд без него, это делает итеративную работу агента над доказательством практически интерактивной. Инструмент также накапливает базу уже доказанных теорем и лемм, которые можно переиспользовать, а не доказывать заново.

Кому это важно

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

Как это применить

Установка, клонирование репозитория с GitHub и запуск скрипта setup.sh, который готовит релизную сборку, скачивает рантайм и тулчейн Lean и ставит локальный запускатель mathcode; предварительно нужен вход в CLI Codex. Команда вида mathcode -p "prove that the square of an even number is even" формализует задачу и пытается её доказать, результаты сохраняются в папку LeanFormalizations. Есть отдельная команда для запуска веб-интерфейса в браузере. Требования, macOS (arm64) или Linux (x86_64); данных о цене или лицензии в источнике нет.

Можно ли доверять

Источник, собственный сайт проекта на GitHub Pages, то есть это описание от самих авторов, а не независимый обзор. В библиографической записи проекта авторство указано коллективно как «Team Math-AI», без имён отдельных участников и без привязки к организации. В источнике нет ни результатов тестов, ни показателей успешности доказательств, ни сравнения с другими системами формализации и доказательства теорем, приведено только внутреннее до/после по времени компиляции (~30 с против ~0,4 с). Оценивать реальную эффективность MathCode стоит только после независимой проверки.

Риски и подводные камни

Инструмент завязан на конкретную платформу (только macOS arm64 или Linux x86_64) и на внешний бэкенд, CLI Codex, доступ к которому нужен отдельно. Конвейер формализации построен поверх стороннего проекта AUTOLEAN, который в источнике не описан и не датирован. Данных о лицензии и условиях использования нет, как и информации о том, кто именно стоит за проектом за пределами коллективного названия «Team Math-AI».