👓 Proofs shown to be wrong after formalization with proof assistant | MathOverflow

Read Proofs shown to be wrong after formalization with proof assistant (MathOverflow)

Are there examples of originally widely accepted proofs that were later discovered to be wrong by attempting to formalize them using a proof assistant (e.g. Coq, Agda, Lean, Isabelle, HOL, Metamath,