How to Formalize All of Mathematics
Xena ● Covered by 2 sources
Guest mathematicians Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, and Adam Topaz argue for careful formalizing of mathematics with AI after noting recent successes and failures in AI-assisted theorem proving. They cite Anthropic’s claim that Claude verified Fermat’s Last Theorem using 13 million lines of code over 11 days. They warn that poorly used, under-maintained formal “dumps” will waste resources and damage norms, and instead push for scaled, community-vetted libraries and workflows (e.g., Mathlib and other projects) that people can build on.
Why it matters
It would be a “terrible waste of resources” to formalize mathematics results in libraries nobody uses, because it could disincentivize good research. Several projects are working to ensure formal libraries fulfill real community goals, and within a few years most mathematics could be formalized for exploration and building.