陶哲轩利用AI推进方程理论验证，项目进度达99.99%
著名数学家陶哲轩最近发起了一个项目，旨在利用AI工具和证明辅助语言Lean来描述与4694条幺半群方程定理定理相关的蕴含图。这个项目自9月25日启动以来，已经取得了显著进展，目前完成度已达99.9963%。在需要解决的22028942个蕴含关系中，已有8178279个被证明为真，13854531个被证明为假，仅有826个关系尚未解决。陶哲轩通过众包方式，结合专业和业余数学家的努力，以及自动定理证明器的支持，探索了数学的新领域。这一成就展示了AI在数学研究中的潜力，尤其是在辅助数学家解决复杂问题方面。项目的成功不仅在于技术的应用，还在于它如何将人类专家的智慧与AI工具的力量结合起来，以前所未有的速度推进数学理论的发展。
