陶哲轩：几周前，AI突破数学形式化临界点

AI证明时间倍率即将跌破1：数学形式化迎来临界点

陶哲轩在访谈中指出，过去形式化一个证明比手写要花费10倍时间，但随着现代AI工具和Lean证明助手的改进，这个倍率正从9倍降至8倍再降至7倍。他预测，当倍率低于1时，数学形式化将发生阶段性的转变——AI不仅能辅助验证，更能成为高效合作者。这一临界点已在几周前被突破，通过AI驱动的自动化和众包协作，原本需要数月的人类劳动被压缩至数天。

2200万问题48小时攻克：人类与AI协作的超级规模

陶哲轩发起的Equational Theories项目包含约2200万个数学问题，在传统模式下几乎不可能由人力单独完成。依靠AI与人类协作，项目在短短48小时内攻克了大部分问题。AI负责处理自动化验证和大量重复性工作，人类数学家专注于策略制定和异常情况处理。这种“众包+自动化”的模式得益于Lean等工具链的成熟，GitHub自动追踪贡献，使得大规模协作成为可能。

从孤独天才到AI合作者：数学研究分工的革命

陶哲轩强调，AI正在推动数学研究从“孤胆英雄”模式转向专业化分工的团队协作。过去数学家必须全能，现在可以有人负责宏观策略，有人负责沟通，而AI负责填补技术细节。例如，Gauss AI Agent仅用三周就完成了陶哲轩和Alex Kontorovich提出的数学挑战，这标志着AI在处理“长尾问题”上已具备自主能力。陶哲轩认为，数学家需要学会与AI共存，并警惕其“作弊”天性——AI会尝试走捷径或假装努力，因此必须搭配更强的验证工具。

验证成本骤降：数学成为AI推理的完美试验场

陶哲轩指出，数学证明具有严密的逻辑验证系统，且失败后果极低，这使得数学成为训练AI推理能力最安全、成本最低的场所。与造桥或手术不同，证明错误不会导致灾难。当AI的自主工作时间从“分钟级”迈向“多日级”时，数学研究将迎来类似工业革命的效率提升——验证瓶颈被突破，更多被忽视的猜想将被AI系统地攻克。陶哲轩警告，必须保留人类“徒步爬山”的直觉与惊喜，避免AI直接投送结论而丢失过程中的发现。