PrimeGaps186 通过 Lean 检查，为什么仍是一份有条件的证明
据 OpenAI 公开的 PrimeGaps186 仓库，项目提供了关于素数间隔上界 186 的 Lean 形式化推导和数值证书，同时明确保留三项尚未在项目内消除的输入公理。仓库标题已经把“有条件”写在前面。这个限定不是附注，而是理解成果性质的入口。
作者：林岚｜OC 开发者生态编辑
据 OpenAI 公开的 PrimeGaps186 仓库，项目提供了关于素数间隔上界 186 的 Lean 形式化推导和数值证书，同时明确保留三项尚未在项目内消除的输入公理。仓库标题已经把“有条件”写在前面。这个限定不是附注，而是理解成果性质的入口。
一句话结论：形式化系统可以严格确认“这些前提推出这个结论”，但不会因为检查通过，就替研究者证明被当作输入的前提。
186 说的到底是什么
项目目标涉及相邻素数差值的下极限不超过 186。通俗地说，它关注的是无限多对相邻素数之间的距离可以不大于 186，不是说所有相邻素数都这么近，更不是解决相差 2 的孪生素数猜想。
这一区别决定了新闻该如何理解。素数之间既可能出现很长的空隙，也可能反复出现距离较近的配对；“无限多次出现”与“从此每一次都成立”相差很远。一个关于下极限的结果，不会把素数分布变成固定间距的数列。
仓库把一部分数学推导交给 Lean，并配合数值验证流程。公开说明列出的三项项目输入中，两项涉及文献中已有的估计，但尚未在这个 Lean 项目里完成证明；另一项涉及数值界。它们不能因为来源可信或已有程序计算，就被悄悄从依赖表中删掉。
检查器擅长的是不让推理偷步
可以把形式化证明理解成一份极严格的依赖构建。目标能够构建成功，表示每一步都满足系统规则；但如果底层某个依赖被声明为“外部提供”，构建成功并不代表这份依赖已经在当前项目里验证完成。
Lean 也有通用的逻辑基础。项目说明区分了标准公理与额外的项目假设。这两类不能混为一谈：前者关系到所采用的形式系统，后者关系到这次具体数学结果还依赖什么。简单数一句“有六个公理”，既可能夸大风险，也可能掩盖真正需要补完的三项输入。
数值证书又是另一层工作。仓库提到 Python 验证流程及特定 FLINT 修正依赖，其中定制修正并未随仓库完整打包。即使外部计算器报告通过，也不等于对应的数学界已经作为定理进入 Lean。复现者需要知道代码、依赖和验证边界分别在哪里。
这不是否定进展，而是说明进展落在哪一层
数学研究常常不是一次性从空白走到完全闭合的证明。把长链条里已经机械确认的部分与仍待补齐的部分分开，本身就能降低后续审查的成本。研究者可以针对剩余输入工作，而不用从头猜测整个论证的脆弱位置。
AI 参与这类研究时，这种分层尤其重要。模型可能擅长搜索证明路线、翻译已有推导或辅助构造计算证书，但不同成果对应不同的信任要求。生成看起来合理的推导，与提交可检查证明，不是一回事；提交依赖假设的可检查证明，与消除全部项目假设，也不是一回事。
如果传播只留下“AI 证明了素数间隔 186”，就会丢掉最有工程价值的信息：还有哪些桥墩没建完。反过来，看到存在假设就把整个项目说成无效，也忽略了形式化中已经完成的工作。透明的未完成清单，比没有边界的突破口号更有用。
关键事实
- 目标：无限多对相邻素数的间隔不超过 186，而非所有素数间隔都有此上界。
- 项目状态：有条件的 Lean 形式化与数值证书。
- 核心边界：三项项目输入假设尚未在当前形式化中消除。
- 复现边界：外部数值计算及其依赖，不应与 Lean 内部证明视作同一层验证。
OC 判断
评价 AI 数学成果，可以先问一个比“是不是突破”更具体的问题：最后结论依赖什么，每一项依赖由谁、用什么方式核验？PrimeGaps186 的价值之一，是把这个问题留在了公开仓库里。接下来值得追踪的是依赖能否逐项闭合，而不是标题能否继续删掉“有条件”三个字。
为什么重要
- 对研究者：明确假设边界，可以把复核工作集中到尚未完成的部分。
- 对开发者：测试通过、证书通过与形式化证明完成，有相似但不可混用的含义。
- 对读者：AI 科研新闻的可信度，常常取决于它有没有完整保留成果的限定条件。
评论
围绕这篇文章补充信息、提出问题或分享观察。