借助 AI 沟通发现 17/19/23 曲线简单对称 Venn 图，经 Lean 4 形式化验证
pickover · x · 2026-10-21
数学家 Chris Dzoba 发布 arXiv 论文，首次构造出 17、19、23 条曲线的简单对称 Venn 图——此前的简单对称 Venn 图纪录停留在 13 条曲线（Mamakani & Ruskey, 2014）。据 pickover 介绍，这一发现源自人类与两个互相通信的 AI 模型协作。
- 此前已知：对称 Venn 图对任意素数条曲线都存在（Griggs-Killian-Savage 2004），但交点处有多条曲线通过；「简单」版本（每点恰两条曲线相交）此前只做到 13 条。
- 方法：在球面的旋转不变四角剖分上运行 Metropolis 随机游走，允许区域临时重复，从 Griggs-Killian-Savage 图解消多重点出发搜索；共找到 4 个 17 曲线、12 个 19 曲线、6 个 23 曲线的图。
- 23 曲线情形在两极附近被重复区域卡住两周，最终收散的两个谱系是首批 E=92 个状态中零重复的。
- 每个图都附带机器可检验证书，其中 17/19/23 各一个已由 Lean 4 形式化证明独立验证。
- 全部图均为非单调（non-monotone），这正是以往找到 11、13 曲线图的交叉序列搜索法不可能发现它们的原因。
「研究」频道最新
- Anthropic 与 Citrini 用 Claude 花近 5 万美元设计蝎子毒素结合分子 — chrisalbon · 2026-10-21
- 给 AI 一万美元做开放研究：GPT-6 Astra 与 Claude Fable 5.1 论文仍被专家拒稿 — sayashk · 2026-10-21
- 斯坦福团队推 ScholarCatalyst:专测 AI 检索可启发科研的早期文献 — lateinteraction · 2026-10-21
- Pathway CEO 撰文:Transformer 不够,超级智能需要会积累经验的模型 — schwentker · 2026-10-21
- Laude Institute 资助斯坦福 CLM:面向快速决策的对比语言模型 — Azaliamirh · 2026-10-21
- OpenAI 收购 Orchestra Bio，加码生命科学 AI 模型 Rosalind — TechCrunch AI · 2026-10-21