# Zulip Chat Archive

## Stream: new members

### Topic: per topic intro

#### Nicolas Rolland (Sep 27 2023 at 20:35):

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 (Sep 27 2023 at 20:42):

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 (Sep 27 2023 at 20:45):

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

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

#### Patrick Massot (Sep 27 2023 at 20:56):

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

#### Nicolas Rolland (Sep 27 2023 at 21:11):

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 (Sep 28 2023 at 04:56):

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

#### Yaël Dillies (Sep 28 2023 at 04:59):

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

Last updated: Dec 20 2023 at 11:08 UTC