I can't read the full article, but the part that I can see looks interesting.
The article "Mathematicians found – and fixed – an error in a 60-year-old proof" by Alex Wilkins, New Scientist, has the following summary posted by the ACM: "An error in a proof underlying a widely used branch of modern mathematics was accidentally discovered by mathematicians while translating old proofs to a computer language in a process called formalization. Recently, Kevin Buzzard at Imperial College London and colleagues started to formalize the proof of Fermat’s last theorem. The proof employs many different cutting-edge branches of mathematics, much of which isn’t yet machine-readable, so these must be translated first. While working on the translation, Antoine Chambert-Loir at Université Paris Cité encountered an error, which was quickly remediated." This has long been the argument of Norm (Metamath) & others involved in formalization of mathematics - that formalization forces the revelation of proof errors long unnoticed. Summary in ACM Tech News (2024-12-27): https://technews.acm.org/archives.cfm?fo=2024-12-dec/dec-27-2024.html Full article: https://www.newscientist.com/article/2461891-mathematicians-found-and-fixed-an-error-in-a-60-year-old-proof/ --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/7CF772DD-1896-4B07-9131-2D971C4C23E2%40dwheeler.com.
