陶哲轩在2026年ICM提出“证明消化不良”：AI时代数学面临审核瓶颈

在2026年国际数学家大会（ICM）上，菲尔兹奖得主陶哲轩发表演讲《AI时代的数学》，提出“证明消化不良”概念：AI生成证明的速度已远超人类审核验证的速度，数学正从“证明稀缺”进入“证明过剩”时代。

陶哲轩指出，AI能以“日更”速度批量产出证明，但人类数学家无法及时核实，大量提交的AI证明可能正确却无人验证。他以黎曼零点比例问题为例，人类数学家三十多年仅推进1.6%，AI在一天半内推进25.6%。AI解难题的真实成功率仅1%—2%，且错误可以藏得很深，判断一个证明是否成立有时需花费数天。

为此，陶哲轩提出新的发表准则：如果作者无法以专家水平清晰解释其结果，即使证明已通过Lean等工具的正式验证，也不应发表。“消化”比证明更重要。他亲自示范，将AI产出的森多夫猜想证明从9万行Lean形式化代码整理为1.5万行，并发现一个更强命题，连带解决了1972年的菲尔普斯-罗德里格斯猜想。他认为，人类在阅读艰深论文时的停顿、补全与重新推导，正是建立真正数学理解的必经之路。

陶哲轩的演讲引发对AI与数学关系的重新思考：AI可当“向导”，人类负责“寻宝”，把AI产出的核心中间步骤提炼出来重新理解。