ИССЛЕДОВАНИЕ · RESEARCH · #2565
PaperFormalizer: конвейер автоформализации с участием автора для Lean (arXiv:2610.31810v1)
PaperFormalizer — это конвейер на базе Lean, который преобразует LaTeX статьи в граф зависимостей утверждений, проверяет каждое утверждение на соответствие/двусмысленность/корректность и формализует с доказательствами в Lean с использованием Mathlib и дополнительных библиотек. Система работает внутри кодирующих агентов (Claude Code или Codex), запрашивает у автора разрешение в случае неоднозначностей и выдаёт аннотированную исправленную версию статьи, отчёт об изменениях и связанный код Lean (репозиторий: github.com/Jiyuan-Tan/PaperFormalizer; формализованные статьи доступны на paperformalizer.org).
КЛЮЧЕВЫЕ ТЕЗИСЫ
- PaperFormalizer — это конвейер на базе Lean, который преобразует LaTeX статьи в граф зависимостей утверждений, проверяет каждое утверждение на соответствие/двусмысленность/корректность и формализует с доказательствами в Lean с использованием Mathlib и дополнительных библиотек.
- Система работает внутри кодирующих агентов (Claude Code или Codex), запрашивает у автора разрешение в случае неоднозначностей и выдаёт аннотированную исправленную версию статьи, отчёт об изменениях и связанный код Lean (репозиторий: github.com/Jiyuan-Tan/PaperFormalizer; формализованные статьи доступны на paperformalizer.org).
- Делая автоформализацию с участием автора практичной и удобной для совместного использования, PaperFormalizer может снизить стоимость создания машинно-проверяемых статей и уменьшить скрытые лакуны в математических доказательствах.
ПОЧЕМУ ЭТО ВАЖНО
Делая автоформализацию с участием автора практичной и удобной для совместного использования, PaperFormalizer может снизить стоимость создания машинно-проверяемых статей и уменьшить скрытые лакуны в математических доказательствах.