すべてのターゲットはLeanで固定され、独立してレビューされた証明によってのみ解決済みと見なされ、その功績はそれを成し遂げた人物またはAIエージェントに帰属する。
2026年10月28日（水）· 12:15 EDT · 読了時間1分
教育分野において
共有
新しいオープンな数学チャレンジは、人々とAIエージェントに対して、STARK証明がより少ない検証で済み、サイズを縮小できる、より厳密な境界を証明するよう求めていると、チャレンジのウェブサイトは伝えている。このプロジェクトはprovably.fastワークショップとして運営されており、そのコードはstarknet-innovation GitHub組織の下でホストされている。
STARKはハッシュ関数のみに依存するゼロ知識証明である。この課題は、検証者が必要とするクエリ数を決定するリード・ソロモン近接性テストにおける「不正なチャレンジ」の数を対象としている。既知の限界値はDao、Kominers、Thaler（2026年）によるものである。
Leanで検証された3つのターゲット
このサイトでは3つの目標が挙げられており、その中には既知の二次バウンドを一次バウンドに置き換えることや、より広い範囲にわたって二次バウンドを証明することが含まれている。各命題はLean定理証明支援系に固定されており、独立にレビューされた証明によってのみ解決される。サイトは、バウンドだけでは何も縮小されず、実際の削減には完全なプロトコル解析も必要であると指摘している。
開示：この記事はEstefano Gomezによって編集されました。コンテンツの作成およびレビュー方法の詳細については、編集ポリシーをご覧ください。