I published a proof in the 3/2003 Monthly that I was then not sure was correct and, after thinking about it for hours, I'm still not sure! It doesn't look like other proofs, involving a trick that seems a little too arbitrary, and I don't know quite how to think about it. Maybe the computer could tell me. :o Steve Gray ----- Original Message ----- From: "Henry Baker" <hbaker1@pipeline.com> To: "Gareth McCaughan" <gareth.mccaughan@pobox.com> Cc: <dasimov@earthlink.net>; <math-fun@mailman.xmission.com> Sent: Thursday, March 02, 2006 5:02 PM Subject: Re: [math-fun] Most influential mathematician?
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.