👓 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,

Published by

Chris Aldrich

I'm a biomedical and electrical engineer with interests in information theory, complexity, evolution, genetics, signal processing, IndieWeb, theoretical mathematics, and big history. I'm also a talent manager-producer-publisher in the entertainment industry with expertise in representation, distribution, finance, production, content delivery, and new media.

Leave a Reply

Your email address will not be published. Required fields are marked *