The Mathematics Autoformalization Project (MAP) is a global initiative to transform existing mathematical knowledge into an open, interconnected, machine-verifiable corpus, laying the foundation for a new era of mathematical and scientific discovery.
Our Mission
For centuries, mathematical knowledge has accumulated across millions of papers and textbooks. MAP seeks to bring this knowledge together into a unified computational foundation, making mathematics easier to explore, verify, and extend.
The Opportunity
For centuries, mathematics has advanced through the cumulative efforts of generations of mathematicians. Yet much of this knowledge remains scattered across the published literature, encoded in natural language and dependent on human expertise to interpret and connect.
Formal verification offers a way to represent this knowledge precisely, allowing mathematical results to be checked, searched, connected, and reused.
Until recently, the human effort required to formalize mathematics made comprehensive coverage impractical.
Advances in AI have fundamentally changed what is possible. Autonomous systems can now formalize mathematical developments at scales previously unimaginable.
For the first time, we can seriously pursue the systematic formalization of the world's mathematical literature.
Much as the Human Genome Project transformed biology by creating shared scientific infrastructure, MAP seeks to build a computational foundation for the next era of mathematics.
What We Do
Autonomous AI systems translate mathematical definitions, theorems, and proofs from the published literature into Lean, building upon existing formal libraries wherever possible.
Machine-checked proofs establish deductive correctness, while independent AI reviewers and human mathematicians evaluate whether formalized statements faithfully capture their original meaning.
Formalized results are connected into a shared mathematical corpus, allowing new developments to build on existing knowledge rather than repeatedly reconstructing it.
The territory
Mathematics is one territory with many regions. Each has its own objects, its own methods of proof, and its own literature. MAP's corpus spans all of them, formalized in Lean and connected into one whole.
The MAP Plan
MAP proposes a coordinated, multi-year effort to formalize existing mathematical knowledge at unprecedented scale, beginning with an initial campaign over the coming year.
Rather than treating each theorem or publication as an isolated project, MAP will build an integrated corpus in which definitions, proofs, and mathematical structures can be shared across sources and disciplines.
The effort will progress from foundational graduate mathematics to advanced research literature, systematically building the infrastructure needed for increasingly comprehensive coverage.
These figures represent the project's initial scope and planning targets, not completed formalizations or committed timelines.
The Inflection Point
Recent advances in AI-driven formalization have enabled increasingly large mathematical developments to be translated into machine-checkable code. These milestones demonstrate the growing capabilities of autonomous formalization systems and point toward the possibility of formalizing entire mathematical libraries.
Selected milestones in large-scale formalization · lines of Lean
How much is formalized today · a rough estimate
Of 37,936 definitions, theorems, and proofs tagged across 778 Wikipedia mathematics articles and matched against Mathlib4 declarations. A best-effort snapshot of one sample, not a measure of all mathematics.
Source WikiLean, a project by Jack McCarthy · accessed October 16, 2026
The next challenge is not simply to formalize larger individual results, but to bring the world's mathematical knowledge together into a coherent, reusable whole.
The Future
A comprehensive, machine-verifiable mathematical corpus could transform how mathematics is discovered, shared, and applied.
Enable mathematicians to search existing knowledge, trace dependencies, identify connections across fields, and build new results on verified foundations.
Provide structured, machine-verifiable knowledge that supports the development and evaluation of more capable mathematical reasoning systems.
Make advanced mathematics easier to discover and apply across physics, engineering, computer science, biology, economics, and other quantitative disciplines.
Create an open, extensible representation of mathematical knowledge that captures not only results, but also their assumptions, dependencies, and provenance.
As the cost of formalization and verification decreases, the possibilities for mathematical discovery and application expand.
Collaboration
MAP brings together mathematicians, AI researchers, computer scientists, formal verification experts, and institutions working toward a shared goal.
The initiative builds upon and seeks to connect existing open mathematical infrastructure, including Mathlib, Tau Ceti, Prove2Me, and Formalpedia.
Our aim is to strengthen the mathematical ecosystem by enabling complementary projects and communities to contribute toward a common, reusable body of knowledge.
Formalizing the world's mathematics will require a global effort. We welcome mathematicians, researchers, AI laboratories, universities, foundations, and industry partners interested in contributing expertise, infrastructure, and support.
contact@mapmath.org