OpenAI 把自家模型生成的证明交给了外部专家复核。计算机科学、数学、物理学三个领域，一批被称作 "shepherds" 的学者负责逐条检查这些由 AI 写出的推理。这个动作比结论更值得琢磨：它等于公开承认，模型能写出像模像样的证明，和证明真的成立，是两件完全不同的事。
更硬的一手是形式化。部分证明被翻译成 Lean，交给计算机逐步验证。自然语言的证明可以含糊其辞，Lean 不行——每一步要么成立，要么不成立，没有"看起来很有道理"的灰色地带。这是把 AI 输出从"读起来对"推向"可被机器判定"的关键一步，也是目前少数真能戳破模型幻觉的手段。数学界这些年推 Lean 推得辛苦，如今倒成了检验 AI 的现成工具。
请诺贝尔奖得主级别的学者出面，传播上的考量当然存在。但抛开公关层面，人工复核加形式化验证这套双轨制，指向的是同一个悬而未决的问题：AI 在科学发现里到底是助手，还是作者？署名权、责任归属、成果可信度，全卡在这儿。在答案明确之前，先让机器把每一步算清楚，大概比再刷几个基准测试的分数都更有说服力。
