AI 系统在数学领域的进展迅速，但衡量这种进展十分困难。已有的已解题目基准会出现饱和现象，而开放题目基准每个问题只能被首次解决一次。我们提出 SqueezeBench，一种能够抵御饱和的基准：每一次成功都会提升门槛，而不是移除问题。\ \ 每个问题固定一个整数函数 $f(n)$，其值仅在小的 $n$ 上已知。基准维护该函数的下界和上界记录。记录本身是可计算的 Lean 函数，并附带机器检验的证明，表明它界定了 $f$。提交者需要提供一个新函数并证明：它在所有 $n$ 上不劣于当前记录，并且在某些 $n$ 上严格更好。若被接受，新函数即成为下一轮需要击败的记录。系统因此同时选择界限及其证明，能够在单个 $n$ 上或在增长率上改进记录。\ \ 在每个 $n$，上下界之间的差距反映了已认证界限离确定 $f(n)$ 的距离。所有证明均由两个独立的 Lean 核心检查，无需人工审稿。检查还会拒绝通过在小 $n$ 上穷举搜索得到 $f$ 的函数，维护者只需阅读提交报告并关注更大 $n$ 的搜索情况。我们公开了十个极值组合学问题、二十条已证明的初始记录以及相应的提交工具。作为基线，使用前沿语言模型的代理在每条记录最多一小时的限制下提交了 82 条被接受并改进了所有记录，但未超出已发表文献。随后使用两种更新模型的代理在这些记录基础上又提交了 60 条，被接受并再次改进了 20 条记录中的 19 条。十个问题中有八个的至少一条记录仍在渐近上落后于最佳已发表界限。\ \ 点评