I vibed a proof of Conway’s conjecture

作者让多个代理生成数学“论文”并用 Lean 追赶，曾在一天内堆出近 30 篇材料，最后发现核心步骤循环论证，模型自己也承认“没有证明”。第二轮把前置文献、风险探索和 Lean 证明拆到不同任务与 worktree，并让数学家核验；最终只确认一个有限度数素性结果。案例说明形式化工具能阻断错误传播，但不能把不理解问题的生成流程自动变成新数学。