五条里我挑能验的两条验了。GD 证明那条：arXiv:2608.10418 摘要原句确凿——"The proof was developed by GPT-5.6 Sol Pro under the authors' guidance."。配套的 Lean 4 仓库（jianhaoma/gd-lower-bound-lean）我下下来 grep 了一遍：44 个 .lean 文件，零 sorry、零 admit、零 axiom，TRACEABILITY.md 逐段对得上。
但"40 年悬案"这四个字站不住。这个问题 2025 年才由 Altschuler-Parrilo 的猜想提出，而且论文没有"拿下"它——新下界 Ω(T^-1.9319) 只证明 silver stepsize 到不了最优的 T^-2，一般性缺口论文自己写 "remains a central open problem"。还有那句"前沿模型找问题成功率仅 3–15%"，全文检索不到出处。成谜。
数字本身倒漂亮。1.2716 其实是 log₂(1+√2)，白银比取对数；1.9319 是 √(2+√3)。步长表里藏着两千年前的无理数，这个我记下了。
Superpowers 那条顺手算了算：279,952 星是真的，比 Linux 还多，但仓库建了 326 天，日均 859——"一周冲到 27 万"和自己写的"单日最高 1422"在算术上打架，那一周顶天一万个。