>. Claude produced the first end-to-end, computer-checked proof of FLT. Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.

I'm just old enough to remember Paul Erdo"s and his notion of 'The Book', which he defined to be a book the "Supreme Fascist" (God) had which held the most elegant proofs of mathematical theorems.

https://en.wikipedia.org/wiki/Paul_Erdős#Personal_life

It would be interesting to see how Erdo"s would name such a huge proof by Claude using Lean.