The main goal (project Z) of this four year proposal is to formalise mathematics. This is utterly unrealistic, and of course is to be considered a beacon very very far in the distance. Fields medalist Voevodsky suggests a 500 year horizon for this! To pile on to the difficulty of doing this, Thomas Hales explains his motivation of embarking on a formal proof of his own result, the proof of the Kepler conjecture. The background is that his paper had been accepted in one of the most prestigious mathematics journal, but conditionally on the grounds that his computer-generated proof was so complex that it could not be verified by even a team of 20 (very well trained) human referees:
In truth, my motivations for the project are far more complex than a simple hope of removing residual doubt from the minds of few referees. Indeed, I see formal methods as fundamental to the long-term growth of mathematics.
—Thomas Hales, Flyspeck project
Indeed, mathematics and mathematicians are struggling to organise the information they produce, and the refereeing process will not be capable of responding to rapid advances in our capacities at theorem proving.
So why do I think my short four year proposal is interesting, alongside all those giants? Because it introduces a new idea in the picture, that of MOOCs. It is a fact that soon hundreds of students will be taking the same classes in parallel, and that graduate classes will be taken by dozens of students rather than handfuls. Also, professors in the more basic classes will start to collaborate more on content, and a formalisation effort can help in that direction. Admittedly, the proposal is not very specific, and exposes many ideas. I think the most promising avenue is in a bootstrapping process of the proofs, submitted as crowdsourced work in the context of a MOOC (with the expert explaining the material to formalise on video, say). Already it has been shown that a lot of the Flyspeck poject proofs can actually themselves be automated, and the smart introduction of human mathematician labor can help tighten all the feedback loops.
In any case, this is going to be hard work, far in the distance. In the near future the goals will be more limited, and will probably benefit from MOOC-based research efforts in other disciplines too.
(This post also serves as an updated introduction to the "Connected Courses" course)
|||I have made a reference to it in the previous post.|