Massive Open Collaboration In Math Declared a Success 60
nanopolitan writes "In late January, Tim Gowers, a Fields Medal winner at Cambridge University, used his blog for an experiment in massive online collaboration for solving a significant problem in math — combinatorial proof of the density Hales-Jewett theorem. Some six weeks (and nearly 1000 comments) later, Gowers has declared the project a success, and some of the ideas have already been written up as a preprint."
Too bad he used a blog (Score:3, Interesting)
What he really needed is a threaded message board ala Slashdot.
Why now? (Score:2, Interesting)
It would have been nice, had this been posted before they declared success.
Now all we have is a blog post with a gazillion comments, and all the interesting work has already been done.
Maybe next time we can all join the fun?
Re:halp! (Score:2, Interesting)
Not sure about the density Hales-Jewett theorum, but the method used seems simple enough. The problem he is trying to tackle is not one of determining a proof for the problem, but rather establishing that there either exists a proof for the problem given a set of parameters or does not exist a proof given those same parameters.
To me, it is this problem which seems to be the more useful, at least in general. Basically, if it is possible, through herustics (which is essentially all you're doing by hunting through possibilities thrown out by the combinatorial logic), to determine if a solution must exist (or must not exist) to a given problem given constraints, we can use the same approach to solve quite a number of "there exists"-type problems herustically.
In the case of Linux, this would suggest that if you can define tight enough constraints on a given module (the equivalent of the constraints imposed in the original problem), it should be possible to prove whether or not an arc exists through that module which would violate the constraints without having to find that arc .
If an arc exists that would violate the constraint, that would be the same as finding a "good reason" why the constraints will not work in the original problem addressed in TFA.
This would seem to offer an approach to verification of even fairly complex software, without having to clear all of the hurdles raised by formal software proofs. If you don't have to find the buggy arc, only show that such an arc must exist, then you can use this to identify areas in the code which need fixing.
Since you can bisect any code and then test each of the subcomponents, you can narrow down which blocks of code are faulty without having to be able to prove why, how or where. That part can then be addressed manually.
This would semi-automate at least some elements of bug-hunting and quality control. Even if you could only use the approach in a subset of kernel modules, due to the complexities of interactions, I see no reason why you couldn't use this to perform far more rigorous checks than things like the Stanford Checker or Klokwork are currently capable of.
Re:It's about n-dimensional tic-tac-toe. (Score:3, Interesting)
If that is the interpretation, then where is the crossover point between lower dimensional and higher dimensional space where the draws stop?