per topic intro

Stream: new members

[Nicolas Rolland]

Is there some introductory material per topic for those listed on mathlib reproduced below ?

Say some presentation video and intro article on how to learn, how to prove, what are the conventions, etc..
Wouldn't it make sense to have a presentation of those, easier than source code + mathlib docs ?

I see that some very cursory attempt has been made here with that spirit.

I wonder if some effort is already underway, or if you think it would be worthwhile to (re)launch it ?

---

• algebra
• algebraic geometry
• analysis
• calculus
• category theory
• combinatorics
• core
• documentation,
• formal languages
• functional analysis
• geometry
• homology
• infrastructure
• lean formalization
• linear algebra
• measure theory
• model theory
• number theory
• operator algebras
• performance
• probability
• proof engineering
• tactics
• topology
• type theory

[Damiano Testa]

The series of meetings "Lean for the curious mathematician" often have presentations that focus on subjects like the ones that you mention. Many of those are recorded. I think that it might be a good idea to link the list above to the relevant presentations, though this may require some amount of maintenance, since mathlib evolves relatively quickly!

[Damiano Testa]

For definiteness, this is a link to the latest edition:

https://lftcm2023.github.io/tutorial/index.html

[Patrick Massot]

#mil is meant to contain such introductions eventually, but so far it applies only to topology and analysis.

[Nicolas Rolland]

Patrick Massot said:

#mil is meant to contain such introductions eventually, but so far it applies only to topology and analysis.

Ah ! It makes sense to think of #mil that way. It is pure gold for its current scope !

[Yaël Dillies]

Btw, Patrick, Bhavik and I are still interested in contributing a combinatorics chapter to MIL.

[Yaël Dillies]

My lectures start in a week though. So it'll have to wait a little bit. :sad: