Axiom Math's AI Agents Formally Verified the Stacks Project, Betting on Checking Rather Than Generating

Axiom Math's AI agents have formally verified the Stacks Project, one of the biggest libraries in mathematics, according to a TechCrunch report published on November 5. It is a target that formal tooling has struggled to cover at scale.

The problem Axiom Math is attacking is concrete. Generative models have pushed the cost of producing something that looks like a proof close to zero, and unchecked derivations are now common in preprints, forums and course material. The startup is not building a stronger generator; it is betting on the checking side.

Formal verification works by translating an argument into a machine-checkable formal language and having a kernel validate each inference step. Skipped premises, citations to lemmas that do not exist, and special cases passed off as general ones surface immediately at that layer. Fluent prose cannot carry them through.

From an engineering standpoint, moving a library of this size into a formal environment is hard not because of any single theorem but because of the dependency graph: nearly every result rests on a large base of prior definitions and lemmas, and a single gap breaks the chain above it. Agents are well suited to this kind of high-volume labour, which requires tracking references across many files.

If verification can be scaled, what changes is not only paper quality but the production process of mathematical knowledge. A machine-checkable proof library means results can be searched, reused and built upon directly, without requiring the reader to trust the author.

There is also reason for restraint. Public information so far centres on the claim of completion; coverage, runtime, the number of failing entries and a reproducible public log have not been detailed, and readers should not infer that the entire library has been fully formalized.

Three things to watch: whether Axiom Math opens a re-runnable verification pipeline, whether third parties can independently reproduce the result, and whether formal verification is accepted as a standard step in mathematical publishing. The third is the hardest and will most determine where a company like this ends up.