# Formalizing Mathematics at Scale

arXiv: https://arxiv.org/abs/2605.29955 · HTML: https://mlsanity.com/paper/2605.29955/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 59 references that are in the map.
- First posted on arXiv 28 May 2026.

## Builds on (most cited first, 26 of 26)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [MetaGPT: Meta Programming for A Multi-Agent Collaborative Framework](https://mlsanity.com/paper/2308.00352/) (2023)
- [SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering](https://mlsanity.com/paper/2405.15793/) (2024)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Towards Autonomous Mathematics Research](https://mlsanity.com/paper/2602.10177/) (2026)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [Progress in Formalizing Sphere Packing in Dimension 8](https://mlsanity.com/paper/2604.23468/) (2026)
- [Automatic Textbook Formalization](https://mlsanity.com/paper/2604.03071/) (2026)
- [The Network Structure of Mathlib](https://mlsanity.com/paper/2604.24797/) (2026)

## Built on by (most cited first, 10 of 10)

- [Prove2Me: An Open Collaborative Platform for Scaling Math Formalization](https://mlsanity.com/paper/2608.28433/) (2026)
- [Learning to Discover Interesting Mathematics](https://mlsanity.com/paper/2609.28603/) (2026)
- [When Does Structured Knowledge Help Neural Theorem Proving?](https://mlsanity.com/paper/2609.34460/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization](https://mlsanity.com/paper/2609.39228/) (2026)
- [AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness](https://mlsanity.com/paper/2610.05367/) (2026)
- [Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs](https://mlsanity.com/paper/2610.08144/) (2026)
- [Aligning Faithfulness for Theory-Scale Autoformalization](https://mlsanity.com/paper/2610.18498/) (2026)
- [Definition Grounding in Theory-Level Auto-formalization](https://mlsanity.com/paper/2610.19223/) (2026)
- [Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization](https://mlsanity.com/paper/2610.20573/) (2026)

## Abstract (arXiv)

We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependency-aware task scheduling, and collaborative version control, to translate informal textbook prose into machine-checked definitions and proofs. We apply our methods to a corpus of 26 open-access textbooks spanning analysis, algebra, topology, combinatorics, and probability, producing Atlas: a verified library of over 45,000 Lean 4 declarations and 500 thousand lines of code. We release two artifacts: (i) AutoformBot, the open-source multi-agent framework; and (ii) Atlas, the resulting formal library. Our results suggest that autoformalizing the core content of graduate-level mathematics at scale is now economically and technically feasible. This opens the door to the automated verification of both human- and machine-generated mathematics at a research level.