如果从传统数学史看，数学的发展可以讲成代数、几何、分析、概率、拓扑、逻辑不断分化又统一。但如果从计算机和 AI4Math 看，近十年的主线更像一部数据集形态变化史。
一开始，AI 做数学主要是在回答题：给出最终答案，算 exact match。后来，数据集开始要求模型写过程、生成多条解法、接受 verifier 打分、调用代码执行器、进入 Lean/Coq/Isabelle 这样的 proof assistant，最后又发展出 live leaderboard、去污染评测、研究级问题和提交制 formalization 平台。
换句话说，前沿不只是“模型更会做题了”，而是数学数据集本身从静态题库变成了可执行、可验证、可审计、可持续更新的数学工作流。
这几年 AI 研究的节奏明显变了：模型能力、工具链、论文、开源项目、benchmark 和应用场景都在高速迭代。很多过去需要专家慢慢写、慢慢查的东西，现在可以由模型在几分钟内生成一个看起来很像样的版本：代码、实验计划、定理证明草稿、综述、数据分析、系统设计，甚至新的 conjecture。
这当然是巨大的生产力提升。但它也带来一个更尖锐的问题：当生成速度远远超过人工验证速度时，我们到底靠什么维持可信度？
形式化的重要性，正是在这个背景下突然变得现实起来。
2026 年 7 月，ICM 在费城开会时，AI 已经不再只是数学大会外围的技术展示。Terence Tao 谈“AI 时代的数学”，Alex Kontorovich 谈数学的未来形态，会场还把 Mathematics for AI 和 AI for Mathematics 拆成两场方向相反的圆桌。
几乎在同一时间，另一批更具体的变化正在发生：开放猜想被整理成 Lean 语句，真实数学仓库中的 sorry 被做成动态 benchmark，最新 arXiv 论文里的 lemma 被实时抽取，模型也开始参与形成研究预印本。
但“AI 已经开始解决开放猜想”这句话仍然需要拆开。它可能指奥赛题，可能指把已知证明翻译成 Lean，可能指找到一个更好的有限构造，也可能真的指一个此前未知的数学结论。这四件事的证据强度完全不同。
2026 年 7 月 28 日，Lean Zulip 的 lean4 stream 出现了一个很难忽略的 topic：Counterexample to the Lean Conjecture (Soundness Bug)。
帖子里的三个事实放在一起，几乎像一道故意设计的判断题：
sorry，#print axioms 没暴露隐藏公理，当时的 comparator.live 和旧版 nanoda 都接受了它。False。这不是“形式化验证忽然失效”的故事，也不是一个模型真的完成了世纪数学突破。它更具体，也更值得研究：一份 proof artifact 把 Lean 官方 kernel 的漏检 与 旧版 nanoda 的另一处漏检 拼在一起，恰好穿过了两套原本彼此独立的检查。