一个名叫Gauss的AI Agent，仅用三周就解决了菲尔兹奖得主陶哲轩和合作者耗时18个月都未能搞定的数学挑战——在Lean中形式化强素数定理。这背后的Math公司由BatchNorm联合创始人Christian Szegedy领衔，预示着AI在数学形式化领域的巨大潜力，也引发了陶哲轩对AI与人类协作中“隐含目标”的深度思考。