Mathematicians Found, Fixed Error in 60-year-old Proof

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. [ Click on the image to read the full article ]