先看证据
一句“据称证明”牵出的两种时间
Simon Willison 于 2026 年 10 月 7 日发布了 Jake Boggan 的一段 Hacker News 评论。Boggan 指向 OpenAI/math 仓库中的 problem 180，说 Barnette 猜想“据称”已经得到证明；他同时回忆，自己断断续续研究这个问题 24 年，曾为此投入数千小时，去年夏天甚至有几天以为自己已经解出。评论记录的是听闻和个人经历，不是对证明有效性的确认。
值得读的冲突就在这里：一个研究项目可以在公开目录中迅速出现，一位研究者却可能用几十年把同一个问题纳入生活。若证明最终成立，知识会向前推进，但 Boggan 失落的感受也不会因此变成误读。他把这种感受比作听闻前任突然去世，说明数学问题对长期投入者不只是一个待关闭的题目，也是一段仍在继续的探索关系。
有限范围的验证，不能替代一般证明
Barnette 猜想提出于 1969 年，断言每个有限、简单、平面、二部、三正则且 3-顶点连通的图，都含有一条经过每个顶点恰好一次的 Hamilton 圈。关键在“每个”：它不是说已经找到的图都符合结论，也不是说大量样例没有反例，而是要求结论覆盖所有满足条件的图。证明必须支撑这个普遍断言。
已知的计算结果提供了背景，却不能跨过这个逻辑门槛。1985 年的工作验证了顶点数不超过 64 的情形，这说明一个明确有限范围内的检查，并不自动推出任意规模图都成立。对技术读者来说，这是判断模型数学成果时最容易被传播速度遮住的区别：跑过许多案例、给出有说服力的推理摘要，和证明一个带有无限普遍性的命题，并不是同一种证据。
目录的规模说明产能，不等于正确率
OpenAI/math 的做法，是扩大模型对开放数学问题的评测，并把内部模型生成的研究结果整理成论文家族和手稿。材料给出的目录规模是 722 篇手稿，归为 372 个家族；评测中模型被提出约 4000 个问题。每项结果平均使用约 3 小时 ChatGPT Pro 思考算力，绝大多数结果来自同一个未发布的内部模型。这些数字显示的是生成和整理研究线索的规模，不是经同行确认的定理数量。
这种组织方式的价值，在于把原本分散的模型输出变成可浏览、可追踪的研究入口。仓库还发布了 10 项结果的推理摘要，让读者有机会看到部分工作如何展开。但目录越大，越需要区分“手稿被收录”“推理过程可读”和“结论已被证明”这几个状态。若把条目数量直接读成成功率，规模就会制造超过证据所能支持的确定感。
形式化是证据链的一部分，不是装饰
仓库附有支持材料、部分 Lean 形式化和推理摘要，但材料明确指出，不是所有手稿都完成了 Lean 形式化，未形式化的结果也可能有问题。这意味着这些条目处在不同的验证阶段，不能因为同处一个目录，就默认它们拥有相同的可信度。尤其对 problem 180，现有材料只记录 Boggan 听说它“据称已证明”，并没有给出证明文本或核验结论。
形式化的作用也需要说准确。把证明写入 Lean，可以让形式系统检查形式化内容中的推理步骤，但这不自动回答形式化是否完整表达了原命题、证明是否经过独立数学审查，或最终结果是否有其他缺口。判断一个结果时，读者需要知道具体证明在哪里、形式化覆盖了什么、哪些部分仍依赖非形式化论证，以及由谁检查过。仅有一份摘要，无法替代这些信息。
把模型产出当研究入口，而非定理库
对研究团队和技术负责人，这套目录适合承担“发现与分流”的工作：帮助研究者筛选模型提出的数学线索，定位值得继续检查或形式化的结果。它不适合被当作可以直接引用的可信定理库。对于一个影响理论判断的结论，流程应从原始证明开始，核对推理和适用条件，再检查形式化覆盖与独立验证状态，而不是从标题或目录条目数推断结论已经成立。
Boggan 的评论提醒人们，研究工具改变的不只有产出速度，也包括成果被宣布、被看见和被个人接受的节奏。但这段材料没有提供 Barnette 猜想证明的文本，也没有说明它是否通过同行核验，因此不能据此断言猜想已经解决。稳妥的判断是：把 problem 180 当作待查的研究线索，直到原始证明和验证状态足以支撑更强结论。对数学而言，公开一个候选答案是证据链的开端，不是终点。