Axiom Math Uses AI Formal Verification on the Stacks Project to Counter Mathematical 'AI Slop'

AI-generated content is flooding into mathematics, bringing with it a large volume of proofs that have not been rigorously reviewed. Facing this trend, startup Axiom Math has chosen a different path: using AI agents to perform formal verification of mathematical proofs. According to its disclosure, the company's AI agents have completed formal verification of the Stacks Project—one of the largest document libraries in mathematics.

Mathematics is facing an 'AI slop' problem

Large language models write proofs far faster than humans can review them. A proof that appears structurally reasonable and uses notation properly may contain hidden flaws in key reasoning steps, and such flaws are not necessarily discoverable through quick reading. As AI-generated proofs pour into preprint platforms and academic exchange channels in large numbers, what the mathematics community faces is not 'a lack of content' but 'too much content, with truth and falsehood hard to distinguish.'

Axiom Math calls this phenomenon 'AI slop' in mathematics and argues that manual peer review processes alone are no longer sufficient to cope with it. Verification, rather than generation, has become the more urgent step.

Formal verification: making proofs machine-checkable

The core idea of formal verification is to translate mathematical proofs into a formal language that machines can check step by step, and then have a verifier confirm one by one whether each step of reasoning is valid. Unlike natural-language proofs, which rely on the reader's understanding, formal verification produces a mechanically recheckable conclusion: the proof holds, or it fails at some step.

This approach is not new, but it has long been constrained by labor costs—formalizing existing mathematical literature is extremely labor-intensive work. Axiom Math's entry point is to use AI agents to undertake this translation and verification process, thereby moving formal verification from 'something only a few projects can do' toward 'something that can be done for large-scale literature.'

The core tool that formal verification relies on is the proof assistant, also known as an interactive theorem prover, with representative systems including Lean, Coq, and Isabelle. Such systems contain a built-in formal logic kernel based on type theory or set theory. Users write definitions, lemmas, and proofs in the system's dedicated language, and the kernel checks step by step whether each inference is validly derived from prior steps and axioms.

Unlike automated theorem proving (such as SAT/SMT solvers), proof assistants are not responsible for 'coming up with' proofs, only for 'checking' them; the construction of proofs is still done by humans or AI. Lean's mathematical library mathlib is currently the largest community-built formal mathematics library, having accumulated hundreds of thousands of theorems, and can serve as a real-world reference for understanding 'how large a scale formal verification can already handle.'

What completing verification of the Stacks Project means

The Stacks Project is an important document library in the field of algebraic geometry, large in scale and complex in structure, and has long been regarded as a hard nut to crack for formal verification. Axiom Math's AI agents completing formal verification of it shows that agents possess usable processing capability on long-range mathematical texts with multi-layered dependencies, not merely short exercise-level verification.

The practical value of this result lies in establishing a trusted baseline: once a considerable scale of existing mathematical content has been formalized, newly emerging AI-generated proofs have a verification environment to compare against, without having to build a checking system from scratch each time.

The Stacks Project was initiated and is continuously maintained by Johan de Jong of Columbia University. It is an open online reference work on algebraic geometry and the theory of algebraic stacks, containing thousands of tagged definitions, lemmas, and theorems, with extensive cross-section citations among chapters and dependencies forming a deeply nested graph structure.

This kind of 'long-range dependency' is precisely the most difficult aspect of formal verification: verifying a later theorem often requires first formalizing all the preceding results it depends on, and the absence of any one link will interrupt the check. Therefore, completing formalization of the Stacks Project is not just a matter of handling scale, but also a matter of handling dependency closure, which is why the result is regarded as a marker of difficulty.

The division of labor between generation and verification is being reshaped

Axiom Math's positioning is not to compete with generative models in writing proofs, but to make verification into infrastructure. This division of labor has its own practical logic: the threshold for generation is falling, while the scarcity of verification is rising. Whoever can provide low-cost, scalable verification capability will control the key link in the quality of AI mathematical content.

Of course, formal verification also has boundaries. What it verifies is that 'the proof holds under its formalized formulation,' while whether the formal translation itself is faithful to the original mathematical intent is still a step that requires human oversight. Whether Axiom Math's approach can be stably reproduced on a larger range of literature also needs more public results to test.

For readers interested in the real-world application of AI in scientific research, this direction provides a sample worth tracking: AI is not only a producer of content, but can also be a gatekeeper of content.

One-line Summary

Axiom Math uses AI agents to complete formal verification of the Stacks Project, advocating verification rather than generation.

Paragraph Summary

The article discusses the 'AI slop' problem brought by the large influx of AI-generated proofs into mathematics: large language models produce proofs far faster than humans can review them, and seemingly well-formed proofs may contain hidden flaws. Startup Axiom Math chooses verification as its entry point, using AI agents to translate mathematical proofs into a formal language that machines can check step by step, and has disclosed completion of formal verification of the Stacks Project, an important document library in algebraic geometry. The article notes that this result shows agents can handle complex mathematical texts with long-range, multi-layered dependencies, and that its value lies in establishing a trusted baseline against which newly emerging AI-generated proofs can be compared. At the same time, the article also points to boundaries: whether formal translation is faithful to the original mathematical intent still requires human oversight, and the approach's large-scale stability remains to be tested by more public results.