陶哲轩隔空对话王虹：数学界该学会消化 AI 了

陶哲轩与王虹就 AI 大量产出数学证明给出几乎相同的判断，数学界需要学习使用并理解消化这些成果。陶哲轩花数天整理一份由 AI 参与完成、经 Lean 验证的森多夫猜想证明，把 Lean 代码从约 9 万行压缩到 1.5 万行，并发现整理后的论证还能覆盖更强的 Phelps–Rodriguez 猜想。他同时公开了登记 Lean 验证结果的 Palomar，该库不宣布结果重要性，也不替代同行评审。