2026 年 4 月，中国一支研究团队报告称，他们让一种源自 20 世纪 70 年代的几何定理证明方法接受现代证明助理的检验。Lean 4 面对的任务落在方法的代数底层，奥数图形识别、辅助线构造与优美证明写作都在此次工作范围之外。团队将吴文俊方法中的多项式序、伪除法、特征列和零点分解形式化，再用 Lean 核验相关过程的终止性与正确性。[2]

这项成果闭合了一段耐人寻味的历史回路。吴方法原本就是要把部分几何推理变成机械程序；近五十年后，程序的数学核心也得到了机器核验。

这是一项有分量的数学 AI 用例，范围却比“AI 证明几何”这类标题所暗示的更窄。新成果认证的是基础层。端到端链条仍缺三段：能够在 Lean 中实际运行的几何引擎、把自然语言问题转写为方程的前端，以及把代数证书还原成学生熟悉的证明。它的重要性，在于让这些衔接环节彼此分明，也让概念混用更难发生。

题图是一张吴文俊在个人计算机旁工作的档案照片。数学与系统科学研究院（AMSS）的页面既未注明拍摄日期，也没有说明照片中的机器是哪一套系统，因此照片呈现的是这位数学家的计算工作环境，无法对应到某一次具体的定理证明运行。[7]

最初的转向：从图形搜索转入代数计算

吴文俊把这项发现的时间定在 1976 年末至 1977 年初。他在 1986 年发表的论述中，介绍了一种适用于若干类初等几何的机械化方法，理论基础来自 J. F. Ritt 的工作，以及多项式排序和代数簇理论。[1] 中国科学院托管的一篇通俗历史文章给出了实际步骤：引入数与坐标，把几何题的条件和结论转写为代数关系，按规定次序排列这些关系，随后运行确定性的消元程序，判定结论能否由条件推出。[3]

任务的性质由此改变。综合几何证明常常依赖恰当的构造：延长一条边、作一个圆、发现两个角之间的关系。吴文俊的代数路线绕开了对这种几何灵光的复刻，改换表示方式，直到证明成为多项式计算。

简化来看，题设条件变成一组多元多项式方程，结论则变成另一项多项式条件。方法先把题设组织成三角列或升列形式，随后反复计算伪余式。在相关非零条件成立时，余式为零可以认证结论；零点分解则把解集拆成若干分支，同时处理首项系数（initials）为零的位置。[2]

这些条件远远超出记账细节。它们会标出退化情形：设想中的三角形塌缩为一条直线，交点构造失去唯一性，或推出结论所需的约分条件不再成立。机械化证明的价值，正在于它必须揭示手绘图形可以悄然掩去的假设。

这套方法也有明确的适用范围。吴文俊的原始摘要指出，它适用于满足帕斯卡公理的各种无序初等几何，也适用于不含次序概念的某些几何定理，例如不讨论一点位于另外两点“之间”的命题。[1] 这套程序处理可代数化陈述的能力很强，覆盖范围止于此，无法包办每一种几何论证。

Lean 4 在 2026 年核验了什么

Yuxuan Xiao、Hao Shen、Junyu Guo、Dingkang Wang 和 Lihong Zhi 于 2026 年 4 月 16 日提交的论文在 Lean 4 中形式化了吴—Ritt 特征列方法。团队多数成员隶属于中国科学院数学与系统科学研究院及中国科学院大学，这项工作建立在 Lean 的 Mathlib 代数基础设施之上。[2]

核验范围相当广。形式化内容包括多项式的首项系数与序；单个多项式和三角列的伪除法与伪余式；标准升列与弱升列；基本集、特征列和零点分解算法；以及相关程序终止并满足既定正确性性质的证明。[2]

核心对象是特征列：一组按序排列的多项式，用于把原多项式组约化为适合消元的形式。形式化工作以良序原理连接原系统与特征列，继而核验零点分解的集合论表述：避开各三角列首项系数的零点后，原零点集可以表示为与这些三角列对应的有限个零点集之并。[2]

最后这项限定，正是“不能约去一个取值为零的因子”的形式化版本。一般情形与退化情形从这里分开。定义、算法、终止性论证和集合论命题被置于同一个受检验环境中，代码暗中借用定理陈述之外条件的风险也随之降低。

此前已经有过相关形式化工作：作者提到，Coq 曾为几何定理证明形式化吴方法的一个简化版本。此次论文所称的新增部分，是在 Lean 4 中对特征列方法作全面处理，并纳入零点分解装置。[2] 因此，证明助理技术早已接触吴文俊的思想；2026 年这项工作则在如今居于 AI 辅助形式数学核心位置的一套证明体系中，完成了范围更广的重构。

认证距离实际运行还有一段链条

2026 年论文中力度最强的一句话，范围也界定得很谨慎：这项工作为经过认证的多项式组求解和几何定理证明奠定了基础。[2] 从基础到端到端应用，中间仍隔着若干环节。

作者把抽取实际运行代码列为未来工作，同时还计划扩展到微分多项式；公开代码库也把这套形式化标为开发中项目。[2][6] 当前成果因而仍处在形式化认证层，尚不能称为从 Lean 生成的生产级求解器。在已验证核心之前，还缺少一个前端，用来读取非形式化几何问题、选择坐标、生成题设多项式，并核对图形与代数编码表达的是同一件事。

核心之后还有一次衔接。代数消元轨迹可以严谨，却很少呈现综合证明中便于教学的视觉关系，例如相似三角形、圆内接四边形和角关系。它能认证结论由条件推出，却未必给出解释。Lean 形式化核验的是方法的数学装置，形式化本身尚未把所得论证转成易于人读的证明。

