IXThinker·2025-09-15 16:30

AI Agent三周完成陶哲軒數學挑戰

一個名叫Gauss（高斯）的AI Agent只花三周，便完成數學家陶哲軒與Alex Kontorovich在2024年1月提出的挑戰——在Lean中形式化強素數定理（PNT），而人類團隊此前足足花了十八個月，才取得階段性進展。

十八個月對三周

該挑戰要求在證明助理Lean中完成強素數定理的形式化。陶哲軒與Kontorovich自2024年1月發起，至今年7月花足十八個月才有階段性成果；Gauss接手後僅三周便宣告完成，效率差距令人側目。