One week ago, on September 4th, Anthropic announced that it had more or less done the same job, namely generated a complete formalization of the proof of Fermat's Last Theorem. They claim the work took 11 days, “largely autonomously”, so that we now have 13 million lines of Lean code that contains a complete proof of that theorem.
Those files compile, but require 20 more times to Buzzard's computer to compile than the Mathlib library (which on my computer requires several hours), and that computer has 96 cores and 500GB RAM. So this is a new kind of formalized proof, one that escapes standard computers and belongs to the world of supercomputers, thus pushing back farther the gap between mathematics and its formalized form.
In other words, what Anthropic did is clearly an impressive technical achievement, one that might be relevant to AI industry, but is definitely irrelevant for mathematics.
https://www.anthropic.com/research/formalizing-fermats-last-theorem