面向AI的拉马努金挑战赛
拉马努金挑战赛旨在评估当前AI系统在数学常数公式方面的研究级问题解决能力。挑战赛于2026年7月1日至8月1日开放提交，接受形式化证明、基于CAS的推导或可读的人类证明。提交需包含可重现的代码，且不能依赖未公开的服务。
为了评估当前人工智能系统的数学能力，拉马努金机器项目发起了一项名为“拉马努金挑战赛”的竞赛。该挑战赛提供了一组关于数学常数（如π、e、卡塔兰常数以及黎曼ζ函数的特殊值）的公式，要求参赛者证明这些公式。这些问题的吸引力在于它们既具体又可通过数值进行任意精度的验证，但证明过程可能需要非显而易见的数学技巧。
挑战赛将于2026年7月1日正式开始，提交截止时间为2026年8月1日23:59 UTC。此后，组织者将评估提交的解决方案并公布每个问题的结果。挑战赛有两个主要目标：第一，测试当前AI系统在涉及数学常数显式公式的研究级问题上的表现；第二，避免杂乱且难以处理的验证过程。因此，组织者鼓励提交包含可重现的基于CAS或形式化验证代码的解决方案。
对于什么算作解决方案，组织者按优先级顺序接受了三种类型：形式化证明（使用Lean、Rocq、Isabelle等交互式定理证明器，并附带注释）、基于CAS的推导（使用Mathematica、Maple、SageMath等符号计算系统，并显式展示推导步骤）以及人类可读的证明。如果提交依赖代码完成非平凡数学步骤，则必须包含可读、有文档的代码，并作为证明的一部分。所有提交需包含solution.tex或solution.pdf文件，以及人类可读的推导过程。
挑战赛还制定了规则，例如允许使用任何在2026年7月1日前公开可用的符号系统或库，但不允许依赖新编写的数学软件、隐藏的远程服务、私有API或不可验证的计算。为增加透明度，鼓励参赛者通过指定页面提交，该页面会记录所有提交的姓名和时间戳。同时，参赛者被要求不要在此日期前公开完整解决方案，以保证评估的完整性。
组织者会在挑战赛网站上发布勘误和澄清，提交将根据修正后的官方声明进行评估。评估期结束后，组织者将报告每个问题的接受情况、部分接受情况以及使用的工具或AI系统。对于开放的猜想，任何被接受的证明都将被视为新的数学贡献，作者将按提交顺序获得荣誉。