在最近的一次演讲中，数学家陶哲轩表示，AI 已经被用于自动化数学证明，并且能够辅助数学实验的证明过程，提高验证的效率和准确性。他特别提到，形式化证明工具与 AI 工具的结合可以加速数学定理的形式化验证过程。陶哲轩举例说明，验证期间 AI 可以自动填充证明中的小步骤，保证准确性，并实现大规模协作。
在今年的国际数学奥林匹克竞赛（IMO）上，谷歌 DeepMind 的 AI 系统 AlphaProof 和 AlphaGeometry 2 取得了成绩。这一混合 AI 系统在六道赛题中做对了四道，获得了 28 分，达到了银牌水平。AlphaProof 是一种用于形式化数学推理的强化学习系统，而 AlphaGeometry 2 是 DeepMind 几何求解系统的改进版本。
陶哲轩在自己的博客上对 DeepMind 的 AI 系统参加 IMO 竞赛表达了看法。他认为这是一个重要的工作，改变了我们对哪些基准挑战可以通过 AI 辅助或完全自主的方法实现的期望。例如，IMO 级别的几何问题现在对于专用的 AI 工具来说已基本解决。通过强化学习过程可以找到形式化证明的 IMO 问题至少在某种程度上可以被 AI 攻克。虽然目前每个问题需要相当大的计算量，并且在形式化方面需要人类的帮助，但这一成就无疑是 AI 在数学领域的一大进步。
AI 在数学领域的应用正在逐步展开，并取得了成果。陶哲轩的演讲和谷歌 DeepMind 的 AlphaProof 在 IMO 竞赛中的表现，展示了 AI 在数学证明和推理中的潜力。