研究者跟进 OpenAI/Anthropic 的 ETH 反驳声明，发布 Lean 机器校验的哈密顿回路结果
xennygrimmato_ · x · 2026-10-28
研究者 xennygrimmato 发布 GitHub 仓库 eth-hamiltonicity，跟进 OpenAI（openai/math）与 Anthropic（anthropics/formal-math）于 10 月 26 日发布的「指数时间假设（ETH）反驳」声明——两家的结果目前仍在专家评审中。
该仓库的关键内容：
- 结果仅针对稀疏图（|E| = O(n)），且为渐近性结论，条件依赖于两家实验室的反驳成立
- R1 结果：确定性次指数时间内判定哈密顿回路数量的奇偶性，附随机化判定与有向图版本
- 所有证明在 Lean 中机器校验，且是在重建两家实验室各自 Lean 证明的基础上完成的（仓库含 lean-bridge 与 lean-bridge-anthropic 目录）
- 附论文 PDF、LaTeX 源码与 findings 笔记，MIT/Apache-2.0 双许可
这是对「顶级 AI 实验室声称推翻复杂度假设」这一罕见事件的独立第三方形式化验证，值得关注后续专家评审结论。
「研究」频道最新
- 给模型微调出「执念猫癖」做对照：AI 意识判据全部失效 — MirrorEthic_Anchor · 2026-10-28
- 逐个神经元扫 Qwen3-8B,用 Haiku 给怪异度打分 — Sauers_ · 2026-10-28
- DiscoTrace 获 EMNLP 最佳论文:LLM 答题策略缺乏人类式的社区多样性 — TuhinChakr · 2026-10-28
- arXiv 新论文提出世界模型表征的三问框架：可达性、准入与指派 — SoloGen · 2026-10-28
- OpenAI 发布内部前沿模型数学成果，Terence Tao 长文回应消化之道 — krisspy39 · 2026-10-28
- Divergence Labs 联手 Anthropic 用 Claude 发现食物过敏抗体疗法 — anshulkundaje · 2026-10-28