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. This project should probably be called the Hilbert project, since it would complete a portion of what Hilbert wanted to accomplish with some of his famous problems. Just as TeX has become the de facto mathematics publishing system, we would have an (open source, of course) de facto math theorem checking system. While mathematicians can smirk at the recent Korean stem cell fiasco, mathematics has never developed the technology to avoid the possibility of a similar embarrassment. Furthermore, while mathematicians say that "mathematical truth" is of a higher quality than truth in other fields, mathematics hasn't yet followed through on a program that would guarantee such quality. Java has prompted the development of "proof carrying code" whereby a set of safety theorems are proved every time you load this code. Why shouldn't all of mathematics have the same quality of guarantees? 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. Henry Baker At 04:40 PM 3/2/2006, Gareth McCaughan wrote:
On Thursday 02 March 2006 20:46, Henry Baker wrote:
I was trying to find someone alive, as I wanted to find someone with the credibility to influence non-mathematicians, in much the same way that Einstein helped convince Roosevelt & others re the atom bomb.
So, dare I ask, what is it that you want this credible mathematician to influence people about? :-)
-- g