mlsanityData to 7 Oct 2026

Automatic Textbook Formalization

arXiv 2604.03071 ↗First posted 3 Apr 2026cs.AIcited by 5

Not on the map. Why?

Abstract (arXiv)

We present a case study where an automatic AI system formalizes a textbook with more than 500 pages of graduate-level algebraic combinatorics to Lean. The resulting formalization represents a new milestone in textbook formalization scale and proficiency, moving from early results in undergraduate topology and restructuring of existing library content to a full standalone formalization of a graduate textbook. The formalization comprises 130K lines of code and 5900 Lean declarations and was conducted within one week by a total of 30K Claude 4.5 Opus agents collaborating in parallel on a shared code base via version control, simultaneously setting a record in multi-agent software engineering with usable results. The inference cost matches or undercuts what we estimate as the salaries required for a team of human experts, and we expect there is still the potential for large efficiencies to be made without the need for better models. We make our code, the resulting Lean code base and a side-by-side blueprint website available open-source.

Key facts. Cited by 5 papers in the map (data through 7 Oct 2026). Builds on 19 of its 45 references that are in the map. First posted on arXiv 3 Apr 2026.

Builds on

19 of 45 references.

References · 19

  1. 2023Toolformer: Language Models Can Teach Themselves to Use Toolscited by 4,072
  2. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  3. 2022Autoformalization with Large Language Modelscited by 252
  4. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  5. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  6. 2019The Lean mathematical librarycited by 127
  7. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  8. 2023At Which Training Stage Does Code Data Help LLMs Reasoning?cited by 82
  9. 2019Accelerating Self-Play Learning in Gocited by 60
  10. 2025Code to Think, Think to Code: A Survey on Code-Enhanced Reasoning and Reasoning-Driven Code Intelligence in LLMscited by 47
  11. 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematicscited by 43
  12. 2015A formal proof of the Kepler conjecturecited by 42
7 more
  1. 2024Unveiling the Impact of Coding Data Instruction Fine-Tuning on Large Language Models Reasoningcited by 31
  2. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
  3. 2026130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?cited by 16
  4. 2026M2F: Automated Formalization of Mathematical Literature at Scalecited by 12
  5. 2025The Equational Theories Project: Advancing Collaborative Mathematical Research at Scalecited by 8
  6. 2022Formalising the h-principle and sphere eversioncited by 6
  7. 2025Growing Mathlib: maintenance of a large scale mathematical librarycited by 5

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 5.

5 papers.

  1. 2026Formalizing Mathematics at Scalecited by 5
  2. 2026Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theorycited by 1
  3. 2026Prove2Me: An Open Collaborative Platform for Scaling Math Formalizationcited by 1
  4. 2026Learning to Discover Interesting Mathematicscited by 0
  5. 2026Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalizationcited by 0