Understanding reasoning by analogy in mathematics in an effort to automate it could enrich both mathematics and artificial reasoning systems
In 1997, an IBM computer named Deep Blue beat Gary Kasparov, the reigning chess champion. In 2011, a computer named Watson beat the two top quizzers on a leading quiz show called Jeopardy. Is it time for a computer to win a Fields Medal — the top prize in mathematics?
Tarski vs EQP
At the root of mathematics are integers — which we can add, multiply and negate. These operations satisfy certain axioms, such as commutativity (order does not matter), associativity (which addition is performed first does not matter), distributivity, etc.
Computers, instead, store information in bits, each of which is either TRUE or FALSE at any time. In place of addition, multiplication and negation are the logical operations AND, OR and NOT. These satisfy certain axioms. The corresponding algebra for bits is called Boolean Algebra.
In 1933, Herbert Robbins proposed a set of axioms from which he conjectured that the usual axioms for a Boolean Algebra could be deduced. Though many leading mathematicians worked on this, this conjecture remained unsolved until 1996, an year before Deep Blue beat Kasparov. Remarkably, it was solved then not by a virtuoso logician but by a computer program called EQP, through a long chain of deductions. At that time it took several days of computing, but today the successor of EQP (called PROVER9) can prove the result in a fraction of a second on a personal computer.
Kepler and Sphere packings
The year after Deep Blue's victory saw a celebrated computer-assisted proof in mathematics — Thomas Hales's proof of the Kepler conjecture. This concerns packing spheres (say apples) in as efficient a way as possible. In 1611, Johannes Kepler had conjectured that the two obvious ways: with each layer arranged in squares or hexagons, are the most efficient. Hales proved this in 1998, using computer calculations for checking a huge number of cases.
Referees for the Annals of Mathematics (the leading mathematics journal) eventually said they were 99 per cent certain of the correctness of the proof — surely a quibble as various conventional papers (including at the Annals) turn out to be wrong, though referees have accepted them without such elaborate caveats.
Hales responded to this by giving a computer-verifiable proof of the Kepler conjecture!
Who guards the guards?
On the face of it, it seems unlikely that those who do not trust software will be convinced by having it checked by other software. But computer proof systems have an elegant way around this circularity. At the heart of such a system is a small trusted core, about 500 lines of code which can (and are) verified independently by several experts — and any sceptic who so wishes. This core then checks the rest of the system, so we can be sure of its correctness. A computer-verifiable proof is then checked by the proof system.
Such an approach has become widespread in hardware and software verification — with the leading chipmakers using this to verify operations of their processors.
Can we formalise proofs?
Writing (or even reading) a fully formal proof of a theorem (that is , a proof in terms of the rules of logic) is a nightmare. However, computer proof systems have powerful automatic deduction engines built into them. Hence, as with ordinary human manuscripts, routine details can be omitted. The computer (unlike a human reader) will, however, actually check the details. Further, in some computer proof systems, proofs can be written in a language resembling ordinary human proofs. We can thus hope to start with some trusted axioms — say those of set theory or arithmetic — and build the rest of mathematics on this core. There are indeed some celebrated results with such computer-verifiable proofs, including the Kepler conjecture and the so-called four-colour problem (which says that a map can be coloured with at most four colours so adjacent regions have different colours).
Further, there are fundamental results in mathematics (developed without computer assistance) whose proofs are viewed with scepticism. A notorious case is the classification of finite simple groups, whose proof is scattered in the literature and possibly even incomplete. Georges Gonthier is leading a program to give a computer-verifiable proof of this result.
Holmes, Watson and beyond
Computers can thus beat humans at calculation and deduction (a la Sherlock Holmes). However the practice of mathematics involves other ingredients, notably searching the literature and reasoning by analogy.
Searching the literature can be facilitated by either writing more computer-verifiable (hence computer-understandable) proofs, or by a Watson-like computer actually managing to understand human proofs — indeed the first commercial application of Watson is understanding the medical literature to help doctors make diagnoses. Analogy lies much deeper and is more mysterious.
An analogy engine?
Why should one care about computers solving mathematical problems? Probably the most practical reason is the same that led to building Deep Blue or Watson — a system capable of winning mind games is also capable of solving real life problems. Indeed mathematics, strongly constrained by rigour and aesthetics but free from practical constraints, has proved to be an extraordinary generator of useful concepts for science and engineering. One can hope that a focus on doing mathematics will similarly drive computers to new heights.
From a mathematician's point of view, attempting to formalise proofs — better still to automate their discovery, should lead to a deeper understanding of many aspects of mathematics.
Indeed, understanding reasoning by analogy in mathematics, in an effort to automate it, could enrich both mathematics and artificial reasoning systems.
(The author is an Associate Professor in the Department of Mathematics, Indian Institute of Science, Bangalore.)