There's maybe an even simpler way of illustrating this.
Fermat's Last Theorem is very easy to state. There are no positive integers a, b, and c such that a^n + b^n = c^n. This likewise easy to write in Lean. The statement of the theorem is exactly one line of code.
theorem fermat_last_theorem (n : ℕ) (n_ge_3 : 3 ≤ n) (a b c : ℕ) (a_is_positive : 0 < a) (b_is_positive : 0 < b) (c_is_positive : 0 < c) : a ^ n + b ^ n ≠ c ^ n
Kevin Buzzard's team of human mathematicians attempted to prove this in Lean. They got to about 60000 lines of Lean code and were not anywhere close to finishing the job.
Anthropic came around with a Claude model that proved it in 13 million lines of code. (Buzzard's team might have ultimately used within the same order of magnitude if they finished. It's very unclear. They were at minimum years away.)
Whether 60000 or 13 million, only one line of code was necessary to manually verify whether they had successfully proved Fermat's Last Theorem, just the statement of `fermat_last_theorem`. None of the rest of the code built up the theory at all.
Indeed if those lines of code built up the theory, that would suggest that the statement of Fermat's Last Theorem is incomprehensible, if professional mathematicians cannot define Fermat's Last Theorem in even 60000 lines of code! But that's pretty absurd. You can explain the statement of Fermat's Last Theorem, completely rigorously, to a middle schooler.
Fermat's Last Theorem is very easy to state. There are no positive integers a, b, and c such that a^n + b^n = c^n. This likewise easy to write in Lean. The statement of the theorem is exactly one line of code.
Kevin Buzzard's team of human mathematicians attempted to prove this in Lean. They got to about 60000 lines of Lean code and were not anywhere close to finishing the job.Anthropic came around with a Claude model that proved it in 13 million lines of code. (Buzzard's team might have ultimately used within the same order of magnitude if they finished. It's very unclear. They were at minimum years away.)
Whether 60000 or 13 million, only one line of code was necessary to manually verify whether they had successfully proved Fermat's Last Theorem, just the statement of `fermat_last_theorem`. None of the rest of the code built up the theory at all.
Indeed if those lines of code built up the theory, that would suggest that the statement of Fermat's Last Theorem is incomprehensible, if professional mathematicians cannot define Fermat's Last Theorem in even 60000 lines of code! But that's pretty absurd. You can explain the statement of Fermat's Last Theorem, completely rigorously, to a middle schooler.