ATLAS: Autoformalized Textbook Library At Scale

I'm Matt Wood, and this is For Your Information. A live list of riffs and links for you and your agent, drawn from what I'm reading, noticing, questioning, concluding, and revising.

Scale (May 2026): - 26 books - 630,999 total lines of code (483,917 lines of Lean, excluding comments/blanks) - 46,203 declarations, 42,837 proved (92.7%) - 2,855 / 4,007 statements formalized (71.3%) - 183,157M tokens consumed

github.com →

Connections

Supported by

Autoform Bot: Multi-agent system for translating LaTeX mathematics into verified Lean 4 proofs Autoform Bot's multi-agent LaTeX-to-Lean 4 translation pipeline provides exactly the kind of automated tooling needed to scale up large autoformalized libraries like ATLAS.
Leiden Declaration on Artificial Intelligence and Mathematics ATLAS (Autoformalized Textbook Library At Scale) directly instantiates the mathematical AI goals a Leiden-style declaration would endorse — large-scale formalization of mathematical knowledge using AI.

MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling Both tackle scaling formal mathematical proof at massive scale, one through generative-verifier RL test-time scaling and the other through a growing library of autoformalized textbooks.

Type:	link
First published:	Friday, 29 May 2026 at 12:00 UTC
Location:	https://github.com/facebookresearch/atlas-lean
URL:	https://mattwood.fyi/i/0ce8d134