轻量级自动化AI流水线能解决研究级数学问题吗？

大语言模型（LLM）最近在生成严格的数学证明方面取得了显着的成功，“数学人工智能”成为一个充满活力的研究领域。虽然这些模型已经掌握了国际数学奥林匹克等竞赛级别的基准，并通过自动形式化在研究应用中显示出前景，但它们通过轻量级、自然语言管道来解决研究问题的部署仍未得到充分探索。在这项工作中，我们证明了下一代模型（例如 Gemini 3 Pro、GPT-5.2 Pro）在集成到针对基于引文的验证而优化的简化自动化管道中时，可以解决复杂的研究级问题。我们在两个新颖的数据集上评估我们的流程：(1) 由顶尖数学家提出的 ICCM 问题集（相当于丘成桐大学生数学竞赛），以及 (2) “第一个证明”问题集，由以前未发表的研究问题组成。我们的管道为前两个 ICCM 集和“第一个证明”集中的所有问题生成了候选证明。前两套 ICCM 和“第一证明”套中问题 4 的解决方案已经经过我们团队的充分验证。所有生成的证明都已提交给官方组织，我们生成的结果是公开的。我们计划在适当的时候开源完整的管道方法。