The mathlib way - mathlib map? graph?

Stream: new members

[Robert Culling]

KIa ora :)

Yesterday I read something to the effect of:

If one wants to focus on formalising a particular topic, then picking up a textbook on that topic and formalising it is much faster than the far more general approach mathlib is taking - it's not the "mathlib way"

Is the "mathlib way" - plan of attack - written/described any where?

Also, is there a visualisation of the mathlib directory structure and the import links? I am dreaming of something as clean as the Path of Exile skill tree but that might not make sense in this context.

I realise I can browse my way through the mathlib library to figure this all out, but you all have written a lot :working_on_it: :construction: which is amazing!

Something I am particularly interested in is the interface between LEAN core and mathlib. What are the initial "non-core" definitions that mathlib makes?

Any pointers for getting my bearings with mathlib would be great :) Thanks!

[Kevin Buzzard]

Mathlib just does things in greater generality than is found in most textbooks, which are often written with pedagogy in mind. For example if you are teaching calculus then you might well teach one-variable calculus first, and multi-variable calculus later on when the students are more mathematically mature. But if you are formalising calculus then arguably this approach makes no sense, because the one-variable story is just the n=1 case of the multi-variable story, which you have to do at some point anyway, so why not do the multivariable story first and then specialise to get the one-variable story?

[Eric Wieser]

Something I am particularly interested in is the interface between LEAN core and mathlib. What are the initial "non-core" definitions that mathlib makes?

Maybe a good example of this is that core (or even Std) does not know what an docs#AddGroup is, and so (among other things) has no generalization that lets you use the same add_comm lemma for both Int and Rat.

[Michael Stoll]

Nat is not really an AddGroup...

[Robert Culling]

Thanks for your responses. I absolutely agree that the general approach is the way to go with this task. Perhaps a more precise version of my question would be: Once you realised the general approach is the way to go, how did you figure where to start? Did a group get together and set out a plan? Or was it more organic than that?

[Kevin Buzzard]

The history is written in this Zulip and in the mathlib GitHub repos. People just talked about designs and made informed decisions

[Jireh Loreaux]

You will find that we are continually searching for the "correct" generality. For instance, only recently was docs#Set.center redefined so that it gives the correct object when the multiplication is non-associative.