Ramanujan AI 挑战赛（一分钟阅读）
摘要
Ramanujan Machine 发起的 Ramanujan AI 挑战赛提出了十个关于数学常数显式公式的研究级问题，旨在测试 AI 系统能否生成有效的形式证明或符号推导。该挑战赛持续至 2026 年 8 月 1 日，接受形式证明、基于 CAS 的推导或附带可复现代码的人类可读证明等形式的提交。
Ramanujan AI 挑战赛旨在测试 AI 系统能否从具体公式出发，产出有效的证明或符号推导。
查看缓存全文
缓存时间: 2026/07/03 17:22
# The Ramanujan Challenge for AI
来源：https://gilkalai.wordpress.com/2026/07/02/the-ramanujan-challenge-for-ai/
## The Ramanujan challenge
Ido Kaminer 与我分享了以下关于 *The Ramanujan Challenge for AI* 的信息，我很高兴与这个博客的读者分享。挑战页面位于 ramanujanmachine.com/ramanujan-challenge (http://ramanujanmachine.com/ramanujan-challenge)；这是完整的挑战论文 (http://www.ramanujanmachine.com/wp-content/uploads/2026/07/The_Ramanujan_Challenge__Clean_.pdf)，以及 Ido 邮件中的一段引用。
> *“该挑战于今日启动，将持续到 2026 年 8 月 1 日。它包含十个关于数学常数显式公式的研究级问题，旨在测试 AI 系统是否能从具体公式出发，生成有效的证明或符号推导。我们设计的规则使挑战兼容形式化和基于代码的系统。可接受的提交包括形式证明、基于计算机代数系统 (CAS) 的推导，或附有可重现代码的人类可读证明。目标不仅是测试 AI 能否找到答案，更是测试它能否产生可被结构化验证的推导过程。”*
## [](https://gilkalai.wordpress.com/wp-content/uploads/2026/07/euler6.png)
第二个问题
相似文章
我们首次提交的 First Proof 证明
OpenAI 为 First Proof 挑战提交了证明尝试，该挑战是一项研究级别的数学竞赛，旨在测试 AI 是否能生成正确且可验证的证明。OpenAI 的内部模型成功解决了至少五个问题（共十个），展示了其在持续推理和严谨数学思维方面的显著进展。
人类在高度严谨的数学测试中仍优于AI
首次 Proof 测试评估了四种AI系统在新型研究级数学问题上的表现，其中最佳模型仅得6分（满分10分），表明当前AI在严谨推理方面仍落后于顶尖数学家。
@rohanpaul_ai: Google DeepMind 的新论文。表明人工智能现在可以搜索形式化数学证明，但仅限于精心限制的范围内……
Google DeepMind 的新论文介绍了 AlphaProof Nexus，这是一个结合了 LLM 与 Lean 证明检查器的 AI 系统，用于在受限的数学领域中搜索形式化证明。该系统解决了来自 Erdős 和 OEIS 集合的几个未解问题，展示了一种新的分工：AI 提出候选证明，验证器确保正确性。
OpenAI表示其模型在长期悬而未决的数学问题上取得了十项进展。AI辅助的发现应达到何种证明标准？
OpenAI发布了十项关于十年来无进展的数学问题的结果，引发了关于AI辅助证明验证标准的辩论。
@ChrisHayduk: https://x.com/ChrisHayduk/status/2076196217109746095
本文比较了两种用于数学问题求解的AI方法：DeepMind的AlphaProof，它在Lean证明语言中使用强化学习；以及OpenAI的原始大型语言模型，该模型在没有正式方法的情况下在2025年国际数学奥林匹克竞赛中获得金牌。