how to track progress?

Stream: general

[Mario Krenn]

hi! i am following sporadically the Lean/Xena project (always having in mind to jump in at some point, maybe with a student). After watching some of the recent talks on youtube on the summer projects, i was wondering, how one tracks the progress of the mathlib. Is there a website where you have listed all of the definitions and theorems you want to implement? With updates when they are implemented?

Also, after a theorem or definition is defined in Lean, can it be used in the formalization of other definitions/theorems?

Are there also some funded projects in Lean (for instane, a bounty on some certain theorems/proofs)?

[Johan Commelin]

@Mario Krenn This is a first order approximation of what you asked for: https://leanprover-community.github.io/undergrad.html

[Johan Commelin]

Also, after a theorem or definition is defined in Lean, can it be used in the formalization of other definitions/theorems?

Yes? I don't really understand this question.

[Johan Commelin]

Are there also some funded projects in Lean (for instane, a bounty on some certain theorems/proofs)?

I'm not aware of any bounties. But people have gotten some personal grants (that they typically applied for themselves) to work on Lean projects.

[Mario Krenn]

Johan Commelin said:

Also, after a theorem or definition is defined in Lean, can it be used in the formalization of other definitions/theorems?

Yes? I don't really understand this question.

Thanks, i think you understand it well, it was just a naive question.

Johan Commelin said:

Mario Krenn This is a first order approximation of what you asked for: https://leanprover-community.github.io/undergrad.html

Great thats very useful thanks!

[Mario Krenn]

Johan Commelin said:

Mario Krenn This is a first order approximation of what you asked for: https://leanprover-community.github.io/undergrad.html

I was going through the list, and I wonder whether it is complete. For instance, i know that there are a number of nice graph theory proofs (e.g. Hall's marriage theorem) that have been formalized, but i cant find any of those concepts in the list.

[Kevin Buzzard]

"undergraduate maths" has a very precise definition here -- it is the content of a specific degree taught in France to people who want to become teachers.

[Johan Commelin]

It's taken from a French undergrad curriculum. See the top of the page.

[Kevin Buzzard]

If you want to know if Hall's Marriage Theorem is in mathlib you can go to https://leanprover-community.github.io/mathlib_docs/ and type Hall's Marriage Theorem into the search box. Wait until the octopuses have had their say, and if they don't come up with much then try the google site search button.

[Eric Wieser]

There's a project at https://github.com/ImperialCollegeLondon/pure-maths-yamls to build a similar list for the imperial undergrad degree, right?

[Kevin Buzzard]

yes but it is sufficiently preliminary that I am not particularly talking about it yet (e.g. right now there are 0 links to mathlib)

[Mario Krenn]

Kevin Buzzard said:

"undergraduate maths" has a very precise definition here -- it is the content of a specific degree taught in France to people who want to become teachers.

Ah OK thanks, thats a great way to have a roadmap for formalizing the whole undergrad curriculum. Is this where the motivation comes from? (i.e. you can claim that the Xena project has succeeded when each element in that list is formalized)?

Are there systematic lists of other theorems, for example those theorems from summer projects? Are they standalone projects or actaully included into the mathlib?

[Mario Krenn]

Kevin Buzzard said:

If you want to know if Hall's Marriage Theorem is in mathlib you can go to https://leanprover-community.github.io/mathlib_docs/ and type Hall's Marriage Theorem into the search box. Wait until the octopuses have had their say, and if they don't come up with much then try the google site search button.

This is very useful for searching, thanks - i will play with it! Can it also be used to keep track of the progress? i.e. to see what has been added in the last few weeks? This is what i couldnt find yet as a non-expert so far, but probably it exists.

[Kevin Buzzard]

The utterances of the octopi are up to date (documentation is recompiled at least once a day) but the google site search is something we can't control

[Kyle Miller]

Mario Krenn said:

I know that there are a number of nice graph theory proofs (e.g. Hall's marriage theorem) that have been formalized

(Just want to mention that the version of the theorem we have (docs#finset.all_card_le_bUnion_card_iff_exists_injective) is essentially Hall's original formulation, which makes no mention of graphs. It seems that pedagogically graphs are used because they help with visually organizing the information, but it turns out they're not essential to the argument. There is a graph formalization, but we haven't gotten around to actually cleaning it up for inclusion in mathlib.

Also, thanks for mentioning the theorem, I completely forgot #7825 was never merged, which removes the restriction that ι be finite!)

[Kyle Miller]

Mario Krenn said:

i.e. to see what has been added in the last few weeks?

One place to see recent changes is #rss > Recent Commits to mathlib:master (it shows progress in the sense that each entry indicates a PR has been merged and closed)

[Yaël Dillies]

Kyle Miller said:

Also, thanks for mentioning the theorem, I completely forgot #7825 was never merged, which removes the restriction that ι be finite!)

Reviewing!

[Kyle Miller]

(@Yaël Dillies Thanks. I'm right now trying to git it up to current mathlib.)

[Yaël Dillies]

Perfect! I'll stop reviewing until you've done that, then.