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

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Would you help him?

Andrzej

Piotr Rudnicki wrote:

> 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 -----