主要证据
- Chinese Academy of Sciences retrospective on Wen-Tsun Wu and Wu's methodS2 · 官方机构来源 · 官方公告 · 2024-06-21
- Wen-Tsun Wu memorial bibliography — mathematics mechanization papersS2 · 官方机构来源 · 官方公告 · 2019-04-30
吴文俊验证后来被称为“吴方法”的几何定理机器证明代数方法
该方法把初等几何代数化：将几何构型编码为多项式方程，并把定理证明转化为符号多项式推理。吴文俊在 Ritt 特征列思想与构造性消元基础上发展出机械化证明路线，并能显式处理退化情形。后续计算机实现证明了多项非平凡几何定理，使代数式自动几何推理成为长期研究方向。
发生了什么？
中国科学院的回顾性资料记载，经过数月手算后，吴文俊于 1977 年农历大年初一首次成功验证初等几何定理机械化证明方法的可行性；1977 年官方节假日档案独立确认当年农历新年首日为公历 2 月 18 日。吴文俊随后于同年在《中国科学》20 卷第 6 期 507–516 页发表奠基性中文论文，英文版于 1978 年发表。
为什么重要？
该事件补上了 Chronicle 中从 Gelernter 早期启发式 Geometry Theorem Machine 到后来成熟符号代数自动演绎路线之间的重要桥梁。它也体现了一种关键的历史 AI4Math 形态：核心创新并非学习模型，而是把一类证明任务转化为可机械执行过程的数学算法。
重要性说明：吴方法把自动几何定理证明从以启发式搜索为主的路线推进到代数化、算法化路线：将几何条件与结论转写为多项式条件，再利用特征列与消元技术处理。CADE 后来将吴文俊的工作明确评价为几何定理证明中的奠基性贡献，其 Herbrand Award 记录也将该方法视为重新推动自动几何定理证明的重要突破。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 尚属声明
- 证据等级
- E2 · 研究记录
- AI 角色
- 仅计算支持
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 新算法
- 接口
- 符号
- AI 贡献
- 核心贡献是由人类设计、面向机械推理的算法。吴文俊先以手算验证过程可行，后续实现再由计算机执行代数证明程序；本记录不把数学发现归因于自主 AI 系统。
- 人类贡献
- 吴文俊提出几何代数化路线，发展构造性多项式方法，以手算检验其可行性，并随后推动计算机实现及更广泛的数学机械化研究计划。
- 验证状态
- 尚属声明 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- —
- 机构
- chinese-academy-of-sciences
- 数学问题
- euclidean-geometry-theorem-proving
- 方法
- characteristic-set-method, polynomial-elimination, symbolic-reasoning, automated-deduction
全部来源与工件
- Chinese Academy of Sciences retrospective on Wen-Tsun Wu and Wu's methodS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-15
- Hong Kong Government Information Services — General Holidays for 1977S2 · 官方机构来源 · 其他来源 · 访问于 2026-09-15
- Wen-Tsun Wu memorial bibliography — mathematics mechanization papersS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-15
- CADE Herbrand Award — Wen-Tsun Wu (1997)S2 · 官方机构来源 · 官方公告 · 访问于 2026-09-15
- 1997 Herbrand Award citation for Wen-Tsun WuS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-15
验证历史
- 1977-02-18 · 尚属声明 · E2 · 研究记录
中国科学院回顾性资料把吴文俊首次成功手算验证定在 1977 年农历大年初一；1977 年官方节假日档案独立确认该日为公历 2 月 18 日。本记录不从只有期号精度的期刊元数据推断后续论文的具体出版日。
更正
当前没有记录的更正。