[FOM] Errors discovered as a result of formalization

[Lawrence Paulson]

Another significant error is here, found by one of my postdocs:

 https://arxiv.org/abs/1911.09354

The paper in question, "Quantum Games and Quantum Strategies”, has been cited nearly a thousand times, so the error What must be called significant.

A description of the Isabelle/HOL formalisation is freely available online:

 https://drive.google.com/file/d/1rw-Td4BUNb5LARKAhKiU3ceThi8V6UkP/view

Larry Paulson
On 14 Jan 2020, 23:35 +0000, Timothy Y. Chow <tchow at math.princeton.edu>, wrote:
> A few years ago here on FOM, the question was raised as to whether there
> were convincing examples of significant errors in proofs being discovered
> during the process of formalization. Here's one FOM post (by me) in that
> thread:
>
> https://cs.nyu.edu/pipermail/fom/2014-October/018210.html
>
> At the time, it seemed that there were no examples. The question was
> raised on MathOverflow some time later.
>
> https://mathoverflow.net/questions/291158/proofs-shown-to-be-wrong-after-formalization-with-proof-assistant
>
> The top two answers to the question are, in my opinion, pretty convincing
> recent examples.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200115/40fd54ac/attachment-0001.html>