面向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系統。對於開放的猜想，任何被接受的證明都將被視為新的數學貢獻，作者將按提交順序獲得榮譽。