7月下旬，在费城举行的国际数学家大会上，陶哲轩描述了一种以前没有过的情况：一项重要结果已经被证明，验证也通过了，却没人能解释这份证明为什么成立，更没办法把它讲清楚、让其他数学家读懂、复用、传下去。 数学界还没真正走到这一步。但要走到那里所需要的技术，已经一项项出现了。AI开始参与文献搜索、构造例子、补齐推导，甚至生成新的证明和反例；形式化工具又能检查其中一部分结果是否正确。生成证明、验证证明、理解证明，开始由不同的人和工具来做，快慢也不同。 这种变化在大会上引发了明显分歧。刚获得菲尔兹奖的雅各布·齐默尔…