“This story really highlights, to me, the poor job which humans do of documenting modern mathematics.”
Two months into teaching Lean the proof of Fermat’s Last Theorem, the computer rejected a key lemma from a 1965 paper. Lemme 8 in Roby’s work on divided powers looks false, and crystalline cohomology has been built on it since the 1970s. Roby, Grothendieck and Berthelot are all dead, so there was nobody left to ask. The rescue came from an appendix by Arthur Ogus, whose first reaction was that the appendix has several errors too.