Re: [isabelle] References about mistakes and gaps in papers



Hi José,

Did you submit any notes eventually?

I came to this question by search engine, and lately I was informed that a
similar question was asked on MathOverflow, where Manuel Eberl also
contributes an answer:

Proofs shown to be wrong after formalization with proof assistant
https://mathoverflow.net/q/291158/125494

Search engine optimization (manually, lol):
I'm posting the MathOverflow link here so that future visitors could
find the question and answer easier :)

On Mon, 6 Aug 2018 at 02:17, Tjark Weber <tjark.weber at it.uu.se> wrote:
>
> José,
>
> On Sat, 2018-07-28 at 19:17 -0400, José Manuel Rodriguez Caballero
> wrote:
> > After trying to formalize the argument from the paper
> >
> > Ali, H. A. S. (2001). 85.26 Another method for Pythagorean triples. The Mathematical Gazette, 85(503), 273-273.
> >
> > I found a gap and I submitted a note to the journal filling this gap.
> > The reviewer was interested in the fact that this mistake was found
> > using a proof assistant (Isabelle). So, for the final version of this
> > note I would like to include a list of papers whose gaps or mistakes
> > where only discovered by means of a proof assistant. I will appreciate
> > any reference. Thank you in advance.
>
> While not focused on proof assistants, the following discussion may
> still be interesting to read:
>
> http://math.stackexchange.com/questions/139503/in-the-history-of-mathematics-has-there-ever-been-a-mistake
>
> It contains numerous further pointers.
>
> The paper "Errors and Corrections in Mathematics Literature" might also
> be of interest:
>
> http://www.ams.org/notices/201304/rnoti-p418.pdf
>
> Best,
> Tjark
>
>
>
>
>
>
>
>
>
>
> När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
>
> E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/om-uu/dataskydd-personuppgifter/
>


-- 
Regards,
Qian Hong




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.