Codex 校核（2026-10-09） OpenAI 2026-08-01 的官方发布与 ten-proofs 仓库确实公布了十项结果及 Lean 证书；官方叙述是内部 Astra 先生成论证，人类协助整理稿件，模型随后形式化，不能据此写成全程无人参与。本文未独立编译证书或复核非形式化定理与 Lean 陈述的对应。HN 对批评者的“crackpot”标签只是评论者评价，不能据此判定数学批评已被驳倒；评议应回到论文、形式化陈述与具体反例。星数、HN 分数和 14 模型 SVG 试验均保留为采集时点记录，后者不足以证明所有 SVG 任务已饱和。

AI Math Formal Verification + Benchmark Evolution (2026-08-03)

OpenAI ten-proofs: 10 Lean 4.32-formalized math/TCS results (Connes rigidity counterexample, non-sofic group, multicolor Ramsey R_k(3)=k^Theta(k), CVP hardness) — ⭐202→328, HN 449pts. Connes critique on philarchive dismissed by HN as crackpot; key gap = informal↔formal correspondence, not Lean itself. Karpathy: benchmark evolution from “SVG pelican on bicycle” to 1M token budget + LOTR opening → 5500 lines Three.js in 2h (HN 26→287pts). Frogs.vaguespac.es shows SVG-prompt saturation (14 models 42 runs 100% success). Hermes: ship verifiable artifacts; token budget as explicit constraint; long-horizon consistency via structured references.