对于当代 AI 系统，这项区别十分重要。语言模型可以提出形式陈述或构造，符号引擎可以完成代数证明义务，证明助理可以核验证书。可靠性取决于清楚划分这些角色的职责，把整条流水线统称为“推理”不能替代这种划分。2026 年的工作加固了中间一层，也就是把多项式的排列关系转成经认证分解的部分。

2024 年的一项基准测试说明这台老引擎为何仍有价值

吴方法此次回归，也不只为了历史保存。2024 年，另一支研究团队在 IMO-AG-30 上重新检验这套方法。这个基准集包含 30 道国际数学奥林匹克竞赛（IMO）几何题，并把它们改写到范围较窄的形式语言中。基准集的原作者估算，这种语言可以表示 2000 至 2022 年 IMO 几何题中的约 75%；不等式和组合几何超出了表达范围。[5] 后来的研究者使用 JGEX 软件，报告吴方法解出了 15 道题，其中包括 AlphaGeometry 未能解出的 5 道题中的 2 道。把吴方法与经典演绎数据库以及角、比率、距离规则的成功案例合并，可覆盖 21 道题；把吴方法与 AlphaGeometry 的成功案例合并，则覆盖 27 道。[4]

两者的互补性，比这些数量引出的奖牌类比更值得关注。神经方法或综合方法会搜索构造与熟悉几何事实组成的推理链，吴方法则直接求取代数后果。两类系统的失败集合可以错开，因此，一套较早的确定性方法仍能为新模型增加覆盖率。

评估范围同样需要看清。2024 年论文的作者手工把基准题转写为 JGEX 兼容形式，其中 4 道题因为软件缺少所需构造而无法转写，所以吴方法的结果基于其余 26 道可转写题目。在一台配备 AMD Ryzen 7 5800H 和 16 GB 内存的笔记本电脑上，15 个成功案例中有 14 个在 5 秒内完成，另一个耗时 3 分钟；失败运行中也会遇到在 5 分钟时限内耗尽内存的情形。[4]

论文将这项研究标为仍在推进中的工作，并把现成程序稀少、可用构造有限、性能欠佳和证明难以人读列为有待解决的弱点。[4] 它所用的软件路线也与 2026 年的 Lean 形式化不同。Lean 论文没有复现 IMO-AG-30 的结果，Lean 新增的正确性保证也没有延伸到基准论文。两项成果合读，可以看到一项衔接机会，完整集成仍未完成：一条研究路线表明吴文俊的代数方法仍能为现代推理前沿增加能力，另一条路线开始让它的数学核心接受认证。

这个用例的成果是一层经过验证的中间层

眼下得到的是一套更严谨的形式几何架构，距离“上传任意图形，得到优美证明”仍有很长的链条。

上游系统先要正确表达几何构造。经过验证的吴—Ritt 层随后可以约化并分解所得多项式组，为已经形式化的算法提供机器核验保证。下游系统则要完整保留非退化条件，并展示代数证书或重建可读的几何解释。每一次衔接都需要单独测试。

接下来值得关注的证据很具体：从 Lean 抽取实际运行代码；建立一条有文档说明的几何陈述到多项式转换通道；在基准运行中完整记录题目覆盖率和资源测量数据；给出可以独立重放的证书；重建证明时保留消元发现的例外情形。上述环节补齐之前，“经认证的几何证明器”仍是一条架构方向，尚未成为已交付的系统。

吴文俊的持久贡献，在于找到一种表示，让一类证明能够成为程序。这条路线绕开了让机器模仿数学家凝视图形的要求。2026 年的形式化把同一种严谨再向下推进一层，追问程序本身的表述是否已经精确到足以由另一台机器核验。

对数学 AI 而言，这才是有用的信号。能力可以来自学习式搜索、符号消元和形式验证的结合；信任则来自清楚知道哪一层提供了哪一项主张，以及证明究竟停在哪里。

来源

1. Wu Wen-Tsun, “Basic Principles of Mechanical Theorem Proving in Elementary Geometries,” Journal of Automated Reasoning 2 (1986), 221–252——原始适用范围、数学基础和计算机运行示例。
2. Yuxuan Xiao, Hao Shen, Junyu Guo, Dingkang Wang, and Lihong Zhi, “Formalizing Wu-Ritt Method in Lean 4”（提交于 2026 年 4 月 16 日）——形式化组成、终止性与正确性结果、作者隶属机构及未来工作范围。
3. Lai Mingdong and Yong Xi, “Wu Wenjun: New ideas for artificial intelligence? They can be found in ancient Chinese mathematical thought,” 中国科学院计算机网络信息中心（2021 年 6 月 29 日；中文）——由中国科学院托管的通俗方法史，以及从几何到代数的三阶段步骤。
4. Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat, and Matthias Bethge, “Wu’s Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry”（修订于 2024 年 4 月 11 日）——IMO-AG-30 结果、硬件、手工转写、软件局限和开发中状态。
5. Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong, “Solving Olympiad Geometry without Human Demonstrations,” Nature 625 (2024)——IMO-AG-30 的原始构建、表示范围和 AlphaGeometry 评估。
6. WuProver, “Lean Characteristic Set”——公开的 Lean 4 形式化代码库及开发中状态。
7. 中国科学院数学与系统科学研究院，“Wu Wenjun at work”（档案照片页面，发布于 2019 年 4 月 30 日；中文）。