suggested tasks for newcomers

Stream: new members

[Joachim Breitner]

Hello! I was wondering if the mathlib project maintains a list of things for curious and interested newcomers (like, potentially, me) to work on? I see the list of missing proofs from the list of 100 theorems, but I am not sure if this is a suitable contributions-welcome list.

[Alex J. Best]

Hi! The 100 theorems list probably isn't the best place to start (many of the easy / fun ones are already done, either merged or in some open PR somewhere).
Instead; we have a few issues tagged as good-first-projects https://github.com/leanprover-community/mathlib/issues?q=is%3Aopen+is%3Aissue+label%3Agood-first-project, and a list of problems from the undergraduate topics list that are "trivial" https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets or "low-hanging-fruit" https://github.com/leanprover-community/mathlib/wiki/Undergrad-low-hanging-fruits.
So I'd say check all these lists out and see what you think might suit you, and feel free to discuss your plans/ideas here of course!

[Arthur Paulino]

You might also come across some lines marked with TODO in mathlib code base. Some of them may represent whole new milestones but some of them might be small goals

[Yaël Dillies]

Look for ## TODO in VScode and you'll find lots.

[Joachim Breitner]

Or maybe I can port some of the proofs about Free Groups that I did in Isabelle a long time ago (e.g. “Free Groups are isomorphic iff their set of generators are isomorphic” )
Anyways, first I have to get into lean etc., before I make too big a promise here ;-)

[Yaël Dillies]

We have docs#free_abelian_group, done by Kenny Lau a while back.

[Patrick Massot]

docs#free_group is also there

[Eric Rodriguez]

Also even docs#subgroup_is_free_of_is_free, but I don't think any further development

[Adam Topaz]

We should have docs#free_group.congr docs#free_group.free_group_congr` or something...

[Adam Topaz]

Although I don't know if the converse is there.

[Adam Topaz]

@Joachim Breitner It's also worthwhile to note that we have a class characterizing free groups in docs#is_free_group which is more general than using just the free_group itself.

[Alex J. Best]

@David Wärn had the strong version of Nielsen-Schreier (giving the rank in terms of the index) at https://github.com/dwarn/nielsen-schreier-lean which I think would give this result, but I don't know the status of that code these days

[David Wärn]

As far as I know the Nielsen-Schreier index formula is orthogonal to the fact that rank is well-defined. (What I showed was that every subgroup has a free generating set whose cardinality satisfies the index formula, but a priori another generating set can have a different cardinality.) Probably the easiest way to prove the latter result would be via the abelianisation. Probably mathlib knows that the abelianisation of a free group is a free abelian group, and that isomorphic groups have isomorphic abelianisations?

[Adam Topaz]

At some point the free abelian group was defined as the abelianization of the free group.... I'm not sure if that's still the case.

[Adam Topaz]

It is :)

/-- The free abelian group on a type. -/
def free_abelian_group : Type u :=
additive $ abelianization $ free_group α

[Yaël Dillies]

Btw the file containing free_abelian_group is one of the last ones to import deprecated stuff, if someone feels like cleaning that up!

[Joachim Breitner]

Ah, right. Back then when I tried to prove this in Isabelle I first shied away because all the proofs I had seen use the abelianization, which wasn't available in Isabelle. Then someone pointed me to a proof that doesn’t use that (it goes via Hom(F(X),C2)), and I used that. But since abelianization is available in mathlib, likely an simpler proof is possible.

[Yaël Dillies]

The reason for this import has to do with considering free_abelian_group as a monad and Kenny going wild with monadic programming.

[Adam Topaz]

@Yaël Dillies what's deprecated in that file?

[Adam Topaz]

Oh I see it's just all the ascii art..

[Eric Wieser]

Regarding an earlier message, an easy task would be to change the type of docs#free_group.free_group_congr to (α ≃ β) ≃ (free_group α ≃* free_group β)

[Eric Wieser]

In that it would be good practice for leaning how to use lean to glue together existing definitions and proofs

[David Wärn]

Eric Wieser said:

Regarding an earlier message, an easy task would be to change the type of docs#free_group.free_group_congr to (α ≃ β) ≃ (free_group α ≃* free_group β)

This is actually false! If α and β are both unit, then α ≃ β has one element while free_group α ≃* free_group β has two (one for each automorphism of $\mathbb Z$). All you get is a 'logical equivalence' (by which I mean the map (free_group α ≃* free_group β) → (α ≃ β) is ill-behaved)

