On Friday 03 March 2006 01:02, Henry Baker wrote:
Computer proof-checking technology (HW & SW) have gotten to the point where it now makes sense to develop a system whereby _every_ mathematical proof could eventually be _checked_ by computer. This won't happen overnight, but will require a 10-20 year effort to develop a generic system into which one could shovel all the lemmas, theorems, etc., so that _every_ paper submitted to a math journal would come with its own certification that the proof is valid. ... I'm trying to find someone with the stature to start pushing such a project. This is a project worthy of finishing in the 21st century. It is probably more important in the long run than going to Mars.
Ah. So surely what you're after is someone with credibility and influence *among mathematicians and computer scientists*? That strikes me as quite different from what you originally asked for, but maybe I'm missing something. Thomas Hales, who has allegedly proved Kepler's conjecture (with the help of a big computer search), is trying for an easier goal, namely a completely formal and automatically checkable proof of KC. Much work towards that goal is likely to mean progress towards your more ambitious one. -- g