AI 与 Erdős 问题 397：经过验证的证明、先前成果和自我改进的前景

Neel Somani 报告称，他提示 GPT-5.2 Pro 处理 Erdős 问题 397，并提交了一份证明，Terence Tao 将其接受并收录于问题数据库。该证明使用 Harmonic 的 Aristotle 形式化，并经 Lean 检查。Berman 称这是极其困难的开放问题，并说模型花了约 15 分钟；这个时间是报告中的说法，并非审查和形式化所需的全部时间。

一项重要的后续更正是：Tao 的 [AI 贡献追踪表](https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems)将 2026 年 1 月 10 日的解列为完整且经过 Lean 检查，但也记录了 1 月 14 日发现的一份类似的人类完整解，出自 2012 年的一场中国竞赛。因此，这是一份有效的 AI 辅助解，但不能证明它是对此前未解问题的首次求解。Erdős 问题的难度范围很广。

Berman 提到近期几项 AI 辅助尝试，认为模型正开始为前沿数学作出贡献。Tao 清单中的部分条目是完整解，其他则是部分结果、错误结果，或后来发现已有先前解的结果。这些结果不能混为一谈；形式证明验证的是编码后的陈述，并不能证明此前没有相关成果。

他用一张示意图描述智能爆炸：帮助发现更好方法的 AI 可以改进未来的 AI，从而形成反馈循环。这是一种可能的情景，并非根据测量得出的发展轨迹，也不能证明会出现无限智能。这种循环的速度和规模取决于研究、实施、硬件及其他限制。

Berman 将模型在国际数学奥林匹克问题上达到金牌水平作为进步的证据。IMO 是数学竞赛，而不是编程竞赛。竞赛表现与研究开放问题是不同的测试，达到金牌水平本身不能证明模型具备广泛的自主数学发现能力。

他描述了一项由 AI 发现的矩阵乘法改进，却将系统称为 AlphaFold。画面所指的成果来自 Google DeepMind 的 [AlphaEvolve](https://deepmind.google/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/)：其流程发现了一种算法，用 48 次标量乘法完成 4×4 复数矩阵乘法，而引用的此前方法需要 49 次。AlphaFold 研究蛋白质结构；AlphaTensor 则是另一个独立的矩阵算法系统。

Berman 认为，矩阵乘法是 AI 的核心，因此即使小幅改进也可能在大规模应用中发挥作用。但这个特定的 4×4 复数矩阵结果不意味着所有矩阵乘法都变快：实际性能取决于硬件、矩阵大小、数值性质和部署方式。他还讨论了 DeepMind 的报告：AlphaEvolve 帮助优化了部分数据中心调度、TPU 设计和模型训练操作，而不是 Google 的全部基础设施。

Berman 提到 Sakana AI 的 AI Scientist 是另一个自动化部分研究工作的尝试，并认为这些发现最终可能反馈到模型开发中。视频包含 HPC-AI 微调基础设施的付费赞助和赠送额度的推广；这些商业信息反映的是视频发布时的情况。

Berman 展示了 Tao 公开追踪 AI 对 Erdős 问题贡献的页面。它区分完整解、部分结果、失败尝试，以及后续文献检索发现已有成果的情况。有些解结合 GPT-5.2、Aristotle 和 Lean，其他条目则涉及不同系统或人类贡献。绿色形式验证标记的含义比新颖性更窄，也不能证明所有相关问题都已解决。

Berman 预测，更强的数学推理和开放式科学发现最终可能帮助解决疾病问题并改进 AI 本身。这些是充满希望的预测，而不是癌症或所有疾病都会被治愈的证据。他认为 AI 工作可以并行化，但实际系统仍受算力、能源、数据、实验验证和人类监督的约束。