Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs· 拉马努金挑战赛结果：多格式证明的人工智能辅助评估管道
As AI's mathematical capabilities rapidly improve, meaningful benchmarks are shifting from university-level problems and math olympiads to research-level mathematics. The Ramanujan Challenge is a benchmark comprised of research-level problems in number theory, including unpublished results and open conjectures. It presented concrete formulas for mathematical constants whose correctness can be checked numerically, while their proofs may require non-obvious mathematics. Here, we analyze the Challenge submissions, measuring the relative success of different AI models, Computer Algebra Systems (CAS), and formal tools. We find correct submissions that are conceptually distinct from the official solutions, and a proof of one of the published open conjectures. Evaluating the submissions exposed a
AI 辅助评估多格式数学证明的效果，解决拉马努金开放猜想。
- 核心方法
- 通过拉马努金挑战赛，使用AI辅助评估管道分析研究级别的数学证明问题提交。
- 适合谁读
- 研究者
- 要解决的问题
- 评估不同AI模型、计算机代数系统和正式工具在解决高等数学问题上的能力。
- 关键实验
- 分析了来自不同AI模型、计算机代数系统和正式工具的提交结果，未提供具体实验数据。
- 主要贡献
- 发现了概念上不同于官方解法的正确提交，并证明了其中一个开放猜想。
- 意义与局限
- 推动了AI在数学研究应用的发展，展示了AI解决复杂数学问题的潜力，但也暴露了评估方法的局限性。