Maryna Viazovska and Kevin Buzzard, Veritas Fellows for mathematics at planetary scale

Math, Inc. is launching the inaugural Veritas program to build out the tools and methodology for formal mathematics at unprecedented scale. Renowned professor Kevin Buzzard, alongside Fields medalists Maryna Viazovska and Terence Tao, join as Veritas Fellows to lead the effort's defining projects.

The program centers on two landmark formalizations — Fermat's Last Theorem and the universal optimality of the Leech lattice — chosen not only for their mathematical depth but for their capacity to stress-test the infrastructure that a fully formalized discipline will require.

The bottleneck has shifted

For most of its history, formalizing mathematics has been bottlenecked by production. Translating a single research paper into verified Lean code required months of expert labor. Working collectively for nearly a decade, the formal mathematics community produced Mathlib — a library equivalent to roughly fifty introductory textbooks. A significant achievement, and a small fraction of what is known.

That constraint is dissolving. In June 2025, Math, Inc.'s autoformalization produced 3,500 lines of verified code on a classical result related to the ABC conjecture. By September, using the Gauss agent, the team formalized the Strong Prime Number Theorem in 25,000 lines — completing in three weeks what a crowdsourced effort led by Terence Tao and Alex Kontorovich had pursued for 18 months. In February 2026, Gauss formally verified the optimality of sphere packing in dimensions 8 and 24: 200,000 lines of Lean, again in three weeks. Each result scales by an order of magnitude larger than the last. Each taking the same wall-clock time.

The binding constraint on formal mathematics is no longer producing proofs. It is organizing, integrating, and maintaining the proofs being produced.

From literature to codebase

When a proof is written in Lean, it ceases to be a document and becomes software. Definitions can be imported. Theorems can be invoked as functions. Dependency graphs are explicit, complete, and machine-navigable. The full apparatus of software engineering — version control, continuous integration, automated refactoring, dependency management — becomes available to mathematics for the first time. This observation is precise rather than metaphorical.

But software at scale inherits software's unsolved problems. A library growing by hundreds of thousands of lines per week cannot be maintained by human review. Independently formalized results will use incompatible definitions, duplicate existing work, and accumulate technical debt that renders the library unusable long before it reaches its potential. Without active, automated governance, a rapidly growing codebase fragments into modules that are correct individually but incoherent collectively. The program addresses this directly: building the tooling for redundancy detection, definitional conflict resolution, automated refactoring, and continuous integration adapted to formal mathematics.

The formal mathematics stack is, in this precise sense, the verified software stack developed under controlled conditions.

Frontier grand challenges

The program's lighthouse projects span the landscape of modern mathematics, and each is chosen to surface a distinct engineering challenge.

Fermat's Last Theorem, led by Kevin Buzzard, requires formalizing vast stretches of algebraic number theory, elliptic curves, modular forms, and Galois representations — fields largely absent from any formal library. The core difficulty is structural autoformalization: producing not just proofs that compile but definitions organized so that downstream theory can be built on top of them. Fermat's Last Theorem concentrates this challenge because every definition — automorphic forms, deformation rings, étale cohomology, Shimura varieties — must support not only Wiles's proof but the broader infrastructure that future work across the Langlands program will depend on.

Universal optimality of the Leech lattice, led by Maryna Viazovska, builds directly on the 200,000-line sphere packing codebase. The proof extends Viazovska's Fields Medal work to a far stronger result: the Leech lattice minimizes energy for every completely monotone potential function. This formalization will substantially exceed the sphere packing effort in scale, and its bootstrapping argument will push the limits of autonomous mathematical reasoning — agents constructing auxiliary functions with carefully tuned properties over sustained periods without human intervention.

Together, these projects generate the reusable infrastructure, governance tooling, and institutional knowledge that the broader program requires.

Veritas and beyond

Four research frontiers extend beyond the lighthouse projects. Automated discovery agents will traverse the dependency structure of a planetary-scale library to identify structural connections between distant fields — the kind of unexpected bridges, like those between discrete geometry and harmonic analysis in Viazovska's work, that account for much of how mathematical knowledge compounds. Conjecture generation in a formal setting will allow new hypotheses to be tested for consistency against the entire library and pursued at scale. Library governance will mature into the continuous-integration infrastructure that keeps a codebase of millions of lines coherent. And because the same Lean runtime that checks proofs also checks software specifications, every advance transfers directly to the verification of AI-generated code — an operational problem arriving on the same timeline.

The formalization of individual results will soon become routine. The harder and more consequential work is building the engineering discipline that makes a planetary-scale library viable. That work starts now.

We are proud to welcome Maryna Viazovska and Kevin Buzzard as Veritas Fellows.

Math, Inc.