AIのためのラマヌジャンチャレンジ
ラマヌジャンチャレンジは、数学定数の公式に関する研究レベルの問題を解くAIシステムの能力を評価する競技です。2026年7月1日から8月1日まで提出を受け付け、形式証明、CASベースの導出、または人間が読める証明を受理します。再現可能なコードが必要で、非公開サービスは禁止されています。
AIシステムの数学的能力を評価するため、ラマヌジャンマシンプロジェクトは「ラマヌジャンチャレンジ」を開始します。このチャレンジでは、数学定数（π、e、カタラン定数、リーマンゼータ関数の特殊値など）に関する一連の公式が提示され、参加者はそれらの証明を行うことが求められます。これらの問題は、具体的で数値的に任意の精度で検証可能でありながら、証明には非自明な数学が必要となる可能性があるため、AI評価に適しています。
チャレンジは2026年7月1日に開始され、提出期限は2026年8月1日23:59 UTCです。その後、主催者は提出された解答を評価し、各問題の結果を報告します。このチャレンジには2つの目的があります。第一に、現在のAIシステムが数学定数の明示的な公式に関連する研究レベルの問題を解決できるかどうかをテストすること、第二に、非構造化で過剰な検証プロセスを回避することです。そのため、再現可能なCASベースまたは形式的に検証されたコードを含む提出が推奨されます。
提出が認められる解答の種類は、優先順位の高い順に以下の3つです。形式証明（Lean、Rocq、Isabelleなどの対話型定理証明器を使用し、各主要な証明ブロックにコメントを付ける）、CASベースの導出（Mathematica、Maple、SageMathなどの確立された数式処理システムを使用し、導出に使用した記号的ステップを明示する）、人間が読める証明。非自明な数学的ステップにコードを使用する場合、そのコードは読みやすく、文書化され、証明の一部として正当化される必要があります。提出されたコードには、結果を再現するために必要なソースファイルと適切なインライン文書が含まれていなければなりません。
使用できるシンボリックシステムやライブラリは2026年7月1日以前に公開されたものに限ります。新たに書かれたコード（AI生成コードを含む）は信頼できる外部オラクルとしては扱われず、隠れたリモートサービスやプライベートAPI、検証不可能な計算に依存することはできません。透明性を高めるため、すべての提出は指定ページを通じて行うことが推奨され、提出者の名前とタイムスタンプが記録されます。参加者は完全な解答を2026年8月1日より前に公開しないよう求められます。
問題文に曖昧さや誤りが見つかった場合、主催者はチャレンジウェブサイトで訂正を発行します。評価期間終了後、主催者は各問題について、どの提出が受理されたか、部分的なものか、どのツールやAIシステムが使用されたかを報告します。未解決の予想については、受理された証明は新しい数学的貢献として扱われ、提出順に著者に名誉が与えられます。