Zulip Chat Archive

Stream: new members

Topic: suggested tasks for newcomers


Joachim Breitner (Jan 10 2022 at 18:13):

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 (Jan 10 2022 at 18:17):

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 (Jan 10 2022 at 18:21):

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 (Jan 10 2022 at 18:27):

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

Joachim Breitner (Jan 10 2022 at 18:36):

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 (Jan 10 2022 at 18:55):

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

Patrick Massot (Jan 10 2022 at 19:04):

docs#free_group is also there

Eric Rodriguez (Jan 10 2022 at 19:26):

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

Adam Topaz (Jan 10 2022 at 19:48):

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

Adam Topaz (Jan 10 2022 at 19:49):

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

Adam Topaz (Jan 10 2022 at 20:00):

@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 (Jan 10 2022 at 20:07):

@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 (Jan 10 2022 at 20:42):

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 (Jan 10 2022 at 20:45):

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 (Jan 10 2022 at 20:46):

It is :)

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

Yaël Dillies (Jan 10 2022 at 20:47):

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 (Jan 10 2022 at 20:47):

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 (Jan 10 2022 at 20:48):

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 (Jan 10 2022 at 20:49):

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

Adam Topaz (Jan 10 2022 at 20:49):

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

Eric Wieser (Jan 10 2022 at 20:58):

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 (Jan 10 2022 at 20:58):

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

David Wärn (Jan 10 2022 at 21:11):

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 Z\mathbb Z). All you get is a 'logical equivalence' (by which I mean the map (free_group α ≃* free_group β) → (α ≃ β) is ill-behaved)

Johan Commelin (Jan 11 2022 at 07:07):

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 (Jan 11 2022 at 07:08):

It would be a better descriptive for sure.

Yaël Dillies (Jan 11 2022 at 07:21):

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

Johan Commelin (Jan 11 2022 at 07:39):

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

Johan Commelin (Jan 11 2022 at 07:39):

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

Kevin Buzzard (Jan 11 2022 at 08:09):

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

Kevin Buzzard (Jan 11 2022 at 08:09):

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

Kevin Buzzard (Jan 11 2022 at 08:14):

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 (Jan 11 2022 at 08:15):

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

Kevin Buzzard (Jan 11 2022 at 08:16):

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 (Jan 11 2022 at 08:17):

There are two questions:

  • What we want to advertise
  • Where to advertise it

Kevin Buzzard (Jan 11 2022 at 08:22):

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 (Jan 11 2022 at 08:23):

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

Joachim Breitner (Jan 11 2022 at 13:17):

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 (Jan 11 2022 at 13:19):

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


Last updated: Dec 20 2023 at 11:08 UTC