从246到186：这一次到底改变了什么
孪生素数猜想关注的是存在无穷多对差值为2的素数。围绕这一猜想，可量化的指标是"素数间距的最小上界"——即能否证明存在无穷多对素数，其间距不超过某个值。2013年这一上界被推进到7000万，此后经过约十年的工作压缩到246，并长期停滞。GPT-6的贡献是将该上界进一步推进到186，同时配套发布了完整论文、可执行的Lean 4形式化代码，以及一份记录推理全过程的CoT文档。
具体方法上，GPT-6构建了一个包含40个元素、直径恰好为186的可容许集合，并在GPY筛法中发现了"三重稠密可除性"这一新的组合条件，从而放宽了此前对模数平滑性的严苛限制。最终通过多维Selberg筛法中的主控函数，把高维积分转化为可严格计算的有限系数恒等式。值得注意的是，41维的尝试被模型自身判定为死胡同，转向40维后才取得突破。
对不同用户群体的实际价值
对纯数学研究者而言，核心价值不在186这个数字本身，而在方法论层面的新提示：新的因子分解条件如何被发现、维度选择如何被调整、为何要在某个精度阈值上从浮点近似切换为精确有理数算术。这些思路可以作为拓展研究方向的参照。
对AI与推理模型研究者而言，这份CoT文档是少有的、关于大模型在长链条形式化推理中如何自我纠错的完整样本：模型如何识别投机路径不可行、如何在41维失败后重构问题、如何主动规避浮点误差带来的隐性风险。这些行为模式对改进推理模型的训练与评测有参考意义。
对教育与科普场景而言，论文、Lean 4代码与CoT文档三者齐备，使得原本门槛极高的解析数论前沿成果，具备了从课堂演示到研究入门的多层次使用可能。
适用场景与选择标准
适合使用的场景：解析数论与组合数学中存在大量"可容许元组""筛法估计"等结构化、目标明确的子问题。这类问题可以被编码为有限维优化或形式化命题，适合大模型做系统性搜索与候选构造。
需要谨慎的场景：依赖于尚未被形式化的深层定理的问题。GPT-6的证明建立在三条未在Lean中证明的输入公理之上，涉及有限域上的指数和估计。这些结论虽然在既有数学文献中已被证明为真，但尚未被全部转化为Lean代码。这意味着在形式化覆盖不足的领域，直接采信AI证明仍存在缺口，需要人工复核底层引理。
不适合的场景：需要全新概念框架或公理体系变革的问题，以及高度依赖专家个人审美与判断的构造性结果。AI擅长在已有框架内做精细搜索，但当前阶段难以替代数学家的概念创造工作。
如何用起来
对于希望复现或验证这一结果的研究者：
- 获取开源仓库 PrimeGaps186，内含论文PDF、Lean 4源代码与Python数值脚本
- 准备Lean 4工具链，并安装Python的FLINT高精度数值计算库
- 编译并运行Lean 4代码，确认每一步逻辑链可被机器验证
- 配合运行Python脚本生成数值证书，检查关键估计的数值证据
- 通读CoT文档，对照Lean代码理解每一步推理动机
对于希望将类似能力用于自身研究问题的用户：当前GPT-6的能力主要通过论文与开源仓库形式对外呈现，并未以通用API的方式直接提供数学证明服务。关注后续是否开放专项推理接口或工具链，是判断能否在自己的问题上落地使用的关键。
成本与落地建议
算力层面：Lean 4形式化验证本身对算力要求不高，普通工作站即可运行；但数值证书生成涉及高精度有理数运算，规模较大时可能占用数十GB内存与数小时计算时间。
时间层面：阅读并理解整套证明与CoT文档需要扎实的解析数论基础，初次接触通常需要数周；若要复现类似流程并适配到自己的问题上，调试筛法参数与Lean代码往往需要更长时间。
落地建议：
- 不要把"上界从246到186"简单等同于"AI已攻克孪生素数猜想"，终极目标仍是间距为2，距离尚远
- 在引用AI生成的数学证明时，明确区分"已形式化验证部分"与"依赖未形式化公理部分"
- 对关键结论，至少安排一位领域专家人工复核CoT中的关键步骤
- 当前阶段，AI数学证明最适合作为研究助手，用于拓展搜索空间与提示新方向；最终判断仍需人类研究者做出