QED：用于开放问题数学证明生成的开源多智能体系统

本文探讨 AI 能否为开放研究问题生成原创且非平凡的数学证明。尽管基准测试表现优异，但大语言模型在生成真正新颖证明方面仍面临挑战。通过系统实验，作者识别出阻碍可靠证明生成的七种失败模式，如上下文污染、引用幻觉及证明计划不稳定等。为此，提出 QED，一个开源多智能体证明系统，其架构设计直接针对上述失败模式。在五个应用分析与偏微分方程的开放问题上评估显示，QED 成功生成了三个问题的正确证明，并经专家验证为原创且非平凡。