文章摘要
【关 键 词】 数学挑战、AI工具、众包项目、证明辅助、数学探索
陶哲轩，一位著名的数学家，最近发起了一项挑战，旨在探索是否可以利用AI和众包的方式扩展数学问题的证明范围。他提出了一个项目，使用Lean4证明辅助语言来形式化多项式Freiman-Ruzsa猜想，并在三周内取得了成功。这个项目的成功展示了AI工具在数学研究中的潜力，尤其是在验证和分解复杂数学问题方面。
传统的数学研究通常由少数专家完成，但陶哲轩认为，通过将项目分解成小模块，可以让更多的人参与进来。他提到了众包项目“Polymath”作为例子，该项目没有使用证明辅助语言，限制了其规模。现在，他希望结合证明辅助语言来突破这一限制。
陶哲轩还提出了一种新范式，不仅用于形式化现有的数学，还可以用来探索新的数学问题。他提出了一个泛代数领域的项目，涉及对原群的等式理论的中等规模探索。原群是一个简单的数学结构，可以通过添加额外的公理来得到更复杂的结构，如群、半群或幺半群。陶哲轩介绍了十一个关于原群的等式公理的例子，并探讨了这些公理之间的推导关系。
这个新项目的目标是探索等式公理之间的推导关系，特别是那些能够推导出其他公理的公理。陶哲轩特别关注是否存在介于常数公理和结合律公理之间的等式公理。他通过哈斯图（Hasse diagram）描述了这些公理之间的完整推导关系，并回答了MathOverflow上的一个问题。
此外，陶哲轩还提到了“忙碌海狸挑战”和“互联网梅森素数大搜索”（GIMPS）等众包计算项目，这些项目在精神上与他的新项目相似，尽管它们使用的是更传统的工作量证明机制，而不是证明辅助语言。
总的来说，陶哲轩的项目展示了AI和众包在数学研究中的潜力，尤其是在验证和分解复杂数学问题方面。通过结合证明辅助语言和众包，他希望能够探索新的数学问题，并克服传统研究方法的限制。
原文和模型
【原文链接】 阅读原文 [ 1849字 | 8分钟 ]
【原文作者】 新智元
【摘要模型】 moonshot-v1-32k
【摘要评分】 ★★★★☆
