陶哲轩众包数学项目：99.99% 完成，AI 贡献有限
著名数学家陶哲轩发起的“众包”数学研究项目已接近尾声，该项目旨在确定 4694 条 magma（原群）方程定律之间的蕴含关系。经过 19 天的努力，项目已完成 99.9963%，但 AI 工具的贡献却远不如预期。
该项目汇集了专业和业余数学家、自动定理证明器、AI 工具和证明辅助语言 Lean，目标是构建一个描述这些方程定律之间蕴含关系的图。项目参与者需要确定 4694 条定律之间可能存在的蕴含关系，并证明其真假。
项目进展喜人，但 AI 贡献有限
截至目前，项目已解决 99.9963% 的原始蕴含关系，剩余的少量关系中，一些已被证明为真，一些已被证明为假，只有少数悬而未决。尽管 AI 工具在项目中发挥了一定作用，例如加速编写 Lean 证明和 LaTex 蓝图，但对于解决核心任务——证明蕴含关系，更“老式”的自动定理证明器表现更为出色。
项目成果：新发现和新技术
尽管 AI 的贡献有限，但该项目仍取得了显著成果。研究人员发现了新的证明技术和构造方法，用于证明给定的方程理论并不蕴含另一个方程理论。此外，他们还发现了奇特的代数结构，例如“Asterix”和“Oberlix”，这些结构具有独特的特征，在其他研究中可能无法被发现。
人类与 AI 的协同合作
项目参与者来自各个领域，包括各个职业阶段的数学家和计算机科学家、学生和业余爱好者。Lean 平台在整合人类生成和机器生成的贡献方面发挥了重要作用，但许多自动生成的成果最初由人类在特定情况下获得，然后被泛化和形式化。
未来展望：AI 的潜力
尽管 AI 工具在该项目中的贡献有限，但陶哲轩认为 AI 在未来可能发挥更重要的作用。他期待 AI 工具能够在更复杂的数学问题中发挥更大作用，例如解决更难的蕴含关系或发现新的数学结构。
该项目证明了人类与 AI 协同合作的巨大潜力，也为未来数学研究提供了新的思路。尽管 AI 工具尚未在数学研究中发挥决定性作用，但其潜力不容忽视。随着 AI 技术的不断发展，我们可以期待 AI 在数学研究中发挥越来越重要的作用。
参考文献：
注： 本文参考了机器之心网站的报道，并加入了个人观点和分析。
Views: 0