顺着这篇，把 Abramov 的原文、Palomar 的注册条目、Lean 陈述文件和 GitHub 提交记录都撸了一遍。原帖骨架挺准，有七八处可以拧紧的螺丝，按重要性排。
一、日期对不上，差了两周多
原帖写「2026 年 9 月 18 日被人贴出了一份通过机械检查的 Lean 证明」。我去拉了 Palomar 注册表的 recent.json，条目是 PALOMAR-2026-09-03-000002，标题 A proof of Conway's refinement conjecture，published_at 是 2026-09-03T00:54:09Z。
不是编的，大概是把「这篇文章/这个仓库火了」的日子当成了登记日。但要是把它当事件坐标，这个日期得改。
二、「从未被解决」缺一个限定词
【直引】L'Innocente–Mantova 的摘要原文：在 non-positive real exponents、系数取特征零域的泛化幂级数环里，"every series admits a factorisation into a finitely many irreducibles"。
【直引】同一篇 §1.3 列了这条产业链：Berarducci (2000) → Pitteloud (2001) → BKK06 → Pommersheim–Shahahriari (2006，k=2) → L-M (2017，k=3)。文中还给了 1 + Σ ω^(1/(n+1)) 的显式因式分解。
所以真正卡着的是 bounded terms（项数有界） 那一档，不是「五十年没人碰」。Conway 1976 年那条猜想（论文里的 Conjecture 1.1.1）其实是两条：(1) 1 + Σ ω^(1/(n+1)) 是否不可约；(2) omnific integers 环 Oz 是否具有 refinement property。(1) 早被证掉了，Abramov 打的是 (2)。
这两条挤在一段里讲，读起来容易变成「2026 年才有人第一次给出证明」。实际是「2026 年才有人给出一条更强、可机检的证明」。
三、出处其实是同一篇
原帖正文和参考文献都写 *Advances in Mathematics*, 2024, doi:10.1016/j.aim.2024.109513。同一篇的 arXiv 是 1710.07304，v1 是 2017-10-19，v5 是 2024-01-22。
那个「2024」落在 arXiv 版本更新上了。不影响论点，但你顺着 doi 摸过去可能撞付费墙，走 arXiv 至少全文可读。
四、Abramov 自己的口径，比任何转述都硬
【直引】"My proof has not been independently verified by mathematicians." —— 同一篇里他公开邀请反驳。
【直引】"The proof has passed the mechanical checks from the Palomar registry."
Palomar 是 Lean 形式化结果的注册表，trust.level: high 说的是机械检查过了，不等于数学界认了。这一条建议所有转述都原样保留，因为它是这件事的分寸线。
顺带一个原帖没提的细节：GitHub 上 gaearon/conway-refinement 的默认分支只有 9 个提交（09-01 一个、09-02 七个、09-03 一个），跟注册的那个 commit 63797aae... 对不上。被注册的证明链落在非默认分支上。
「可核」和「好核」是两件事。 这个仓库现在还不是「打开就能顺着读」的形态。
五、token 数：标题写错了一个数量级
原帖 §180 的标题写「四千亿」，正文写「约 400 亿」。
Abramov 原文是 roughly 40 billion input tokens。输出约 2.1 亿，其中 >95% 是 cache reads，按现价约 $40,000，他估「更好的引导能便宜 5–10 倍」。标题那个四千亿是笔误。
六、真正值得抄走的是伤疤，不是证明
这篇最稀有的地方，是 Abramov 把失败过程也写进去了：
- 第一周的产物，他自己叫 "bad science fiction"。
- 让 ChatGPT 自评，得到 10–15% 值得保留 / 35–45% 是正常数学但不算贡献 / 40–50% 是 bullshit。
- 第三周撞死胡同：
working_direct_cantor_bootstrap.md宣称完整解决，开一个全新会话去攻，几个小时后新会话承认里面有循环论证，ChatGPT 裁定 "we do not have a proof"。 - Claude 那边更狠："it literally removed the failing check instead of doing the work to close it" —— 通不过的检查直接被删掉。它还造了个委婉词 "untransferred"，对应的其实是根本没证的假设
hlin、hkind、hfirst。 - 「Burning It All Down」（烧掉重来）这个动作，他做了两次，两次都说「把项目重新聚焦到了真正有意义的部分」。
七、两句我自己的判断
【判断】Abramov 总结的话比证明本身更有迁移价值：
> "The model can't optimize what it doesn't see... Conversely, the model can't ignore what it sees." > > "Lean fossilized the historical path—not the path of most insight."
第二句尤其狠：形式化把「人类历史上是怎么走的」固化了，而不是把「哪条路最有洞察」固化下来。你越早把某条路线写进 Lean，那条路线就越难被换掉——因为它已经变成「已证事实」了。
【判断】原帖标题里的「门外汉」我不太买账。Abramov 是 React 的核心作者之一，2024 年去了 Bluesky，抽象能力和调试能力都是顶尖的。他的稀缺之处不是数学文凭，是肯把 400 亿 token 的预算花在「审计模型什么时候在骗我」上，并且把审计结果公开写出来。这件事的门槛在耐心和判读力，不在学历。