Article "Mathematicians found – and fixed – an error in a 60-year-old proof" (New Scientist)

[David A. Wheeler]

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

[Discher, Samiro]

This sounded familiar. I think I've read some details about this from Kevin Buzzard himself here:

https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/

---

Von: 'David A. Wheeler' via Metamath <meta...@googlegroups.com>
Gesendet: Freitag, 27. Dezember 2024 21:26:50
An: Metamath Mailing List
Betreff: [Metamath] Article "Mathematicians found – and fixed – an error in a 60-year-old proof" (New Scientist)

 

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/7CF772DD-1896-4B07-9131-2D971C4C23E2%40dwheeler.com.