Ramanujan Challenge 结果：面向多格式证明的 AI 辅助评估流程

随着 AI 的数学能力迅速提升，有意义的基准测试正从大学水平问题和数学奥林匹克竞赛题转向研究级数学。Ramanujan Challenge 是一个由数论领域研究级问题组成的基准测试，其中包括尚未发表的结果和开放猜想。该挑战提出了数学常数的具体公式，这些公式的正确性可以通过数值方法检验，但其证明可能需要非显然的数学知识。在本文中，我们分析了挑战提交的答案，衡量不同 AI 模型、计算机代数系统（CAS）和形式化工具的相对表现。我们发现了一些在概念上不同于官方解答的正确提交答案，并证明了一个已发表的开放猜想。对提交答案的评估还暴露出第二个挑战：如何可靠地大规模判定复杂证明。为此，我们提出了一套 AI 辅助评估流程，用于评估自然语言证明、CAS 代码和 Lean 形式化证明的语义正确性与逻辑正确性。与传统的一次性 LLM 判定相比，我们的流程将自然语言证明中的误报判定率从 23% 降至 6%，并将对辅助代码的判定准确率从 46% 提高至 58%。这一方法为大规模评估研究级数学提供了一套方法论，并有望应用于数学和科学领域的 AI。