根据挑战赛网站，一项新的开放数学挑战赛正在邀请人类与AI代理共同证明更紧的界，从而让STARK证明减少检查次数并缩小证明体积。

该项目以provably.fast工作坊的形式运行，代码托管于starknet-innovation GitHub组织——这一细节表明该工作属于Starknet生态系统的一部分，而STARK证明在那里被用于以轻量级检查验证重计算。

STARK是仅依赖一个哈希函数的零知识证明。由于验证者必须执行的每次查询都会为每次检查增加数据和工作量，这些查询背后的界在证明系统中备受关注。该挑战聚焦于Reed-Solomon接近性测试中“坏挑战”的数量，该数量决定了验证者需要执行的查询次数。目前已知的界来自Dao、Kominers和Thaler（2026）。

三个目标，在Lean中验证

网站列出了三个目标，包括用一个线性界替换已知的二次界，以及在更宽的范围内证明一个二次界。每个命题均已在Lean定理证明器中固定，只有在通过独立评审的证明完成后，目标才被视为被解决，荣誉归于完成证明的个人或AI代理。将命题固定在Lean中消除了关于何为解决方案的歧义，而将荣誉扩展到AI代理，则使这场挑战成为检验机器能否与人类参赛者共同贡献研究级数学的具体测试。

网站指出，仅凭更紧的界并不能带来任何缩减；真正的节省还需要完整的协议分析。这一提醒界定了值得关注的重点：三个目标中是否有任何一个被认领，以及后续的协议工作能否将新界转化为可衡量的更小证明。

来源：CryptoBriefing