寻找短证明中的错误：解析下界的元数学

我们研究证明复杂度下界的 refuter 问题。假设 $\varphi$ 是一个不承认长度为 $s$ 证明的困难 tautology，即在某个证明系统 $P$ 中不存在长度为 $s$ 的证明。在对应的 refuter 问题中，我们获得（查询访问权限的）一个声称证明 $\varphi$ 的长度为 $s$ 的证明 $\pi$，我们的目标是在 $\pi$ 中找到无效的推导步骤。正如有界算术中的 witness 定理所暗示的，refuter 问题的计算复杂性与底层下界的元数学密切相关。我们聚焦于对应于解析下界的 refuter 问题，因为解析是证明复杂度中最被广泛研究的系统。为捕捉解析下界（规模）refuter 问题的复杂性，我们引入了一个新的类 $\mathrm{rwPHP}(\mathsf{PLS})$，它属于决策树 $\mathsf{TFNP}$ 中，可以视为 $\mathsf{PLS}$ 的随机版本。在有界算术中解释时，我们的结果表明，理论 $\mathsf{T}^1_2(\alpha) + \mathrm{dwPHP}(\mathsf{PV}(\alpha))$ 刻画了证明（最简单的）解析规模下界所需的“推理力量”。作为一个推论，我们获得了令人惊讶的解析下界的有效证明。特别是，我们表明许多解析规模下界可以用低宽度的随机解析 [Pudl\'ak--Thapen, CCC'17] 证明。