2026年8月11日，Anthropic宣布其未发布模型成功提高了黎曼假设的解的下界。这一结果由Anthropic内部两位数学家确认，并通过开源证明助手Lean完成形式化验证，标志着AI在数学发现领域迈出了重要一步。 黎曼假设是数学领域最著名的未解难题之一，150多年来始终无人攻克，至今仍悬赏100万美元。据TechCrunch报道，Anthropic的未发布模型虽然没有完全证明该假设，但通过提高该假设成立的解的下界，取得了重大进展。这项于周一宣布的成果，是近期一系列AI驱动数学突破中的最新进展。 这一进展来自一个非同寻常的实验设置。Anthropic一位未接受过深入数学训练的职员，提示模型“认真尝试”证明黎曼假设，然后放手让模型在一天半时间内自主协调任务。模型在此期间测试了650个不同想法，协调60个子代理协同工作，共消耗3100万输出token。论文脚注详细记录了各子代理的贡献分工：2个子代理提出了关键想法，13个子代理贡献了辅助思路，30个子代理尝试但未能成功，13个子代理负责验证论证，另有2个子代理撰写了初稿。 该结果已由Anthropic内部两位数学家确认，并使用开源证明助手Lean进行了形式化验证。这一形式化验证环节至关重要——它提供了机器可检查的证明，直接回应了外界对AI生成证明可靠性的担忧。 从更广泛的视角看，这一成果预示着AI在数学发现中的角色正在发生深刻变化。传统上，数学研究依赖人类直觉和创造力，而AI系统如今已能自主探索大量可能的证明路径，并在子代理协作中实现有效分工。这种“大规模并行推理”的能力，正在为数学研究开辟新的可能性。 然而，AI参与数学证明也引发了学界争议。一些数学家对AI生成证明的可解释性持保留态度，认为缺乏人类能够直观理解的推理过程，可能掩盖潜在的错误。但Lean形式化验证的应用，恰恰为这一问题提供了一种解决方案——通过机器验证确保每一步推理都有据可循，从而在保证可靠性的同时，让AI的创造力得以充分发挥。
热门跟贴