# 数学与形式证明

前沿版本：2026-10-16.1；领域F07

## 概念与例子：AI数学证明为什么需要两种核对

数学证明要说明命题为什么成立。AI可以提出论证或搜索证明，形式化工具则把命题和推理写成机器可检查的语言；两者还需要核对是否表达了同一个数学问题。

把“所有对象”误写成“某些对象”，机器可能严密证明了一个更弱的命题。因此通过Lean检查很有价值，但数学家仍要检查语义、新颖性和研究价值。

- 形式证明：使用严格规则和形式语言表示命题与推理。
- Lean：能够机械检查形式命题及其推理依赖的证明助手。
- 盲审：审阅者在不知道系统身份的情况下判断稿件质量。

## 具体进展

### 竞赛证明从形式系统走向自然语言

IMO是国际数学奥林匹克竞赛。2024年AlphaProof与AlphaGeometry 2解出4/6题、获得28/42分，达到银牌标准，需专家在自然语言和形式语言间翻译，计算时间约2–3天。[2024与2025的官方过程对照](https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/)

2025年advanced Gemini Deep Think研究版本在4.5小时时限内，以自然语言解出5/6题、得35/42分，达到金牌标准。配置使用并行思考、额外强化学习训练、解题数据与提示；不能把成绩转移给任意Gemini产品。IMO确认提交解答，未审查底层模型和整个运行流程。不同年度题目与配置也不能换算成统一增长率。[2024与2025的官方过程对照](https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/)

既有研究报告的事实摘要与条件说明；具体引用在正文标注
对应材料：[2024与2025的官方过程对照](https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/)

### 研究稿件与形式化证书

