PaperFormalizer превращает LaTeX-статьи в проверенный Lean-код с участием автора

Команда из Стэнфорда предложила способ, который должен сделать формальную верификацию математических статей рутинной частью подготовки публикации. PaperFormalizer, выпущенный Джиюанем Таном, Василисом Сиргканисом и Хосе Бланше, превращает LaTeX-исходник в Lean-проверенную версию работы. Он работает как агентный конвейер внутри Claude Code или Codex. Ключевая идея: даже тщательно вычитанная статья может содержать мелкие пробелы в доказательствах или формулировках допущений, и лучше всего их закрывает сам автор, которому машина помогает.

Конвейер от LaTeX до Lean

Процесс начинается с исходника. PaperFormalizer транскрибирует статью в граф зависимостей утверждений: какие леммы нужны для теорем и что на что опирается. Затем каждое утверждение проходит аудит на естественном языке по трём осям: верность исходному смыслу, неоднозначность и корректность. Только после этого система формализует утверждения и доказывает их в Lean.

Для доказательств конвейер использует несколько источников:

• Mathlib, основная математическая библиотека Lean;
• опциональные доменные библиотеки под конкретную область;
• личный набор инструментов автора, то есть его собственные леммы и определения.

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

Автор решает, что утверждает статья

Автоформализация обычно страдает от тихой подмены смысла. Модель может доказать формально безупречную теорему, которая говорит не то, что имел в виду автор. Создатели PaperFormalizer исходят из того, что только автор знает, что утверждение должно означать и как лучше закрыть формализационный пробел.

Поэтому система следует нескольким правилам:

• если утверждение допускает больше одного прочтения, конвейер останавливается и задаёт вопрос;
• каждое исправление подаётся на естественном языке и в TeX-символах как предложение, которое можно принять, отклонить или перенаправить;
• любое решение, способное изменить заявленное в статье, остаётся за автором.

В отличие от систем, которые пытаются формализовать чужие работы целиком и автономно, здесь человек выступает арбитром смысла, а машина берёт на себя тяжёлую механику доказательств.

Что получает автор на выходе

Результат работы состоит из трёх частей:

• аннотированная и исправленная версия статьи;
• отчёт обо всех внесённых изменениях;
• Lean-код, в котором каждая декларация связана с утверждением, которое она формализует.

Последняя связь важна для читателя. Можно открыть любую теорему в тексте и увидеть соответствующий ей проверенный Lean-объект, а не искать соответствие вручную.

Общая библиотека проверенных работ

Авторы предлагают и экосистемный слой. Исследователи могут публиковать верифицированные статьи на сайте paperformalizer.org, а те, кто строит на этих результатах, получают возможность переиспользовать готовый Lean-код. Это снижает цену формализации следующей работы в той же области: нужные определения и леммы уже есть и проверены.

Инструмент опубликован на GitHub в репозитории Jiyuan-Tan/PaperFormalizer. Работа вышла 22 октября 2026 года и попала в ежедневную подборку Hugging Face Papers; организация на странице указана как Stanford University.

Практический смысл для исследователей

Для математиков и теоретиков из статистики, экономики и машинного обучения, чьи выводы держатся на доказательствах, это способ получить независимую проверку до отправки в журнал. Особенно полезно там, где ошибки в допущениях проходят рецензирование незамеченными. Порог входа ниже, чем у ручной формализации в Lean: нужен LaTeX-исходник, доступ к Claude Code или Codex и готовность отвечать на вопросы системы.

Осторожность тоже нужна. Конвейер проверяет, что формальное утверждение доказано, но соответствие формализации замыслу по-прежнему подтверждает человек. Поэтому качество результата зависит от внимательности автора в тех самых точках, где система останавливается и спрашивает.