There is no way Fermat could have fit that in the margin. Definitely vindicated.

The next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It’s clear to everyone including Anthropic that this proof isn’t as concise as it could have been. When it’s concise enough to be accepted into Mathlib is when victory truly is upon us.

Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct?

How have we not merely substituted one verification problem for another?

>> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.

> Pretty insane.

I don't think the count of "intermediate theorems" tells you anything. Here's something from an algebra textbook:

---

Let G be a group, let H be a subgroup [of G], and let N be a normal subgroup [of G]. Then

H ∨ N = HN = { hn | h ∈ H, n ∈ N }.

---

This says that the subgroup closure of H and N, the smallest subgroup that contains them both, is identical with the set consisting of all products of an element of H (on the left) and an element of N (on the right).

Part of the proof:

---

Suppose that x and y are elements of [the set of products hn]. Then x = h₁n₁ and y = h₂n₂, where hᵢ ∈ H and nᵢ ∈ N. Now h₂⁻¹n₁h₂ = n₃ ∈ N, as N is normal in G. So n₁h₂ = h₂n₃. In this case

    xy = (h₁n₁)(h₂n₂)
       = (h₁(n₁h₂)n₂)
       = (h₁(h₂n₃)n₂)
       = (h₁h₂)(n₃n₂),

---

This will translate directly into lean. If you do it this way, you will prove at least 10 of what would be described in lean as 'intermediate theorems':

    ∃ h₁ ∈ H, ∃ n₁ ∈ N, x = h₁ * n₁
    ∃ h₂ ∈ H, ∃ n₂ ∈ N, y = h₂ * n₂
    h₂⁻¹ * n₁ * h₂ ∈ N
    n₁ * h₂ = h₂ * n₃
    x * y = (h₁ * n₁) * (h₂ * n₂)
    (h₁ * n₁) * (h₂ * n₂) = (h₁ * (n₁ * h₂) * n₂)
    (h₁ * (n₁ * h₂) * n₂) = (h₁ * (h₂ * n₃) * n₂)
    (h₁ * (h₂ * n₃) * n₂) = (h₁ * h₂) * (n₃ * n₂)
    h₁ * h₂ ∈ H
    n₃ * n₂ ∈ N

especially compared to existing 129 pages proof by human