3 ms·

It looks like an exercise for a course in "Algebra 2" in my university. (A different course name in other universities.) I probably should know it. Give me 30

It looks like an exercise for a course in "Algebra 2" in my university. (A different course name in other universities.) I probably should know it. Give me 30 minutes to prove it. (Part of the magic is in "normal".) My algebraic friends surely know it and they would never include it in a paper because everyone knows it. I'm surprised it's not in mathlib. Perhaps it is and the AI made a copy. Perhaps it isn't and it is a nice PR for beguiners.

thaumasiotes 1mo ago
It is in mathlib. In textbooks it's presented as an introductory part of the Second Isomorphism Theorem; in mathlib it's here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Subgroup/Pointwise.html#Subgroup.coe_mul_of_left_le_normalizer_right https://leanprover-community.github.io/mathlib4_docs/Mathlib... . 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.
thaumasiotes 1mo ago
> 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.)

thaumasiotes 1mo ago

It is in mathlib. In textbooks it's presented as an introductory part of the Second Isomorphism Theorem; in mathlib it's here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Subgroup/Pointwise.html#Subgroup.coe_mul_of_left_le_normalizer_right https://leanprover-community.github.io/mathlib4_docs/Mathlib... . 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.

thaumasiotes 1mo ago

> 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.)