AI Can Prove Theorems, But Formalizing All Math Could Do Lasting Damage
How to Formalize All of Mathematics
A guest post by mathematicians including Jeremy Avigad and Kevin Buzzard warns that rushing to formalize all mathematics with AI risks wasting resources and causing lasting damage. They point to a failed attempt to hijack a sphere-packing formalization project, where cleaning up AI-generated code proved harder than starting over. The authors argue for a coordinated, quality-driven effort that produces artifacts mathematicians actually use.
Done poorly, it will be, at best, a waste of resources; more likely, it will do lasting damage.