使用 20 个并行运行的 Codex 账户解决 20 个 Erdős 问题
与 Lean 4 和大规模云算力相连的 AI 智能体，如今正在为数十个高难 Erdős 问题生成经过机器验证的证明，这既令人振奋，也让人对这对数学研究意味着什么感到不安。评论者探讨了技术架构、资金与开源计划，并指出虽然形式化证明本身很有说服力，但把它们转化为适合人类阅读、富有洞见的论证仍是一个独立的挑战。讨论进一步延伸到“无用”纯数学的价值、随着证明搜索自动化后人类数学家的未来角色，以及 AI 驱动的定理证明最终可能如何与现实世界影响和经济变化联系起来。
基础设施、算力与模型访问
- 项目通过 OAuth 令牌使用多个 Codex 账户，并借助自定义 broker 对 API 调用进行负载均衡；“在本地运行 GPT”是措辞问题，并非自托管模型。
- 本地算力是一台多 vCPU 服务器；评论者指出，这类硬件对爱好者来说是可负担的。
- AI 智能体配有 bash 工具，并可访问虚拟机上预装的数学包。
- 提到的模型包括：GPT-5.6（用于生成）、Fable（用于 Lean 证明检查/摘要）、Gemini embeddings。
Harness、开源与贡献
- 问题主要集中在“agentic harness”：循环如何编排、哪些模型在“驱动”、以及如何衡量进展；细节仍停留在高层。
- 另一位参与者描述了一个类似的独立系统：在内网进行主权推理、用于 Lean/Sage 的沙箱化 worker、开权重模型，以及进一步微调的计划。
- 大家对将系统开源并允许贡献很感兴趣；作者表示该项目最初只是一个快速、封闭的实验，之后可能会开放。
有效性、严谨性与写作
- Lean 4 证明由机器检查；Fable 起到某种裁判作用。
- 批评意见：证明摘要在技术上过于密集，不适合人类读者；把形式化证明转化为清晰、优雅的解释是一个独立的、目前仍缺失的步骤。
- 作者承认这一点，并计划改进写作。
- 一些提交的 Erdős 题解曾被暂时撤回，不是因为错误，而是因为表述混乱或仅是部分结果；相关工作仍在进行。
- 有人建议集成 Lean 的“comparator”工具，以在修改上下文时防止细微的不健全性。
纯数学与 AI 定理证明的价值
- 讨论集中在：看似“无用”的纯数学究竟是自洽且对社会并不重要，还是它有着意料之外的应用历史（例如密码学）以及内在的审美价值。
- 有些人把解决 Erdős 问题看作一个基准和技巧来源，而非直接应用；真正的现实世界影响可能更多来自前沿问题或千禧年难题。
- 也有人认为，即便这只是纯娱乐，它与任何智力爱好一样正当。
对数学家与社会的影响
- 有人担心 AI 证明系统会“把数学的乐趣吸走”，并威胁数学家的工作；反驳意见将其类比为更早期的自动化焦虑（例如织机、计算器）。
- 多位评论者认为，数学家将转向理解、猜想和审查 AI 生成的证明；高级证明本就常常超出单个 human 的能力。
- 更广泛的讨论涉及把生计与工作解耦、潜在的 UBI，以及对 AI 公司的征税；对于政策变革的紧迫性存在分歧。
AI 在数学中的现状与未来
- 许多人对 LLM 如今能解决非平凡的 Erdős 问题感到惊讶；人们的看法正在从“LLM 能做数学吗？”转向“我们能把这推进到什么程度？”
- 预期的未来包括：对现有数学进行大规模自动形式化、大规模自动猜想生成与评估，以及可能出现类似 BOINC 的分布式数学探索协作。