Math # AI 27/n 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…