Email Gateway (Aug 22 2022 at 17:42): Email Gateway (Aug 22 2022 at 17:42):From: Lawrence Paulson <lp15@cam.ac.uk>
This is amazing! Although many errors in proofs have been found using proof assistants, this may be the first time that the result was a published correction in the same journal. Perhaps we should log such events?
Larry Paulson
Email Gateway (Aug 22 2022 at 17:43):From: Manuel Eberl <eberlm@in.tum.de>
Well there is this:
https://www.sciencedirect.com/science/article/pii/S0165176516302063
This is a case where the proof could not be easily repaired; the
solution was, in the end, to prove a stronger statement with a much more
complicated proof.
If I say that any formalisation of a non-trivial pen-and-paper proof
will probably uncover some mistakes/gaps/missing cases, I think it is at
most a slight exaggeration. I have certainly found numerous ones in the
past few years.
However, the majority of those are easily fixed and people don't really
care about those very much or will even say that those are ‘not really
mistakes’. I think these mistakes are usually not published anywhere
because they are too minor. Even for not-so-trivial mistakes, in my
experience, it is usually a 50:50 chance whether the authors of the
original proof will respond to a polite email pointing out the problem.
Manuel
Email Gateway (Aug 22 2022 at 18:10):From: Tjark Weber <tjark.weber@it.uu.se>
José,
While not focused on proof assistants, the following discussion may
still be interesting to read:
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/
Email Gateway (Aug 22 2022 at 19:19):From: Qian Hong <fracting@gmail.com>
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 :)
Last updated: May 06 2024 at 12:29 UTC