数学家警告：AI 虽能证定理，但盲目形式化数学恐致资源浪费与长期损害

Mathematicians’ reactions to last week’s big OpenAI release range from excitement to frustration, but one thing is clear: AI has become remarkably good at proving theorems, both formally and informally. The successes in the formal realm have led AI enthusiasts to declare that now is the time to formalize all of mathematics as a legacy for future generations.

We are sympathetic to this proposal. We recognize the power of new technologies for mathematical reasoning and appreciate what they can contribute to the subject we know and love. We are generally optimistic about the role AI can play, but we are deeply concerned by some recent calls to formalize everything as quickly as possible. If done well, a large-scale, coordinated formalization effort could enormously expand mathematical exploration and discovery. Done poorly, it will be, at best, a waste of resources; more likely, it will do lasting damage.

We prefer to see formalization done well. This post therefore clarifies our concerns, describes some of our experiences with AI and formalization, and offers a positive vision of how we can all work toward a world in which all, or almost all, mathematical definitions, theorems, and proofs are equipped with a formal representation, and in which these artifacts help mathematics flourish.

Just as the role of AI in mathematics is a fraught subject these days, so too is its role in formalization. The range of attitudes among expert formalizers toward AI is as wide as the range of attitudes among mathematicians more broadly. We are aware that some of our closest friends and colleagues, whose opinions we value and respect highly, stand strongly opposed to large-scale formalization using AI. Nothing we say here should be taken as representative of the views of any of the organizations or communities with which we are associated.

The concerns

Let’s start with the observation that a formal artifact is not worth much if nobody uses it. When Math, Inc. tried to hijack a project to formalize Maryna Viazovska’s higher-dimensional sphere-packing results last February, it impressively demonstrated what the technology could do, but beyond that, it contributed nothing to mathematics. The original project team kept preparing a quality formalization of the 8-dimensional result and soon discovered that cleaning up the AI-generated code was more trouble than it was worth; it turned out it was better to throw the code away and do it right, still with ample help from AI.

When Anthropi