[FOM] response to Lasse Rempe-Gillen (Re: Formal verification)

[Dustin Wehr]

Lasse,

You aren't being naive at all. The problem is the Interactive Theorem
Proving community's obsession with "trusted small kernels". They are
not interested in conditional verification. If you write the kind of
computer-checkable formal proof that I think you have in mind, where
you take as assumptions theorems/lemmas that are routinely proved in
undergraduate math classes, it will be regarded as incomplete and
ignored. They aren't satisfied until everything is encoded/defined
using inductive datatypes, sets, provably-halting programs, etc.

Let me illustrate with an example. For a project not in formalized
mathematics, I wrote some code that, given
-a source file for a basic natural deduction system for (a very
superficial extension of) many-sorted FOL
generates:
-an HTML document, for reading the proof, and
-first-order theorem proving problems, which can be fed into any
first-order theorem prover that accepts TPTP's standard format
(http://www.cs.miami.edu/~tptp/), for verifying the proof.

Here's a toy example that I wrote while developing my code. It's a
proof that there are infinitely-many prime numbers:
http://www.cs.toronto.edu/~wehr/thesis/infinitely-many_primes.html

It is not acceptable in the Interactive Theorem Proving community because:
-It uses an axiomatic definition of < for the natural numbers, rather
than a definition in terms of a provably-halting recursive function.
-It takes as axioms that:
  - n! + 1 > n
  - for all n and positive m ≤ n, m divides n!
  - for all n and m > 2, if m divides n then m does not divide n + 1

One can (I hope) find a proof of that theorem in the libraries of all
the major ITP systems. To get that extra .0001% of assurance of the
correctness of the proof, you would need to:
(a) Trust that there are no serious bugs in the system. I strongly
expect that is true of Isabelle/HOL, Coq, etc. But, unlike my code and
the code used to check the resolution proofs that first-order theorem
provers spit out, you wouldn't have time to check it yourself.
(b) Check or trust that the objects used in the statement of the
theorem have been defined/encoded correctly.

I think it's fine to trust in (a) and usually fine to choose trust in
(b). The reason I mention (a) and (b) is to compare with what you need
to do to be assured of the correctness of a conditional proof that is
written in a formal but transparent mathematician-friendly syntax
(unlike most ITP systems), which is just to have a sufficiently good
understanding of the intended model of the language that you can
verify that the assumptions are true with respect to it.

-Dustin