Backgound and Motivation:

Leibniz dreamed of mechanising reason and mathematics but didn't have the wherewithall. Lots of people still want to do it, and think logic, computers and a bit of graft will do the trick.

A Short History of Rigour in Mathematics Formalisation is a stage in the evolution of standards of rigour in mathematics. The Formalisation of Mathematics During the period from about 1821 to 1908 mathematicians restored and surpassed the standards of rigour which had been established during the period of classical greek mathematics but neglected during the mathematisation of science.

Formality and Rigour in 20th Century Mathematics Early in the 21st century two unprecedented problems were outstanding which still remain with us. Both reflected the unmanageable complexity of doing mathematics in practice to the best known standards of formal rigour. Formalised Mathematics This excellent paper by John Harrison provides a wealth of background and motivation.

The QED Manifesto A proposal concerning the formalisation of mathematics. Lots of enthusiastic rhetoric and some more detailed ideas. (a critique) Math by Proof - What is it, and why should we? UK funding? MathFit, MathKit

Formal Foundations:

This whole enterprise depends upon the fact that mathematics can be reduced to logic. So you need to know what a formal logical foundation system is.

Logicism Logicism is the philosophical doctrine that mathematics is or is reducible to logic. You don't have to swallow this, but it helps.

Formal Foundations Whether logicism is true or false the best logical basis for the formalisation of mathematics is a formal foundation system.

Developing Formal Maths:

A first goal is to be able to productively develop mathematical theories, in collusion with computers, with all theorems and proofs formal and machine checked.

This is what AUTOMATH was about, its what Mizar is now being used for, and its what the QED manifesto seems mainly concerned with. Its not so hard to do but it doesn't get used by many mathematicians (in the global scale of things) and doesn't deliver the kind of functionality which would help applications.

Some level of automation in finding formal proofs is essential because of the amount of detail in a formal proof (in traditional formalisations). Even with state of the art proof automation the process of producing a formal machine check proof is significantly more labour intensive than traditional methods of preparing proofs for journals.

Applying Formal Maths:

A more ambitious (and maybe more profitable) goal is to exploit the formal methods to get computers which are good at applied mathematics.

Proof and Computation In general proof is something which is required during the development of a mathematical theory, e.g. complex analysis. When it comes to application of the theory, proof is not generally called for. In application computations or other problem solving methods are adopted which are justified by the theoretical results previously proven. The standard of rigour adopted is perhaps slightly relaxed in applications. Machines more easily cope with a mass of formal detail, but are not so good at informal methods.

The basic idea here is that by adapting merging compiler technology and proof technology we can effect a formal mechanisation of mathematics which combines the logical rigour of proof based techniques with the levels of automation and speed realised within their domains by numerical symbolic mathematical software. This is a possible approach to the development of mathematical machine intelligence, but delivery of worthwhile functionality does not depend upon achieving artificial intelligence.

---

© created 1996/1/4 modified 1998/08/14