Two articles on formal computer proof

Two articles on formal computer proof, including Gonthier's proof of the four-colour theorem, courtesy of a summer school announcement from Bengt Nordstrom.

The Economist

On this theme I liked E.B. Davies's Whither Mathematics? which covers three crises faced by mathematicians in the twentieth century: Gödel's incompleteness theorem, the proof of the four colour theorem, and the "distributed" classification of the finite simple groups by a large number of mathematicians.

"In 1875 every suciently able mathematician could fully absorb the proof of every theorem that existed within a few weeks. By 1975, a year before the four colour theorem was proved, this was not even close to being true, but it was still the case that some mathematician fully understood the proof of any known theorem. By 2075 many fields of pure mathematics will depend upon theorems that no mathematician could fully understand, whether individually or collectively."
Post a Comment

<< Home

This page is powered by Blogger. Isn't yours?