This paper on universal search mentions (on pp. 6-7) that proof checking can be done in $O(n^2)$ where $n$ is the length of the proof. Is this optimal? I don't want to specify the problem too precisely at the risk of excluding a useful interpretation, but for example if we take plain first order logic with some quickly computable set of axioms like ZFC, then checking time is dominated by substitution verification (which is linear time) for the linearly many proof steps, hence the quadratic bound, and I am fairly sure there are proof sequences that exercise this bound, where we substitute $O(n)$ many slightly different variations on an $O(n)$ sized formula.
But I don't know if I am baking in too many assumptions about how a proof system must work, and I would like a lower bound that considers arbitrary alternative proof encodings, as long as they can do something equivalent to "FOL + axioms" proof verification.
More formally, let us fix an effectively computable FOL theory $T$ (like ZFC), and a standard (effectively computable) encoding of formulas as bitstrings. Let's call the algorithm above, using a sequence of formulas and substitution, the "baseline algorithm" $B$.
The input to the algorithm $A$ is consists of two parts: $(\phi, p)$ where $\phi$ and $p$ are bit strings of lengths $k$ and $n$ respectively (where $k\in O(n)$), and $\phi$ encodes a formula in the language of $T$. We will say that $A$ is a verifier for $T$ if $\phi$ is a theorem of $T$ if and only if there exists some $p$ such that $A$ accepts $(\phi,p)$. What is the best lower bound on $A$'s time complexity?
Edit: In fact, we need more than this, because a proof verifier can get an artificial leg up by being too picky. If it rejects all proofs then it is not equivalent to $T$, but it might reject all proofs that are not of size at most $\sqrt n$ suffixed by $n-\sqrt n$ zeros; in this case it can appear to be linear time since the actual proof content is only $O(\sqrt n)$. So we add a constraint that for every $B$-proof $q$ of $\phi$ (that is, algorithm $B$ accepts $q$ as a proof in its own format), we can compute (in $o(n^2)$) an $A$-proof $f(q)$ of $\phi$ which is at most a constant factor longer than $q$.
Edit 2: For the sake of concreteness, I will specify algorithm $B$ a bit more. It is intended to be a standard proof algorithm but augmented with conservative techniques to make it not obviously suboptimal. (There are probably additional mechanisms I am missing.)
Each step either constructs a formula using a formula constructor like $\to$ or $\neg$ and formulas constructed in previous steps, or is an application of a primitive inference rule to theorems constructed in previous steps, or is an axiom. We assume that every formula is constructed at most once, and take advantage of this to make formula equality testing $O(1)$. Proofs that do not satisfy this property can be spuriously rejected, but proofs can be "deduplicated" in $O(n\log n)$ so this is not a severe restriction.
An example of a proof which takes $O(n^2)$ to check with this algorithm is (using PA as the FOL axiomatization):
- Let $A_n:=\forall x, S^n(x)\ne 0$
- We prove $A_{n+1}$ from $A_n$ by instantiating $x$ to $S(x)$, and $A_1$ is an axiom.
Now there are $\Theta(n)$ many subformulas involved in all the $A_n$ put together, and $A_{n+1}$ is proved from $A_n$ using $\Theta(1)$ steps, so the entire proof is $\Theta(n)$ large ($\Theta(n\log n)$ if you include the size of the numbers in the backreferences, omitted in the word-RAM model). However, each time we substitute $S(x)$ for $x$ in $S^n(x)\ne 0$ we must traverse the stack of successors, which takes $\Theta(n)$ time, so the overall proof is $\Theta(n^2)$.
