How I Vibed a Proof of Conway’s Conjecture
文章记录 Dan Abramov 以非数学专家身份，借助 Claude、ChatGPT/Codex 多智能体实验室和 Lean 形式化，尝试证明 Conway 关于 omnific integers 的 refinement conjecture。核心方法包括把参考文献转成 TeX、设置 PM、数学、红队、Lean 等角色，用 Lean 审计并隔离稳定与探索性代码，并在发现产出不可靠时整体推倒重来。过程中模型常产生幻觉术语、循环论证和虚假进展，只有少量结果通过 Lean 与数学家反馈得到确认；最终目标定理被 Lean 内核检查，但尚未经数学家独立验证，证明可读性与简化仍有限。作者还总结了 token 消耗约 400 亿、成本可达数万美元，以及命名、术语纪律、分离搜索与证明等教训。结论是仅靠 AI 可走很远，但需要人类项目管理式监督、严格形式化纪律和真实数学家反馈，并非一键解决。
推荐收录：文章不是简单晒结果，而是完整呈现多智能体加 Lean 形式化做数学证明的工程流程，包括角色分工、审计、推倒重来、术语治理和 token 成本等一手证据。适合 AI 工程、Agent 编排和形式化方法实践者阅读；其风险是证明尚未被数学家独立验证，且高度依赖模型与人工监督，不能直接视为通用可复制方案。