(这是一篇客座文章，由杰里米·阿维戈德、凯文·巴扎德、约翰·科梅林、雷米·德根、金·莫里森、奥利弗·纳什和亚当·托帕兹撰写。) 数学家们对上周OpenAI的大规模发布反应各异，从兴奋到沮丧，但有一件事是明确的：人工智能在形式化和非形式化地证明定理方面表现得相当出色。形式领域的成功使得人工智能的爱好者宣称，现在是将整个数学形式化以留给未来世代的最佳时机。我们对此提案表示理解。我们认识到新技术在数学推理中的力量，并欣赏它们能为我们熟知和喜爱的学科贡献的内容。我们对人工智能所能发挥的作用总体上持乐观态度，但我们对一些最近提出的尽快形式化一切的呼声深感忧虑。如果做得好，大规模、协调的形式化努力可能会极大地扩展数学探索和发现。如果做得不好，充其量也只是资源的浪费；更有可能，这是会造成持久的损害。我们希望看到良好的形式化。因此，这篇文章阐明了我们的担忧，描述了我们与人工智能和形式化相关的一些经历，并提供了一个积极的愿景，展望如何让我们所有人共同努力，朝着一个几乎所有数学定义、定理和证明拥有形式表达，并且这些成果能够促进数学蓬勃发展的世界迈进。正如人工智能在数学中的作用如今是一个棘手的话题一样，它在形式化中的作用也是如此。专家形式化者对人工智能的态度范围与更广泛的数学家群体的态度一样广泛。我们意识到，一些我们亲密的朋友和同事，对他们的观点我们高度重视和尊重，坚决反对使用人工智能进行大规模的形式化。我们在此所说的任何内容都不应被视为代表我们所关联的任何组织或社区的观点。关切事项让我们先观察一个现象：如果没有人使用，形式化成果的价值便微乎其微。当Math, Inc.去年二月试图劫持一个项目，以形式化玛丽娜·维亚佐夫斯卡的高维球体包装结果时，它展示了该技术能做什么，但除此之外，对数学并没有任何贡献。原项目组继续准备这个八维结果的高质量形式化，并很快发现清理人工智能生成的代码比它值得的麻烦要多；结果发现，抛弃这些代码，再加上人工智能的充分帮助，直接重新进行会更好。当Anthropic宣布Claude已经用1200万行代码在11天内正式验证了费尔马最后定理时，凯文·巴扎德愉快地赞扬了这个成果，同时也宣称他没有意图终止他正在进行的更现代的证明的形式化。再一次，尽管这一成就令人印象深刻，这段人工智能生成的代码可能几乎没有持续的价值。这到底是怎么回事？定理并没有遭到严重质疑，因此，形式化成果的价值完全在于我们所获得的超越简单正确性的东西。我们希望形式化一切，因为我们希望利用这些形式化来做更多数学，并比没有它们时做得更好。我们希望考虑可能的推广，探索不同数学分支之间的联系，以及考虑意想不到的应用。我们希望重构和改善我们的知识：手动形式化的乐趣部分在于意识到我们可以调整我们的概念，使其更优雅、更高效，并更适合我们的目的。知识在未能促进我们理解之前是没有价值的；形式化的价值来自于我们与数据的使用和互动。当OpenAI宣布关于纳维-斯托克斯方程的解在有限时间内失效时，自然语言证明伴随着一个Lean形式化。与之前的例子相比，正确性信号在这里 played 起了关键作用：现在几乎没有怀疑该解是正确的，尽管自然语言证明大部分是难以理解的。尽管如此，OpenAI还是因如何获得结果、创意的来源和信用，以及担忧专注于正确性会阻碍千禧年奖旨在促进的探索和理解而引起了数学界的愤怒。所以，即使在这里，毫无修饰的形式化成果也是一把双刃剑。OpenAI后来的数据包含了令人惊讶和重要的数学，同时也显示出对读者和理解构建的显著漠视（一些结果已经被撤回，许多非形式/形式对在微妙或显著方面相互分歧，大多数非正式写作难以穿透）。这解释了我们的担忧。如果花费数百万美元去形式化数学结果于事无补，那么……