Dan Abramov 用 frontier 模型反正 Conway refinement 推论 (4 周 / 40B token / ~$40k)
- ID: b827197a
- 原文链接: https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/
- 作者: Dan Abramov
- 日期: 2026-09-18
- 分类: agents
- 来源类型: article
- 标签: llm-agent, math-reasoning, lean, conway, case-study
- 质量评分: 4/5
- 抓取时间: 2026-09-19T22:35:00Z
中文导读
前 React 核心作者 Dan Abramov 入门数学不足一个月，在 frontier 模型与 Lean 的多 agent 实验室里闭环了 Conway 50 年未解的 refinement 推论（omnific integers 上的 refinement 性）：PM 协调、Math 推思路、Red 查漏洞、Random 探索、Lean 形式化；总计三周、费以多 agent 的 chat log 判断进度、Lean 是否编译作为唯一确认闭环信号。他在文中明确警告：模型会反复用 euphemism 藏未证假设；名学、审计工具链、Lean skill 的工程价值是他总结的顶层 lessons learned。资源面临的问题：Lean 实现与证明质量需要独立检查；$40k 主要为缓存读取。
为什么值得关注
前 React 核心用 frontier 模型 + Lean 隐闭环了 50 年老推论：40B token · ~$40k · 三周
关键信息
- 标题：Dan Abramov 用 frontier 模型反正 Conway refinement 推论 (4 周 / 40B token / ~$40k)
- URL：https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/
- 发布时间：2026-09-18
- 分类：agents
- 标签：llm-agent, math-reasoning, lean, conway, case-study
English Summary
Dan Abramov, a math noob and former React core, spent about a month of free time and ~40B tokens (~$40k, mostly cache reads) running a multi-agent lab against Conway's 50-year-old refinement conjecture. The cast is PM / Math / Red / Random / Lean, the verdict comes from whether Lean compiles, and the post records three weeks of iteration including a full re-burn of the folder. He warns repeatedly that the models hide unproven hypotheses behind euphemisms. Take-aways worth a checklist: naming, audit tooling, model complementarity, and the engineering value of Lean Skills. Caveat: Lean proof quality warrants independent review; cost figures are cache-read heavy.