Axiom Math has formalized almost all definitions and theorems in the Stacks Project algebraic geometry textbook in Lean, which checks every step of a proof: AI agents wrote most of the 15,75 million nonempty lines of code, while humans checked about 30 thousand against the textbook

Axiom Math has formalized almost all definitions and theorems in the Stacks Project algebraic geometry textbook in Lean, which checks every step of a proof: AI agents wrote most of the 15,75 million nonempty lines of code, while humans checked about 30 thousand against the textbook

On November 4, Axiom Math released the library on GitHub and launched a website displaying textbook pages alongside their Lean code. According to the company's description, both mathematicians and AI agents can use the library's definitions and theorems in new proofs.

Mathematician Johan de Jong conceived the Stacks Project in 2005 and continues to lead it. The textbook contains 7 654 pages on algebraic geometry, the branch of mathematics that studies shapes defined by equations. Each definition and theorem has a permanent four-character tag that links it to the corresponding Lean code.

Axiom explains its reason for formalizing the textbook in Lean: AI systems produce mathematical arguments faster than humans can check them, so software needs to take on the verification. Formalizing algebraic geometry in Lean was difficult because a modern proof can depend on a long chain of theorems that had yet to be formalized in Lean.

The agents translated theorem statements into Lean and constructed proofs. Axiom identifies consistency as a particular challenge: two agents can prove valid theorems about the same object while defining it slightly differently. Lean will accept each file separately, but combining their results will be difficult.

Lean checks that a proof establishes the statement as written; if that statement is inaccurate, it will certify a proof of a different theorem from the one in the textbook. Thomas Hales, whose proof of the Kepler conjecture on the densest packing of spheres was verified by computer, wrote in a guest post on mathematician Terence Tao's blog that a Lean proof should be accepted only after a human has checked the statement. Axiom writes: “Ensuring that every formal statement faithfully captures the mathematical meaning of the source text is even more important than checking its proof.” According to the company's description, statements are checked automatically: agents compare them with the textbook, and an inaccurate definition will become apparent because other theorems depend on it.

On October 27, Axiom released its Lean formalization of the classification of finite simple groups, a theorem about symmetry. In that project, humans checked a single final statement. Stacks contains thousands of statements, and the library is divided into two tiers. StacksCore accounts for about 0,2% of the lines: the authors of the formalization checked this code against the textbook themselves, a process the project description calls “self-assessment.” StacksFrontier contains the rest, mostly written by agents: Lean has accepted its proofs, while human review of the code is still pending.

According to Axiom, the agents found dozens of statements in the textbook that needed clarification: some lacked necessary assumptions, while others failed in special cases. When agents could not complete a proof, they investigated the cause, constructed counterexamples, and formalized corrected theorems.

On October 21, Stacks Project founder de Jong asked people to refrain from submitting AI-written comments and corrections for the time being, adding: “Anything you find using AI, I can also find using AI (and perhaps I already have)!”

Axiom says it respects this request and keeps its counterexamples and corrections in its own GitHub project. On November 5, user koffie opened an issue there, saying they had been unable to find a readily accessible list of errors in the textbook and asking for the problems described in Axiom's blog post to be published in a more accessible form than Lean source code.