Ramanujan挑战赛结果：多格式证明的AI辅助评估流程

论文提出多格式证明AI评估流程，并报告误判率下降。

资讯摘要

论文分析Ramanujan挑战赛提交，该基准由数论研究级问题构成，含未发表结果与开放猜想。作者比较不同AI模型、计算机代数系统与形式化工具的表现，发现与官方解法概念不同的正确提交，以及一个已发表开放猜想的证明。针对大规模可靠评判复杂证明的难题，论文提出覆盖自然语言证明、CAS代码与Lean形式化的AI辅助评估流程，作者报告自然语言证明误判率由23%降至6%，支撑代码判断准确率由46%升至58%。

要点速读

1. Ramanujan挑战赛包含数论研究级问题，涉及未发表结果与开放猜想。
2. 分析发现与官方解法概念不同的正确提交，以及一个已发表开放猜想的证明。
3. 论文提出的AI辅助评估流程报告自然语言证明误判率从23%降至6%，代码判断准确率从46%升至58%。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/31 08:00:18（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。