>> 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₂),
which shows that xy has the correct form.
---
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
But none of these would be called an "intermediate theorem" in a paper proof.