Search papers, labs, and topics across Lattice.
AutoformBot, a multi-agent system, automates the translation of mathematical textbooks into formally verified Lean 4 code. By orchestrating thousands of LLM agents with verification tools and dependency-aware scheduling, the system constructs Atlas, a library of over 45,000 declarations and 500,000 lines of code derived from 26 textbooks. This demonstrates the feasibility of large-scale autoformalization, enabling automated verification of mathematical content.
Graduate-level mathematics can now be auto-formalized at scale, opening the door to automated verification of both human and AI-generated proofs.
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.
