Last Person Standing
Posted by David Corfield
Tim Gowers is engaged in a new venture in open source mathematics. As one might expect from a leading representative of the ‘problem-solving’ culture, Gowers has proposed a blog-based group problem solving challenge.
He motivates his choice of problem thus:
Does the problem split naturally into subtasks? That is, is it parallelizable? I’m actually not completely sure that that’s what I’m aiming for. A massively parallelizable project would be something more like the classification of finite simple groups, where one or two people directed the project and parcelled out lots of different tasks to lots of different people, who go off and work individually. But I’m interested in the question of whether it is possible for lots of people to solve one single problem rather than lots of people to solve one problem each.
Coincidently, Alexandre Borovik, my colleague on the A Dialogue on Infinity project, came to Kent on Wednesday and spoke about the classification of finite simple groups in his talk ‘Philosophy of Mathematics as Seen by a Mathematician’. Alexandre expressed his fears that parts of mathematics may be becoming to complicated for us. He considered the classification of finite simple groups, whose proof is spread over 15000 pages. There is a project afoot to reduce this to a ‘mere’ 12 volumes of around 250 pages each, so 3000 pages. But these will be extremely dense pages, not at all the kind of thing people will find it easy to learn from.
So what happens when the generation of mathematicians involved in the classification project retires? Apparently, Inna Capdeboscq is the youngest person out of the few people who understand things thoroughly enough to repair any discovered breaches in the proof. Alexandre estimated that in twenty years she will be the last such non-retired mathematician in the world. He doubts any youngsters will take on the baton.
Now is this a (belated) bout of turn of the century pessimism, or is there some intrinsic complexity in the classification which cannot be compressed? Do we have examples of long proofs from earlier times which have been enormously simplified, not just through redefinition?
On a positive note, Alexandre mentioned something we’ve discussed before at the Café, that a radical rethink of this area may be possible. Recall the suggestion that some of the sporadic simple groups are flukes, and should rather be seen as belonging to a larger family, some of whose members ‘happen’ to be groups.
Monstrous moonshine is associated with many of the sporadics, and there is evidence for the participation of some of those thought to be outside its scope – the pariahs. All this ties in with a
fantastic amount of mathematics, so just possibly new ideas will emerge to allow for the classification of the larger family.
However, I had the impression from Alexandre that none of this will help enormously simplify the original classification. So I wonder what would be the effect on future mathematicians using the result if there was nobody left alive who understood it fully. Would it be used with misgiving?
Re: Last Person Standing
I was extremely intrigued by Freek Wiedijk’s article on the computerization of formal proof-checking in the December 2008 issue of the Notices, in which he suggests that
Perhaps this may provide an answer? Certainly in the particular case of finite simple groups, the timing seems unlikely; it would probably require some youngsters to take on the massive project of understanding and formalizing the proof even once formalization becomes tractable. But at least in principle, having a long proof completely formalized could enable us to continue using it with confidence even after no living human fully understands it any more.