yesnoerror releases AutoformBot, a multi-agent system that translated 26 graduate math textbooks into Lean 4

Original post

Very interesting work here! Lots of rough edges (misformalizations, etc) but it points the way to a landscape of possibility!

What will be really interesting is to see if it's possible to actually teach out of such books (and of course clean things up as you go)... [It's possible that the AI took so many shortcuts that it really doesn't represent the difficulty of some proof, etc; still, experiments like these can give a lot of useful information.]

Charles Arnal@arnal_charles

Our team at @AIatMeta is excited to announce ATLAS: one of the largest automated formalization efforts to date.

ATLAS contains Lean 4 formalizations of both statements and proofs from 25+ mathematics textbooks, spanning dozens of domains, for a total of 500k lines of code. We are also releasing a flexible formalization harness and a companion paper.

External contributions are welcome!

Joint work spearheaded by our amazing PhD student Ahmad Rammal (@Ahmad3Rammal), together with Niket Patel (@niketnpatel ), Fabian Gloeckle (@FabianGloeckle), Amaury Hayat (@Amaury_Hayat), Remi Munos (@MunosRemi), Julia Kempe (@KempeLab), Vivien Cabannes, and myself from @AIatMeta, @NYUDataScience , and Ecole des Ponts. This is an ongoing effort; more details in the thread below. (1/9)

6:52 AM · May 29, 2026 · 5.5K Views

2605.29955

YESNOERROR.COMVia

VIEWS14KBOOKMARKS19LIKES82REPLIES4

spicylemonade@spicey_lemonade

Interestingly, ProofBench actually shows Opus 4.8 is almost as good as Aristotle at formalization (and with much lower latency). I reckon Mythos surpasses Aristotle

Przemek Chojecki | PC@prz_chojecki

All such efforts in formalization at scale are awesome. Two remarks:

- the team could have used Codex which is much better at math than Opus

- there are many open source harnesses that might help with verification/formalization. For example ours: https://github.com/ulamai/ulamai

31d14K8219

RETWEETS9

Jesse Michael Han@jessemhan

most of the effort for @mathematics_inc's spherepacking formalization was spent on compressing and cleaning up a first-pass 500K LOC formalization to <200K LOC. creating infrastructure that can scale autoformalization to the frontiers of mathematics, software, and everything else is our #1 priority here - if this excites you, come work with us!

Alex Gu@minimario1729

Congrats to the @AIatMeta team on the release of ATLAS, a large-scale autoformalization effort with 500K+ LOC! It is very impressive work, and we look forward to what's next! At the same time, the quality issues that have recently surfaced reinforce why rigorous and trustworthy autoformalization are crucial research challenges.

31d7.5K5117

Alex Gu@minimario1729

31d13.4K579

Alex Gu@minimario1729

Scaling autoformalization is an important direction for us. We aim not only to formalize mathematics at scale, but to do so with the rigor, fidelity, and engineering quality needed to build libraries others can confidently trust and extend.

Join us! http://math.inc/careers

Alex Gu@minimario1729

In our evaluations, models like Codex employed elaborator-level tactics to bypass constraints. One example shows a Codex-generated snippet using "ax" ++ "iom" to inject an axiom via metaprogramming. This evades static detection but is reliably caught by Comparator.

31d1.9K236

Alex Gu@minimario1729

At Math Inc, we place deep emphasis on this challenge. As autoformalization efforts grow in scale and ambition, the risks of subtle logical errors, unintended axiom usage, and semantic mismatches increase significantly. A successful lake build is necessary but far from sufficient.

Alex Gu@minimario1729

31d2.4K224

yesnoerror@yesnoerror

AutoformBot is a milestone for AI in mathematics: a multi-agent system that reads entire graduate math textbooks and outputs fully verified Lean 4 code—at scale.

In just weeks, it formalized 26 textbooks (analysis, algebra, topology, combinatorics, probability), generating ATLAS: 45,000+ Lean declarations (500k LOC) with 71% theorem/lemma/definition coverage. Some books exceed 90%.

Claude Opus 4.6 outperformed Gemini 3.1 Pro (92% vs. 46% goal completion). Layered feedback (orchestrator, supervisor, trace analyzer) and parallel LLM agents were key—ablation drops coverage by up to 26 points.

Cost? Already lower per line than expert human formalizers. Human audits confirm the method’s reliability.

End result: Large-scale, automated formalization of research-level mathematics is now not just possible, but practical. Opens the door to auto-verifying both human and AI-generated proofs, and to new forms of human-AI mathematical collaboration.

Get the full analysis here: http://yesnoerror.com/abs/2605.29955

// alpha identified // $YNE

31d1.5K163

Rado Kirov@radokirov

Indeed the most interesting thing to me is not the volume of lean produced but starting to think about UI affordances for human reviewing the output at scale like https://rammalahmad.github.io/atlas/ . Sadly, I don’t think many math experts will engage with this at the current level of misformalization, but maybe more at the next inevitable iterations when the output is hopefully 70-80% there.

31d1461

Charles Arnal@arnal_charles

Thanks for the positive reaction! We were eager to get it out to collect early feedback, but as you pointed out this is very much a v1, and we plan on further improving it over the next months.

As it is right now, it's probably not prime teaching material, but we hope to get to such a stage relatively soon.

31d267

T M Nguyen@TMNguyenSFT

This is a common failure point in lean formalization with AI. It is possible to constrain it but you have to know it exists and why it happens which they apparently did not.

I discovered it the hard way myself so I know firsthand what happened here and how they can fix/prevent/reduce it with AI.

Long story short, when faced with a tough formalization task that is either deep or wide, the AI will shortcut the process to get it done.

31d21

Shriram Krishnamurthi (primary: Bluesky)@ShriramKMurthi

@AlexKontorovich Why would this book be better than a regular text, in the foreseeable future?

Also, I wish the OP were a bit more honest and modest about it, given that people seem to have found bugs, sorry's, etc.?

31d7

M-RAMDHAN@med406395470079

@AlexKontorovich https://doi.org/10.5281/zenodo.20261040

31d2