[FOM] Errors discovered as a result of formalization

[Timothy Y. Chow]

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.

Tim