[mizar] [jstevh@msn.com: Proof checking another perspective]

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

I think you may enjoy this.

PR

----- Forwarded message from JAMES HARRIS <jstevh@msn.com> -----

From:	"JAMES HARRIS" <jstevh@msn.com>
To:	piotr@cs.ualberta.ca
Subject: Proof checking another perspective, receive me

Dear Professor Rudnicki:

I read with interest just now the "QED Manifesto" only to see with dismay 
that it was written back in 1994 and little seems to have changed.  You see 
I have a label as a math "crank" as I've spent some years posting on the 
sci.math newsgroup among others on Usenet, while I'm not a mathematician, 
and I've spent a lot of that time having made various claims that I'd proven 
Fermat's Last Theorem, only to later admit that I was wrong.

However, along the way I found some mathematics that does work; however, 
it's still rather dramatic, and now I'm stuck.  A math paper that I wrote is 
currently at a journal, where it's been since August of last year, maybe 
they'll come through for me, maybe they'll look at it and say it doesn't fit 
standard math formats, or some other reason to say no.

Yet if there were something like what the QED Manifesto said out there then 
I could run my argument through a proof checker!

So there's another way that automating and formalizing could help, by being 
a place you could send someone like me, who might against all odds, or 
beliefs to the contrary have found something important, but ran into a wall 
with the math community.


James Harris

_________________________________________________________________
Get some great ideas here for your sweetheart on Valentine's Day - and 
beyond. http://special.msn.com/network/celebrateromance.armx

----- End forwarded message -----