2025年9月，一款名为Gauss的AI工具引发关注。它仅用三周时间完成了数学家陶哲轩和Alex Kontorovich耗时18个月尚未完全解决的挑战——在Lean中形式化强素数定理（PNT）。Gauss由AI公司Math开发，是首个可协助顶级数学家进行自动形式化的Agent，能将人类数学内容转换为机器可验证的形式语言。其生成了约25000行Lean代码，包含上千个定理，大幅缩短了传统需多年完成的工作。陶哲轩对此表示，AI工具虽然高效，但可能忽略项目中的隐含目标，因此项目组织者需更明确地阐述所有目标。Math公司创始人Christian Szegedy曾因提出Batch Normalization技术获ICML时间检验奖，推动了深度学习发展。网友对Gauss的技术细节充满期待，但官方尚未发布具体技术报告。