There are 4 articles in the Special Issue:

- Formal Proof, by Thomas Hales
- Formal Proof - The Four-Colour Theorem, by Georges Gonthier
- Formal Proof - Theory and Practice, by John Harrison
- Formal Proof - Getting Started, by Freek Wiedijk

However, having mathematics become utterly reliable might not be the primary reason that eventually formal mathematics will be used by most mathematicians. Formalisation of mathematics can be a very rewarding activity in its own right. It combines the pleasure of computer programming (craftsmanship, and the computer doing things for you), with that of mathematics (pure mind, and absolute certainty). People who do not like programming or who do not like mathematics probably will not like formalisation. However, for people who like both, formalisation is the best thing there is.Clearly, formalisation is "geek heaven"!

The Wikipedia page on Formal Proof is a useful place to start learning the basic concepts. Informally, the idea of "formal proof" is that you replace error-prone human mathematicians by error-free computers, which are then used to expand each step of a (human-generated) proof all the way down to the fundamental axioms of mathematics. Naturally, this leads to extremely verbose formal proofs, but computers are ideally suited to handling this verbosity, and the advantage for us humans is that we can ensure that our proofs are error-free, because they have been checked by computer in every detail. Of course, we might have neither the time nor the inclination to fully "understand" the details of these proofs.

The following is a verbatim copy of the main part of a posting of mine Burden of Proof that I wrote over 2 years ago on my ACEnetica blog. It is very relevant to the issue of "formal proof" which is why I have included it here.

My own view on this issue is that a computer generated proof hasexactlythe same status as a human generated proof. The difference is only one of the degree of assistance provided to the brain of the human to help with the generation of the proof. A totally unassisted human would have to somehow do the whole proof mentally, which severely limits the length of proofs that are accessible. A human with the typical assistance that is allowed in an examination room (i.e. pen and paper) has the luxury of at least being able to write things down, which allowsmuchlonger proofs to be reliably generated. The mechanics of generating a proof then reduce to using well-defined rules to manipulate symbolic expressions, where pen and paper are used as a medium for representing these symbols, and the rules are implemented in the human brain.

The degree of assistence in generating a proof can be taken one stage further by using a computer to implement some or all of the rules for manipulating the symbolic expressions, rather than implementing all of the rules in the human brain. This seems to be a fairly radical step to take, because hitherto the only part of the proof that was "outside" the human brain was its "dumb" representation using pen and paper, whereas the "clever" bit involving the implementation of rules to manipulate this representation was "inside" the human brain.

Let us consider what these rules of manipulation actually are. Effectively, they define a procedure for taking an initial expression constructed out of symbols, and repeatedly operating on it using the rules to eventually generate the required final expression. The cleverness is in theconstructionof the set of rules, which is where a human is the best source of the cleverness needed to create the rules. There isnocleverness in the repeatedapplicationof these rules; all that is required is that their application is donereliably, which is where a computer is the best approach, especially if the proof has many steps.

Use a human todefinethe rules of manipulation, and use a computer toimplementthese rules. This approach seems to me to be entirely uncontroversial, and it is exactly how computer generated proofs are done. Note that software bugs in the computer part of the proof are dealt with in ananalogousway to "software" bugs in human part of the proof, i.e. try a variety of approaches on a variety of platforms.

## No comments:

Post a Comment