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