OpenAI数学仓库发布的是未公开内部模型的研究产物。原报告截至10月12日记载：首发722篇稿件、372个结果族，因符号错误撤回3篇后为719篇、372族；history记录300/719篇带顶层Lean形式化，约42%。这些是仓库产物口径，不是独立定理数或尝试成功率。[当前仓库与历史记录](https://github.com/openai/math/blob/main/README.md) [撤回与修订历史](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/history.md)

本轮读取的README方法段补充说明，评估提出约4000个问题，多数结果按同一程序产生，每项结果平均使用约3小时该模型的思考计算，也存在例外和人类可读性编辑。此方法说明读取于10月14日，未逐字确认10月12日README快照，不能反推当时全部方法信息已公开；4000题与稿件也不一一对应，不能相除计算成功率。[当前仓库与历史记录](https://github.com/openai/math/blob/main/README.md)

Lean机械检查形式命题与推理依赖，但还要核对它是否表达了原问题、结论是否新颖。研究产物量和机器证书都不能替代数学语义检查与同行评议。[当前仓库与历史记录](https://github.com/openai/math/blob/main/README.md)

既有研究报告的事实摘要与条件说明；具体引用在正文标注
对应材料：[当前仓库与历史记录](https://github.com/openai/math/blob/main/README.md)、[撤回与修订历史](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/history.md)

### 自然语言与Lean翻译受到技术质疑

10月6日公开的Navier–Stokes技术质疑给出一个具体翻译问题：自然语言估计要求比输出多4阶导数，Lean对应结果要求多5阶。可以理解为机器检查的版本多加了一层条件，因此结论更弱，可能没有覆盖原文声称的范围。[质疑预印本](https://arxiv.org/html/2610.08144)

这是该预印本对特定版本的技术质疑；作者在Disclaimer中没有判定自然语言证明本身正确与否。读者应同时核对被讨论版本与后续修订，不能把质疑当作最终裁决。[质疑预印本](https://arxiv.org/html/2610.08144)

既有研究报告的事实摘要与条件说明；具体引用在正文标注
对应材料：[质疑预印本](https://arxiv.org/html/2610.08144)

## 时间线

- 2024（原报告记载的进度/观察 / 年份）：专用数学系统达到IMO银牌标准
  日期依据：2026-10-13研究报告第7模块；本次未把未披露日期补成精确日期
- 2025（原报告记载的进度/观察 / 年份）：Gemini在比赛时限内达到金牌标准
  日期依据：2026-10-13研究报告第7模块；本次未把未披露日期补成精确日期
- 2025-07-21（论文/项目页面发布 / 日期）：2024与2025的官方过程对照的原始发布记录；不代表实验在该日完成
  日期依据：原始页面元数据 article:published_time
- 2026-10-06（技术质疑首稿 / 日期）：Navier–Stokes语义/形式化对照预印本v1公开。
  日期依据：arXiv v1页首与首稿记录；不是裁决日
- 2026-10-07（仓库修订与撤回 / 日期）：history记录符号错误撤回与形式化更新。
  日期依据：history事件标签；不是文档首发日
- 2026-10-12（研究材料范围 / 资料截止）：这份研究摘要的资料范围，不是上述事件统一发生的日期。
  日期依据：原研究报告事实范围

## 工作意义

这有望减少证明搜索和形式化的重复劳动，但问题选择、自然语言与形式命题的对应、外部复核仍是重要工作。

### 后续观察

基准情景是系统继续帮助搜索、写作和形式化局部论证，数学家仍承担问题选择、语义对照与最终判断。若独立团队在预先封存的新题上重复得到可发表证明，并逐项公开自然语言—形式命题映射，能力判断才可上调；观察重点是后续 First Proof 盲审、跨机构复现、形式化语义审计及被独立研究采用的结果。

## 证明材料

### Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad

[2024与2025的官方过程对照](https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/)；类别：原始研究或机构项目说明；状态：active
支持：用于说明：竞赛证明从形式系统走向自然语言
定位：官方文章 Breakthrough Performance at IMO 2025 with Gemini Deep Think；Making the most of Deep Think mode；文末IMO审查范围脚注。
先核对这条材料所讨论的系统或版本，再沿上述位置阅读具体结果与条件。
原始发布：2025-07-21；修订：未提取；原始页面元数据 article:published_time
2024与2025的配置和题目均不同；官方确认解答不等于流程独立复验。
2026-10-14书目信息，非实验复验。

### math/README.md at main · openai/math

[当前仓库与历史记录](https://github.com/openai/math/blob/main/README.md)；类别：公开代码或模型资料；状态：active
支持：用于说明：研究稿件与形式化证书
定位：README：Navigating the collection、How the results were produced。
先核对这条材料所讨论的系统或版本，再沿上述位置阅读具体结果与条件。
原始发布：未知；修订：未提取；原页面未提取到可靠发布日期，保持未知
当前main方法说明不自动代表10月12日历史快照；未复核全部稿件或数学正确性。
2026-10-14书目信息，非实验复验。

### math/history.md at fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb · openai/math

[撤回与修订历史](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/history.md)；类别：研究仓库修订历史；状态：active
支持：用于说明：研究稿件与形式化证书
定位：history：October 7, 2026 → Withdrawals / Additional Formalizations。
先核对这条材料所讨论的系统或版本，再沿上述位置阅读具体结果与条件。
原始发布：未知；修订：未提取；原页面未提取到可靠发布日期，保持未知
同一仓库版本历史；不按文件或链接累计独立结果。
2026-10-14书目信息，非实验复验。

### Navier–Stokes lost in translation – Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs

[质疑预印本](https://arxiv.org/html/2610.08144)；类别：技术质疑预印本；状态：active
支持：用于说明：自然语言与Lean翻译受到技术质疑
定位：arXiv v1 §1末尾Disclaimer；§3.1 Example 3.1与式(3.1)/(3.2)。
先核对这条材料所讨论的系统或版本，再沿上述位置阅读具体结果与条件。
原始发布：2026-10-06；修订：未提取；arXiv v1首稿记录
特定版本的技术质疑，非最终正确性裁决；未复跑形式化。
2026-10-14书目信息，非实验复验。

### First Proof 第二批盲审报告

[First Proof 第二批盲审报告](https://1stproof.org/assets/docs/report.pdf)；类别：原始研究或机构项目说明；状态：active
支持：后续研究级盲审的阅读入口；本页不据此发布成功率。
定位：First Proof第二批报告：评审方法、题目与逐项评审结论。
题目与模型信息隔离情况需连同评审结果阅读。
原始发布：未知；修订：未提取；未从二进制资料猜测发布日期
此处保留既有研究的后续观察入口，未重核全部盲审结果。
2026-10-14书目信息，非实验复验。

本页整理：2026-10-14；事实范围：2026-10-12。概念解释与既有研究展开；元数据访问不是原始实验复验。

阶段：研究验证：少量结果经盲审、数学家核查或Lean检查；没有足以证明广泛稳定部署的证据。
前沿较快；转化渐进；信心中。定性判断不是职业自动化率。