[Math] Algorithmic complexity of formal proof verification

computational complexitylo.logicproof-assistantsproof-theory

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 to True if its argument is positive, and evaluates to False otherwise. The size of a proof of is_positive is constant (it's just a proof of True when is_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 of is_positive$2^n$ take time exponential in $n$. Here is the Coq code:

(** Define a version of [+] which is recursive on the right argument. *)
Fixpoint plusr (n m : nat) {struct m} : nat :=
  match m with
    | 0 => n
    | S m' => S (plusr n m')
  end.
(** Define a version of [*] which is recursive on the right argument. *)
Fixpoint multr (n m : nat) {struct m} : nat :=
  match m with
    | 0 => 0
    | S m' => plusr n (multr n m')
  end.
Fixpoint pow (base exponent : nat) {struct exponent} : nat :=
  match exponent with
    | 0 => 1
    | S e' => multr base (pow base e')
  end.
(** Test [pow] *)
Compute pow 1 2. (* 1 *)
Compute pow 2 3. (* 8 *)
(** Return [True] if a number is [S _], [False] if it is [0] *)
Definition is_positive (n : nat) : Prop :=
  match n with
    | 0 => False
    | S _  => True
  end.
Time Check I : is_positive (pow 2 9). (* 0.09375 *)
Time Check I : is_positive (pow 2 10). (* 0.40625 *)
Time Check I : is_positive (pow 2 11). (* 1.875 *)

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).

Related Question