拉马努金挑战赛上线：用 AI 证明数学常数公式
研究者发布「拉马努金挑战」，邀请 AI 证明 π、e、卡塔兰常数等公式，分加密待证与未证两类型，截止 8 月 1 日。
一项名为「拉马努金挑战」（The Ramanujan Challenge）的新基准在 Hacker News 亮相，旨在检验当下 AI 系统解决研究级数学问题的能力。该挑战围绕 π、e、卡塔兰常数及黎曼 ζ 函数特殊值等经典数学常数的显式公式设计题目，要求参与者用 AI 或人工方式给出可被数值验证的证明。
题目设计：加密待证与未证双轨
挑战的题目列表分两类：一类公式的证明已被作者掌握，但会在初始阶段被加密、不公布思路；另一类是尚未被证明的开放命题。组织者表示，这种设计既能评估 AI 对已知非平凡证明路径的还原能力，也能检验其在开放猜想上推进数学的能力。为避免验证过程变得不可控，所有题目都可通过高精度数值计算直接核实结果。
提交形式：三类方案按优先级排序
组织者明确了三类可接受的提交形式，按优先级依次为：
- 形式化证明：使用 Lean、Rocq、Isabelle 等交互式定理证明器书写，需附带对主要证明模块、定义与引理的注释与直觉说明。
- CAS 可复现推导：基于 Mathematica、Maple、SageMath、Magma、PARI/GP、SymPy、RISC 软件包或 ramanujantools 等成熟的计算机代数系统，代码需显式暴露符号推导步骤。
- 人类可读证明：以传统数学文本呈现，因评估耗时会显著更长，仅在条件允许时予以审核。
任何依赖代码完成的非平凡数学步骤都必须随提交公开、可读、文档齐全，并提供 solution.tex 或 solution.pdf 文件说明人类可读的推导过程。
时间安排与工具限制
挑战将于 2026 年 7 月 1 日正式发布，截止时间为同年 8 月 1 日 23:59 UTC。组织者强调，所使用的任何符号计算系统或数学库必须在 7 月 1 日前已公开发布，以避免评测沦为对新生成数学软件的测试。在挑战期间新写的代码可作为解题脚本，但包括 AI 生成代码在内，都不会被视为可信外部预言机，提交不得依赖隐藏的远程服务、私有 API 或不可复核的计算。
公开讨论与结果公布
组织者鼓励参与者就挑战展开公开讨论，但为维护评测的公正性，要求在 8 月 1 日前不要公开完整解答。若题目出现歧义或印刷错误，组织者会在挑战网站发布勘误，提交结果将以更正后的官方题面为准。评审期结束后，组织者将逐题公布各提交是否被接受、属于部分接受，以及使用了哪些工具或 AI 系统；针对开放猜想的有效证明将被视为新的数学贡献，按提交顺序公布解法并署名致谢。已有参与者于 7 月 1 日起陆续提交方案，首批 SHA-256 哈希记录显示，名为 Robert Sneiderman 的提交者率先在挑战开放数小时内提交了三份解答。