Comment »Posted on Saturday 8 November 2008 at 9:35 pm by Jacob Aron
In Mathematics

Well, not quite, but close. Notices of the American Mathematical Society have published details of computer programs that can provide rock-solid mathematical proofs.

This is extremely important, because in maths, proof is king. You could count prime numbers (which can only be divided by one or themselves) until the proverbial cows come home, and by the time you get to one squillion – not actually a real number, but let’s say it’s pretty big – you might be satisfied to say there were an infinite number of primes. Not so the mathematician, who will only be convinced by a logical proof.

The trouble is, even in the most basic proof you have to make some assumptions of previous results in the field. It doesn’t really matter because a sufficiently advanced reader will be able skip over these leaps of logic, but some theorems become some long and complex that even without dotting all the mathematical “i”s the proof can reach hundreds of pages long.

Checking such a proof would be incredibly arduous, but for the mathematician it must be done. This is where computers come in. A computer can develop a “formal proof”, in which every single statement is checked all the way back to first principles.

We’re not even talking 1 + 1 = 2 here. The Principia Mathematica, a seminal work on the foundations of mathematics published nearly a century ago, does not reach a proof of 1 + 1 = 2 until page 379. And mathematicians use pretty small fonts.

This demonstrates how ridiculous it would be to create such a formal proof by hand. It would be like providing a full dictionary definition of each word in this blog post along with the text – madness. Yet, for mathematicians to be truly, truly sure, a formal proof is the only way to go.

The computers aren’t quite there yet. Mathematicians still have to break the proofs down before they are fed into the program, so there we’re not quite at the level where your PC can leaf through the latest mathematical journals. It is possible, however, to let the computers “explore” the mathematics on their own – and perhaps even come up with some points the humans may have missed.

Ultimately, mathematicians would like to have formal proofs of at least the most important theorems. Thomas Hales, one of the authors writing in the Notices, says that such a collection of proofs would be akin to “the sequencing of the mathematical genome”. Impressive stuff.


Sorry, comments for this entry are closed at this time.