FAR：从文献寻找问题，筛选数学发现供专家复核

AI系统越来越有能力为数学研究做出贡献。在研究实践中，前沿模型的推理是一种有限资源，而专家数学评审更为紧缺。因此，善用这些稀缺资源是让AI辅助数学发现高效的核心。在大多数当前的AI-for-math工作流中，人力集中在开头和结尾——选择合适的研究问题以及之后评审由此产生的成果。这两个环节正在成为研究级数学的瓶颈。我们通过提出一种新的人机发现范式来解决它们。人类输入不再是一个预先选定的单一问题，而是专家有兴趣、有专长的研究方向。系统随后在广泛的文献语料库中搜索该方向上的候选问题。受搜索与推荐系统启发，我们构建了Find、Attempt和Recommend（FAR），一个从文献到评审的级联，自动化搜索合适的问题，并将人类注意力集中在通过多阶段筛选的成果上。在一次组合数学试点中，该流水线从5,245篇组合数学论文出发，恢复6,453条候选猜想或公开问题，并过滤出4,717条表面上良定且仍未解决的猜想。随后的推理与自动分诊阶段产出598个可能解，并挑选77条供作者团队评审。其中，我们识别出许多有趣的发现，包括关于Davies--Jenssen--Perkins--Roberts、Erdős--Straus、Ikenmeyer--Pak--Panova和Lund--Saraf--Wolf的猜想与问题的结果。这些结果展示了这种人机协作新方式对数学发现的有效性。