We are in Washington this week for Organizing Mathematical Knowledge in the Age of AI and Formalization, a two-day meeting at the National Academy of Sciences building convened by the Board on Mathematical Sciences and Analytics. It brings together mathematicians, the formalization and AI communities, and leaders from industry, government and philanthropy. The agenda is about infrastructure, incentives and coordination, and about mathematical knowledge as shared infrastructure for science, engineering and every other domain that depends on reliable reasoning.
The theme that drew our attention was proof distillation.
Mathematics is accelerating. Lean and AI together now settle problems faster than the community can read them. The clearest example is the Equational Theories Project, which produced twenty-two million machine-checked true-or-false results in universal algebra. In March, Terence Tao and Damek Davis launched the SAIR Mathematics Distillation Challenge to compress those results into a cheat sheet of under ten kilobytes that a weaker model, or a person, can actually use, with a second stage that requires Lean proofs rather than answers. The interesting number was not twenty-two million. It was ten kilobytes.
That is the new problem. Call it proof indigestion. A theorem proved by a machine and checked by a kernel is true, but it is not yet knowledge. Knowledge is what a person can find, understand and build on. When proofs arrive faster than they can be read, refereed and folded into the textbooks and libraries of a subject, the bottleneck moves from generation to digestion: exposition, canonical statements, and libraries organized so that the next proof can find the last one.
This is exactly the shape of the problem in software. Tau-prover produces proofs at machine speed. Each one is a certificate, but a pile of certificates is not infrastructure. The work now is to organize what gets proven so that it compounds, which is the same job Mathlib did for mathematics and the reason we are building the equivalent for code.