In this question, suppose $S$ is some popular real-world automated proof system that is stronger than or equivalent to Peano Arithmetic. I would be happy with a positive answer to the following for any such $S$, so please feel free to cherry-pick $S$ to make that easier:
Can the validity of an $S$-proof be verified in time polynomial in the
string-length of the proof?
I've been able to find some work assessing progress in formal proof verification, such as
http://www.ams.org/journals/notices/200811/tx081101408p.pdf
but not much on the algorithmic complexity of verifying the outputs of various approaches, so I figure I must be looking in the wrong places / using the wrong search terms. Please, help point me in the right direction!
Best Answer
No, for languages based on Martin-Löf Type Theory
In proof systems based on Martin-Löf Type Theory, including Coq and Agda, proof-checking can involve evaluating arbitrarily complicated (proven-terminating) programs.
As a simple example, we can define a function
is_positive : ℕ → Prop
that evaluates toTrue
if its argument is positive, and evaluates toFalse
otherwise. The size of a proof ofis_positive
is constant (it's just a proof ofTrue
whenis_positive
is given an argument that evaluates to a numeral). However, it's relatively easy to define an exponentiation function that makes checking a proof ofis_positive
$2^n$ take time exponential in $n$. Here is the Coq code:Since numbers are stored in unary, by default, in Coq, the proof term
I : is_positive (pow 2 n)
has $\mathcal O(n)$ nodes.You could, hypothetically, output evidence of well-typedness. In the degenerate case, where your well-typedness evidence is just a trace of the execution of the typechecker, you get linear time checking in the length of trace (assuming your trace-encoding isn't eliding expensive details).
I'm uncertain about languages like HOL, which are not based on dependent type theory. It's plausible that there are some systems where proof-checking is extremely simple, and can't involve any computation. I would look at Metamath as a likely candidate, even though it's closer to machine-checked proof than automated theorem proving (and I don't know of anyone using it for things outside of pure math).