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

13M lines does seem extreme and there is probably a lot of inefficiency given the way the proof was developed. Cutting it down is probably a long road, but is also a very well defined problem that AIs can probably just go do with enough time and budget now.

> 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