[Johan Commelin]

Yaël Dillies said:

Btw the file containing free_abelian_group is one of the last ones to import deprecated stuff, if someone feels like cleaning that up!

I think it would be a good idea to git mv src/deprecated src/unbundled.

[Yaël Dillies]

It would be a better descriptive for sure.

[Yaël Dillies]

However the plan is still to get rid of it, right?

[Johan Commelin]

@Yaël Dillies No, I don't see why we should get rid of it.

[Johan Commelin]

Sometimes they might just be genuinely useful. They just shouldn't be the default API/entry point.

[Kevin Buzzard]

When I was pushing the deprecated imports towards the leaves there were times when the new code was clunkier than the old

[Kevin Buzzard]

Regarding the original question, I think it's time we had a new list of interesting things to do

[Kevin Buzzard]

I think there are problems with all the current lists. I think that the way to grow the community is to start advertising a new list of mathematically interesting problems which are now accessible and which would be good first issues for people with a mathematical background but little Lean experience -- a project to get their teeth into. I have an in progress list here https://github.com/kbuzzard/xena/blob/master/student_projects.md but right now I have to worry about teaching and it's too number theory heavy

[Yaël Dillies]

I have some ideas myself. For example, #11308 will unlock Sperner theory with lots of cool untapped stuff.

[Kevin Buzzard]

I am unclear about whether it's a good idea to just spam the mathlib issues page and mark a bunch of issues as "good for the mathematician wanting to learn Lean"

[Yaël Dillies]

There are two questions:

• What we want to advertise
• Where to advertise it

[Kevin Buzzard]

I want to start pushing the idea of Lean to PhD students. Not "become my student and spend 4 years formalising" but "do a PhD with someone else and do some formalising on the side". For this I think we need a list of fun accessible projects at MSc level

[Kevin Buzzard]

I think it's an easy sell because lean is in the collective consciousness of young mathematicians right now

[Joachim Breitner]

Also, I don’t think it’s an easy task: The reverse direction (free_group α ≃* free_group β) → (α ≃ β) I think requires a bit of proving? But yes, that’s the task I set for myself :-)

[Kevin Buzzard]

if they're iso then the abelianisations mod 2 are iso and we know that isomorphic vector spaces have bases of the same cardinality but what perhaps won't be there right now is that the generating set is a basis

[Martin Dvořák]

Idea for beginners: https://github.com/leanprover-community/mathlib4/blob/e76a76c36a1c2792438b62656bb94234bc4e5317/Mathlib/Data/Matrix/Block.lean#L227-L230
Create Matrix.fromRows and Matrix.fromColumns versions of it.

[Eric Wieser]

@Chance Nahuway, since you expressed interest in matrices in mathlib and making a first contribution, this should be a very easy thing to start with (in that most of the difficulty will be in learning the contribution process)

[Bolton Bailey]

It would be nice if there were a few more PRs/issues with the good-first-issue tag for better newcomer visibility.

[Chance Nahuway]

Eric Wieser said:

Chance Nahuway, since you expressed interest in matrices in mathlib and making a first contribution, this should be a very easy thing to start with (in that most of the difficulty will be in learning the contribution process)

Thanks Martin for suggesting this, and Eric for tagging me! I’m going to be spending the next week or two going through one of the intro textbooks. Then these two items look like a great place to start really working. I know you guys could probably code these up in a matter of minutes, but thank you for saving something for us newbies :)

[Martin Dvořák]

Maybe an idea for beginners: Matroid.disjointSum is commutative.
docs#Matroid.disjointSum
However, before anybody starts working on it, @Peter Nelson should perhaps clarify whether the commutativity should be proved from a commutativity of a more general matroid sum.

[Malte Dickson]

Hi! I'm new here and I'm considering doing a project where I can spend up to around 100 hours (or less) on something. I was considering doing some proofs about abundant numbers (I generally like number theory), but I thought I'd check here to see if anyone has other suggestions? A bit of a restriction is that I've only studied math up to I think something like an advanced high school level.

[Kevin Buzzard]

My course has an elementary number theory section here https://github.com/ImperialCollegeLondon/formalising-mathematics-2024/tree/main/FormalisingMathematics2024/Section15numberTheory . You could try filling in some of the sorrys there.