There is a nice article by Dana Mackenzie in Science magazine about computer mathematics. There is also an okay article in The Economist. Reading them will give you an idea of what I work on.
The world of mathematics has changed. These are the first two articles that mention this change.
This week I have the pleasure of having Georges Gonthier visit our group. Georges Gonthier has completed a computer verified proof of the four-colour theorem. The previous proofs of the four-colour theorem have been a combination of traditional combinatorial reasoning and a computer program to perform a billion case analysis. It can be hard to accept such proofs because it is hard to be reasonably certain of the correctness of the software that does the case analysis. Georges’s proof is different. His proof is written in Coq. Coq is a unified language for both writing proofs and writing programs. In this language Georges writes the combinatorial proof, he writes the program for the case analysis, and he proves the program is correct. All details of the entire proof is checked by the computer all the way down to the logical foundations.
Once one trusts the proof checking software, one needs to check that the statement being proved is actually the statement being claimed. This can potentially be difficult. The characterization of planar graphs can be complicated, but Georges goes even further by also giving a clear topological characterization of the four-colour theorem. A map is a list of disjoint open connected subsets of ℝ². Two sets (countries) are adjacent if their boundaries share at least two points. Any such map is four colourable.
The combinatorial proof is entirely constructive. Going from the above topological statement to the combinatorial statement requires classical reasoning.
The four-colour theorem, once questioned, has now been checked to a higher standard than most mathematical proofs. This only the beginning. This proof will be followed by a computer verified proof of the Kepler Conjecture, and then by a computer verified proof of classification theorem of finite groups. With the most complex proofs being held to such a high standard, regular proofs will be held to the same standard. Soon all mathematical proofs will be required to be verified by a computer before being accepted.