>> 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
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':
The part of the proof that I quoted just proves that the product set HN is closed under multiplication - the product of any two elements in HN is also an element of HN. This is part of proving that HN is a subgroup. You might call it an 'intermediate theorem' to that proof.
My point isn't that this is missing from mathlib, or that this result is part of the work mentioned in the blog post. It's that doing this proof in a way that matches the textbook proof requires you to prove a large number of "intermediate theorems", and that those "intermediate theorems" often look more like computational steps than anything that a mathematician might call "theorems".
In particular, note that the 10 required intermediate theorems I mentioned all refer to free variables.
> Perhaps it isn't and it is a nice PR for beginners.
By the way, there is a steady stream of people who come into the "new members" channel on the Lean zulip and ask for ideas for a minor contribution they can make. The stock answer is generally that the low-hanging fruit has been picked.
But that isn't really accurate. If your goal is to get something, anything, into mathlib with your name on it, you probably can. Choose some undergraduate exercises, try to formalize them using mathlib, and at some point you'll run into some convenience lemmas that you wish were present. You can then produce one of those lemmas and try to get it accepted.
(As part of a project I'm working on, I produced a proof that involved showing that a function was bijective from the already-existing mathlib theorems that it was injective and surjective. There was no one-step existing theorem despite the existence of the injectivity and surjectivity theorems.
When I complained about some other part of my proof, somebody else picked up on that and quickly submitted a convenience theorem directly stating the bijectivity. That's the kind of thing I'm talking about, though you can go more complex than that example.)
> 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
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':
But none of these would be called an "intermediate theorem" in a paper proof.