The Map: Mathematics Autoformalization Project

Anthropic's Claude autoformalized Fermat's Last Theorem in 11 days, writing 13 million lines of code that also covered the prerequisite 20th-century literature, according to the MAP (Mathematics Autoformalization) Project. The result extends a five-order-of-magnitude growth trend in autoformalized math, from roughly 400 lines at the DeepMind IMO silver-medal era to 3.5K lines for de Bruijn's ABC theorem in June 2025, 25K lines for the Prime Number Theorem in September 2025, 200K lines for Maryna Viazovska's sphere-packing work in March 2026, and 1M lines for OpenAI's Erdős Unit Distance Conjecture formalization in June 2026. The MAP Project aims to build a comprehensive formal database of all known mathematics, an effort compared to AlphaFold's tabulation of 200 million proteins, and Kevin Buzzard, who held a £900K grant to formalize Fermat's proof over 5 years, now plans to formalize the Langlands program literature.

We are poised to translate all known math into formal code. This is the math-equivalent of the Human Genome Project, or AlphaFold in modern times. On September 4th, Anthropic shocked the math world by formalizing Fermat’s Last Theorem https://x.com/AnthropicAI/status/2095947707605266436 . Fermat famously stated it in 1637, Sir Andrew Wiles & Richard Taylor proved it in 1995, and recently Kevin Buzzard launched a project to formalize it: translate the human proof into machine code. This was long viewed as a pipe dream, and Buzzard had a £900K grant to do so over 5 years. Even so, this would only scratch the surface, since the Fermat proof also depends on loads of math literature from the 20th century. That is why it was so shocking when, in just 11 days, Claude wrote 13 million lines of code to autoformalize the Fermat proof, along with all the pre-requisite literature. For Buzzard, this now unlocks the chance to formalize the literature the Langlands program, which he is concerned might contain subtle errors. This achievement would have been thought crazy just last year, but in fact the implications are much more profound. We now have the opportunity to formalize all mathematics currently known to humanity. Just as AlphaFold tabulated all 200 million proteins known to humanity, the MAP Project is aimed to do the equivalent in math: create a comprehensive formal database for all known mathematics. Unlike the replication crisis which plagues other sciences, the formalization process can flag errors in the literature, which have occasionally destabilized entire research programs historically. We are already seeing early examples of this in recent AI-for-math results. Claude’s achievement is not just one data point, but in fact one in a growing sequence. Back when Deepmind’s IMO silver medal remained supreme, the record for autoformalized math was around 400 lines. - In June 2025, the record jumped to 3.5K lines with the formalization of de Bruijn’s ABC https://www.youtube.com/watch?v=WMzP-nmrd6g theorem. - In September 2025, human-assisted autoformalization of the Prime Number Theorem https://x.com/jdlichtman/status/1966240549272482288 broke 25K lines of code, completing the 2024 challenge set by Terry Tao and Alex Kontorovich. - In March 2026, the autoformalization of Maryna Viazovska’s Fields medal work on sphere packing https://x.com/jdlichtman/status/2028587770520965487 totaled 200K lines of code. - In June 2026, OpenAI’s autoformalization of the Erdős Unit Distance Conjecture https://x.com/AlexKontorovich/status/2070561716778254769 crossed 1M lines of code. - Now, Claude’s proof of Fermat’s Last Theorem in 13M lines represents a smooth exponential in the growth of 5 orders-of-magnitude. As shocking as the scale of the Fermat's Last Theorem proof, the trends becomes much more visible on a logarithmic plot: Beyond the raw code length, the proof of Fermat's Last Theorem draws on an expansive swath of modern mathematics. The increasing complexity of mathematical contents and level of autonomy that AI agents have demonstrated is simply awe-inspiring. I began my mathematical life in number theory. In 2019, I came to Oxford for my doctorate with James Maynard, motivated by the mysteries of the prime numbers https://www.quantamagazine.org/graduate-students-side-project-proves-prime-number-conjecture-20220606/ . However, also that year, Kevin Buzzard gave a talk in the Oxford seminar about a new programming language called Lean: His talk rewired my nerve endings. He explained how natural-language math could be translated into Lean, so the correctness of a proof became the compilation of a program. Buzzard himself "became addicted" to Lean programming, after hearing Tom Hales' 2017 talk on the historic formalization of Kepler's conjecture. Kepler was itself a centuries-old problem, whose eventual solution was so complicated that human referees could not vet it for certain. But after over a decades-long effort, Kepler was formalized. Buzzard's talk immediately convinced me of the power of machine verification, and the increasingly complex mathematical topics that Lean could handle gave a sense of inevitability. This was a true revolution to "digitize mathematics", as he put it. At the same time, I knew a parallel revolution was taking shape in artificial intelligence, following ImageNet, AlphaZero, and the Transformer. Now, the subsequent rise of chatbots--and agents this past year--have taken the AI revolution to unprecedented heights. Until recently, my work has remained in number theory, and I was only monitoring AI & formalization progress from afar. Manual programming was a specialized skillset unto itself, and even experts took great lengths to translate even small excerpts of natural-language math. But this past year, I found myself on the front-lines in a singular moment in the history of mathematics. The revolutions in AI and formalization are now converging into a hybrid: autoformalization. The ability for AI agents to formalize on their own is taking off, both in the volume and quality of code generated. Back when I was monitoring AI and formalization progress from afar, I noticed that the majority of my colleagues were quite dismissive of, not only the rate of progress, but also the impact that would be felt on the field. I kept quiet, but always felt that dismissal quite confusing. However, the past year of undeniable progress in AI-for-math and formalization has corroborated my predicted trajectory of the field. It was only this year that I realized I had a voice, taken with some ambivalence, to provide clarifying perspectives. Now more than ever, such voices are needed amidst a backdrop of perceived confusion and chaos during the current transformation of mathematics. AI is now capable to formalize the curricula in graduate mathematics courses, from core topics in algebra, analysis, geometry, topology, and applied math; then beyond to all textbooks and the research literature more broadly. Since math is cumulative by nature, the MAP will represent a historic effort to map the known territory of all human mathematics. Rough estimates on the total mathematical corpus is on the order of 10B lines of code, based Claude's current level of efficiency to say nothing of future efficiency gains . We are now poised to achieve this in the next year, with sufficient coordination and funding among academia, frontier labs, philanthropy, and government. More details to come as the developments rapidly evolve, with limited time to respond to the moment. Many thanks to @patshafto https://x.com/@patshafto for leadership of DARPA’s expMath program, and @ericweinstien https://x.com/@ericweinstien for advice developing MAP. Beyond the intrinsic value of verification, the MAP will also be a foundation for future mathematics. It serves as critical infrastructure upon which the next generation of research will be based. As such, MAP has the prospect to set the stage for future discovery. Amidst the many impressive AI-generated math results in the headlines, the proofs themselves seem to lack genuine originality: the objectively impressive results leverage clever combinations of known methods. Much of the current commentary on AI-for-math assumes that this will remain so forever, and that AI will always lack novel insight. However, fully explicit code has the prospect to provide precise training ground for next-generation models. Hence we shall now map out the territory, and provide a firm base to then set out and explore the mathematical frontier.