FOM: Mizar proofs

[Andrzej Trybulec]

I apologize for late answer.

On Mon, 12 Apr 1999, Harvey Friedman wrote:

> I meant to ask a different question. What I meant was: what is the estimate
> on the length of formal proofs? [The time question is also interesting;
> thank you for answering it.]

In the theory of continuous lattices it seems that proofs in Mizar are
5-10 times longer.

The Knaster theorem (fixpoint for monotonic wrt
inclusion map of a power set) is about 20 lines.

The proof of the Hahn Banch theorem (for real spaces) is about 350 line.

I affraid that the information above may be misleading. The length of the
article devoted to the proof of the Hahn Banch theorem is more than
1600 lines. And a number of lemmas is proved in it that are of general
interest, e.g.

  If X is a subset of dom f and the function f is a subset of a function g
  then f|X = g|X

The proof of it is 7 lines (one of them of the form "end;", that in Mizar
means q.e.d.) In the QED Manifesto such "theorems" are called mathlore.
If we eliminated mathlore, the proofs of substantial theorems would
be longer, I cannot estimate how much longer. 

The proof of the Zermelo theorem is rather short (60 lines) 
only because earlier the the theory of ordinals had been developed.
The proof of the Axiom of Choice (using Zermelo theorem) of the
same length.

The original Tarski's proof is 43 lines long. 

> I am under the impression that the Mizar project not only gets the machine
> to accept derivations, but also creates a proof in a reasonable system, the
> details of which can be specified in advance.

I am not certain if I understand what you mean.

The proof system that we use is basically the Jaskowski system of natural
deduction. (It seems that Americans prefer to name it the Fitch-Jaskowski
system). The main difference wrt some other systems is in the fact that
local constants are allowed in proofs. Not only introduced by the Choice
Rule, but also, when we prove a general sentence, the variables bound
by universal quantifiers may be fixed on the beginning of the proof.

These proofs are written by hand (by the authors)

> E.g., how long is an appropriately formal proof of Fermat's Last Theorem?

I have no idea.

Andrzej Trybulec