根據挑戰賽網站，一項新的開放數學挑戰賽正邀請人類與 AI 代理人證明更緊緻的界，讓 STARK 證明能執行更少的檢查並縮小體積。

該項目以 provably.fast 工作坊形式運作，程式碼託管於 starknet-innovation GitHub 組織之下——這一細節將該計畫置於 Starknet 生態系之中，STARK 證明在該生態系被用於以輕量級檢查驗證大量運算。

STARK 是僅依賴雜湊函數的零知識證明。由於驗證者必須執行的每次查詢都會為每項檢查增加數據與工作量，這些查詢背後的界在證明系統中備受關注。挑戰目標是 Reed-Solomon 接近性測試中「壞挑戰」的數量，這決定了驗證者需要執行多少次查詢。目前已知界來自 Dao、Kominers 與 Thaler（2026）。

三個目標，於 Lean 中驗證

網站列出三個目標，包括以線性界取代已知的二次界，以及在更寬的範圍內證明二次界。每個命題均以 Lean 定理證明器固定表述，且只有在獨立審查的證明完成後，該目標才被視為解決，功勞歸於完成證明的人類或 AI 代理人。將命題固定於 Lean 中消除了何為解的模糊性，而將功勞延伸至 AI 代理人，則使這項挑戰成為對機器能否與人類參賽者共同貢獻研究級數學的具體檢驗。

網站指出，僅有更緊緻的界並不會縮小任何東西；實際的節省還需要完整的協定分析。這一提醒界定了值得關注的方向：三個目標是否有人達成，以及後續的協定工作能否將新的界轉化為可測量的更小證明。

資料來源：CryptoBriefing