陶哲轩：AI让数学进入「工业化」时代，数学家也可以是「包工头」

菲尔兹奖得主陶哲轩在访谈中指出，AI 与形式化证明语言（如 Lean）正推动数学研究从“手工业时代”迈向“工业化时代”。传统研究中大量重复性劳动可通过 LLM 辅助自动形式化得以缓解，而 Lean 将证明分解为原子步骤，实现高效协作与快速迭代——例如一项耗时三周的形式化工作可在一天内完成修改。Peter Scholze 的“液态张量实验”将形式化周期从数十年缩短至18个月，凸显进展。陶哲轩预见未来将出现类似软件工程的分工体系，数学家可作为“架构师”领导项目，同时降低参与门槛，吸纳“公民数学家”。此外，形式化能减少对个人学术声誉的信任依赖，建立可验证的协作基础，从而加速整体研究进程。
来源：https://mp.weixin.qq.com/s/wVTRbVtMZX3-WISdtrjbNg