数学家 Daniel Litt 去年三月打赌，他认为 AI 只有四分之一的概率到 2030 年能写出人类顶级数学家水平的论文。但一年之后他认为这个赌自己要输了。AI 解决问题和产生证明的能力进步之快令数学家倍感震惊。几年前它们甚至无法解决高中数学题，如今它们常常能解决数学家都感到棘手的难题。AI 开始挑战更复杂的数学问题，解决实际的研究问题，帮助自动验证前沿的数学证明——而验证这些证明通常需要数学家团队付出大量努力。AI 生成证明的速度比人类验证证明快得多，因此如果一个定理是由 AI 证明但没有人类去验证，那么它是否真的被证明了？AI 在这方面也能提供帮助。名为形式化的过程可以将自然语言证明翻译到计算机可验证格式。AI 公司 Math, Inc 最近宣布它的工具 Gauss 形式化了 2022 年菲尔茨奖得主 Maryna Viazovska 的得奖证明。证明代码大约有 20 万行。手工计算曾是数学家工作的重要组成部分，但如今这些都已自动化。AI 的进展也可能改变今天的数学。