大模型写Lean证明，353个Erdős开放问题自主解出9个，单题数百美元

大模型不再只写自然语言证明，而是直接产出Lean可编译的证明代码，每一步都由编译器机械校验。 此前这类形式化方法的成功集中在竞赛数学和人工辅助的形式化上，尚未在开放研究级问题上做过大规模评估。 在Formal Conjectures仓库当时全部353条Erdős问题形式化陈述上运行，解出9条，团队专家逐条确认Lean陈述忠实对应原始猜想。

智能体把证明拆成可独立搜索的子目标，用编译器报错和自动证明器反馈逐步补全证明草图。 基础智能体让多个子智能体各自独立搜索，全功能智能体则用进化算法协调它们，并可调用AlphaProof填补子目标。 全功能智能体还证明了492条OEIS开放猜想中的44条，并解决代数几何中Hilbert函数的一个开放问题。

在9道已被解出的Erdős问题上做回溯比较，最简单的智能体设计也能全部解出，只是在最难的问题上花费更高。 规划大规模探索时，更简单的智能体循环在竞赛级基准上表现不佳，因此当时选择了全功能智能体。 在Erdős #138和#125上，全功能智能体比基础配置节省2到5倍成本，但在其余问题上成本效率约为其一半。

这套智能体面向已有Lean形式化陈述的开放问题，输入是带sorry占位符的证明草图，输出是无sorry的证明。它已在组合数学、优化、图论、代数几何和量子光学的研究中使用，其中量子光学与图论的工作仍在进行。作者提出，刻画并扩展智能体的能力边界是后续方向。

作者指出，目前成功集中在Lean数学库成熟、任务常可分解为可处理子目标的领域，大多数Erdős问题仍无法解决，需要大量新理论的问题更无从谈起。智能体继承底层大模型的偏差，搜索方差很高，单题成本因随机性波动明显，且报告的成本未包含发现可处理问题本身的计算投入。全功能智能体在难题上的优势可能随大模型能力提升而减弱。