The Fermat's Last Theorem proof project was led by Tianyi Peng, an assistant professor at Columbia University; the AI autonomously completed more than 30,000 intermediate theorems, generated approximately 13 million lines of Lean 4 code, a volume five times that of the Mathlib core library.