轻量级自动化AI流程能否解决研究级数学问题？

近年来，大型语言模型（LLMs）在生成严谨数学证明方面取得了显著进展，'AI for Math'已成为一个充满活力的研究领域。尽管这些模型已掌握国际数学奥林匹克竞赛等竞争性基准，并通过自动形式化在研究应用中展现出潜力，但其在研究问题上的轻量级自然语言流程部署仍鲜有探索。本文表明，下一代模型（如Gemini 3 Pro、GPT-5.2 Pro）集成到优化的基于引用验证的自动化流程中，能够解决复杂的研究级数学问题。我们在两个新数据集上评估了该流程：（1）由顶尖数学家提出的ICCM问题集（类似于丘成桐大学生数学竞赛），以及（2）包含未发表研究问题的“First Proof”问题集。我们的流程为前两个ICCM问题集和“First Proof”问题集的所有问题生成了候选证明。前两个ICCM问题集和“First Proof”问题集第4题的解决方案已被我们团队完全验证。所有生成的证明均已提交给官方组织，结果公开可用。我们计划在未来适时开源完整的流程方法。