I Vibed a Proof of Conway's Conjecture
3 hours ago
- 作者花费了一个月时间使用AI模型（Claude、ChatGPT、Codex）来解决约翰·康威50年前提出的关于全知整数的康威细化猜想。
- 该证明已在Lean中形式化并通过机械检查，但尚未经过数学家的独立验证。
- 最初的尝试是直接指示AI代理解决问题，但常常产生幻觉或有缺陷的结果，导致重新开始。
- 该项目需要建立多代理系统进行分工，包括Lean验证、数学推理和审计角色。
- 关键见解来自让AI代理相互批评和纠正彼此的工作，尽管许多想法因丢失或被拒绝而被多次重新发现。
- 作者认识到AI在证明形式化方面有效，但在数学创造力和自我评估方面存在困难，因此人类监督至关重要。
- 该过程估计花费了4万美元的API代币（总计约400亿个），并凸显了区分真正进展与AI生成的“胡说八道”的挑战。
- 该证明仍然复杂且难以简化，但作者希望未来能使其对数学家和Lean用户更易理解。
- 作者总结道，虽然该实验展示了用AI进行“氛围编码”数学的潜力，但需要大量的时间、代币投入和细致的项目管理。