‘Moravec’s Paradox’ notes that computers find the hard stuff easy. No surprise, then, that when human get pushed out of the loop it often happens from the top.

The case of mathematics is especially significant:

*Computer-assisted proofs (both at the level of formulation and at the level of verification) have attracted the interest of a number of philosophers in recent times (here’s a recent paper by John Symons and Jack Horner, and here is an older paper by Mark McEvoy, which I commented on at a conference back in 2005; there are many other papers on this topic by philosophers). More generally, the question of the extent to which mathematical reasoning can be purely ‘mechanical’ remains a lively topic of philosophical discussion (here’s a 1994 paper by Wilfried Sieg on this topic that I like a lot). Moreover, this particular proof of the Kepler conjecture [see New Scientist link] does not add anything substantially new (philosophically) to the practice of computer-verifying proofs (while being quite a feat mathematically!). It is rather something Hales said to the New Scientist that caught my attention (against the background of the 4 years and 12 referees it took to human-check the proof for errors): “This technology cuts the mathematical referees out of the verification process,” says Hales. “Their opinion about the correctness of the proof no longer matters.”*

Since computer software became chess-competent we’ve been told that the idea chess is difficult was just an illusion. When we start hearing that about mathematics in general, it will really be time for the dark laughter to begin.