[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: sacook@cs.toronto.edu*Subject*: Re: FOM: computer proofs*From*: Randy Pollack <pollack@dcs.gla.ac.uk>*Date*: Wed, 2 Dec 1998 18:42:56 GMT*CC*: fom@math.psu.edu*In-reply-to*: <98Dec2.101739edt.15577-23704@dvp.cs.toronto.edu> (message from Stephen Cook on Wed, 2 Dec 1998 10:17:38 -0500)*Sender*: owner-fom@math.psu.edu

Let me mention (again) my paper that touches on many of these points: @InProceedings{Pollack:belief, author = {Robert Pollack}, title = {How to Believe a Machine-Checked Proof}, booktitle = {Twenty Five Years of Constructive Type Theory}, editor = {Giovanni Sambin and Jan Smith}, year = 1998, publisher = {Oxford University Press} } Also available from <http://www.brics.dk/~pollack/export/believing.ps.gz>. There is a distinction between 2 kinds of computer proofs that has not been clear in the recent FOM discussion. In one kind of computer proof, we use a computer to syntactically check a (more or less explicit) derivation in a given formal system. Usually, a user gives some commands that a system like Mizar "compiles" into atomic steps of a formal system. (Of course, allowing reference to already proved statements.) Mizar claims to check a particular formal system, but doesn't actually construct a representation of the formal proofs it checks. Some proof systems such as Mike Gordon's HOL do, implicitly, construct such a proof. Taking it even further, my own proof checker, LEGO <http://www.dcs.ed.ac.uk/home/lego/> constructs explicit representations of proofs in the Extended Calculus of Constructions (ECC), which can be independently checked without knowing anything about the internal structure of LEGO. As long as you know the inference rules for ECC, you can check a proof yourself, or write your own computer program to check such proofs. Such an independent checking program only needs to syntactically check a particular formal system, i.e. a few axioms and rules. No matter how long the _proof_ to be checked, the proof checker is a simple program, much simpler than many informal mathematical proofs in textbooks. I am not claiming "absolute certainty" here, I'm comparing complexities. The implementation of such a proof checker may use machine arithmetic to implement the syntactic check of the given formal system, but if the proof being checked involves arithmetic, it will be the formal arithmetic defined in the formal system, and will not call machine arithmetic to execute the steps directly. The second kind of computer proof is like the 4CT proofs discussed on this list. Some informal algorithms are programmed and executed on a computer. These may be long, complicated and subtle algorithms (if the necessary computation is very long, there will be much optimization of the program), which makes it hard to believe. Also we are expecting that the semantics of the computer to match some informal mathematical foundation. For example, the [Robertson, Sanders, Seymour] quote posted by Steve Cook says > ... our programs use only integer arithmetic, and so we need not be > concerned with round-off errors and similar dangers of floating > point arithmetic. But it still depends on correct integer arithmetic, perhaps arbitrary precision, etc., as implemented in hardware. Finally I agree entirely with Sazonov's point "that any formal mathematical proof should have intuitively feasible length". In fact proof checkers of the first kind, that actually construct a representation of a proof, seem to enforce this requirement. So much so that the business of completely formal mathematics (or "explicit mathematics") is largely finding formal systems that we believe and that support proofs of feasible length. -- Randy Pollack <http://www.dcs.gla.ac.uk/~pollack/> Computing Science Dept. <pollack@dcs.gla.ac.uk> University of Glasgow, G12 8QQ, SCOTLAND Tel: +44 141 330-6055

**References**:**Stephen Cook**- FOM: computer proofs

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]