M2F: 대규모 수학 문헌의 자동 정형화

M2F: Automated Formalization of Mathematical Literature at Scale

수학의 자동 정형화는 기계적 검증을 가능하게 하지만, 여전히 독립된 정리나 짧은 코드 조각에 국한되어 있습니다. 교과서나 연구 논문 수준으로 확장하는 문제는 파일 간 의존성 관리, 임포트 해결, 그리고 전체 프로젝트의 종단 간(end-to-end) 컴파일 보장이 필요하기 때문에 아직 대부분 미해결 상태로 남아 있습니다. 본 논문에서는 Lean 환경에서 종단 간 프로젝트 규모의 자동 정형화를 수행하는 최초의 에이전트 기반 프레임워크인 M2F(Math-to-Formal)를 제안합니다. 이 프레임워크는 두 단계로 동작합니다. 명제 컴파일(statement compilation) 단계에서는 문서를 원자적 블록으로 분할하고, 추론된 의존성에 따라 정렬하며, 증명 내에 자리표시자(placeholder)를 허용하면서 프로젝트가 컴파일될 때까지 선언부 뼈대(declaration skeletons)를 수정합니다. 증명 복구(proof repair) 단계에서는 고정된 시그니처 하에서 목표 조건부 국소 편집(goal-conditioned local edits)을 사용하여 이러한 빈 공간을 채웁니다. 두 단계 전반에 걸쳐 M2F는 검증기(verifier)를 루프 내에 유지하며, 툴체인의 피드백을 통해 개선이 확인될 때만 수정 사항을 반영(commit)합니다. M2F는 약 3주 만에 실수 해석학 및 볼록 해석학에 관한 479페이지 분량의 교과서 원본을 153,853줄에 달하는 프로젝트 규모의 Lean 라이브러리로 변환하였으며, 이를 증명이 수반된 Lean 선언으로 완전히 정형화했습니다. 이는 일반적으로 수개월 또는 수년의 전문가 노력이 필요한 수준의 교과서 규모 정형화를 매우 빠른 속도로 달성했음을 보여줍니다. FATE-H 벤치마크에서는 강력한 베이스라인의 $80\%$ 대비 $96\%$의 증명 성공률을 달성했습니다. 종합적으로 이러한 결과는 수학 문헌의 실용적이고 대규모적인 자동 정형화가 눈앞에 다가왔음을 보여줍니다. 본 연구를 통해 생성된 전체 Lean 코드는 https://github.com/optsuite/ReasBook.git 에서 확인할 수 있습니다.

Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is largely unaddressed, as it requires managing cross-file dependencies, resolving imports, and ensuring that entire projects compile end-to-end. We present M2F (Math-to-Formal), the first agentic framework for end-to-end, project-scale autoformalization in Lean. The framework operates in two stages. The statement compilation stage splits the document into atomic blocks, orders them via inferred dependencies, and repairs declaration skeletons until the project compiles, allowing placeholders in proofs. The proof repair stage closes these holes under fixed signatures using goal-conditioned local edits. Throughout both stages, M2F keeps the verifier in the loop, committing edits only when toolchain feedback confirms improvement. In approximately three weeks, M2F converts long-form mathematical sources into a project-scale Lean library of 153,853 lines from 479 pages textbooks on real analysis and convex analysis, fully formalized as Lean declarations with accompanying proofs. This represents textbook-scale formalization at a pace that would typically require months or years of expert effort. On FATE-H, we achieve $96\%$ proof success (vs.\ $80\%$ for a strong baseline). Together, these results demonstrate that practical, large-scale automated formalization of mathematical literature is within reach. The full generated Lean code from our runs is available at https://github.com/optsuite/ReasBook.git.