陶哲轩众包数学项目完成度99.99%：仍未看到AI工具的重大贡献

文章预览

机器之心编译 编辑：杜伟 陶哲轩发起的「众包」数学研究项目终于快要迎来胜利时刻！ 大约在三周前，陶哲轩提出了一个众包项目，结合专业和业余数学家、自动定理证明器、AI 工具和证明辅助语言 Lean， 来描述与 4694 条 magma（原群） 方程定律相关的蕴含图，这些定律可以使用最多四次 magma 操作调用来表达。也即，需要确定这 4694 条定律之间可能蕴含的 的真假。 该项目已运行 19 天， 从已解决的原始蕴含的角度来看，该项目（截至撰写本文）已完成 99.9963% ：待解决的 蕴含中， 已被证明为真， 已被证明为假，只有 悬而未决。尽管在这个集合中，也有 蕴含推测为假，但可能很快就正式反驳。 出于编译效率的原因，他们没有在 Lean 中记录这些推测中的每一个证明；只在 Lean 中证明一组较小的蕴含 ，然后通过传递性来暗示一组更广泛的蕴含（例 ………………………………