(Documentation) "Reading" the Mathlib library

Stream: new members

[Philippe Duchon]

I am still a very novice Lean/Mathlib user, but with interest in formalising mathematics for some time (coming from Coq, which is more commonly used in the Computer Science community, esp. in France). I just started a personal project and spent most of a day browsing the documentation of Mathlib to try to find out how to do things at least half right (I need polynomials and power series in noncommutative variables, which I don't think is there at the moment).

My question here is rather methodological: how to understand how the Mathlib library works. There are a lot of structures out there, and I am clearly getting lost. The fact that many algebraic structures exist in both "additive" and "multiplicative" variants doesn't make things any easier (even though I understand this, partly).

Just looking at the definition of a class it not sufficient, as some definitions are clearly equivalent even though they are intended for different purposes. Zero(types with a distinguished zero element) and Inhabited (types with a distinguished default element) are equivalent, though of course the intent of what to do with them is different; Add and ``Mul``` are also the same thing, types with an internal binary operation. So the intent has to be somehow described somewhere, otherwise the user cannot know which one to use. I understand that some notations can be attached to a class, but looking at the source code or browsing the documentation doesn't show that, at least not simply.

Is there a place I can go to catch on quicker?

(Sorry, accidentally posted before I was done)

[Sébastien Gouëzel]

Indeed, just browsing through mathlib sources will not point you towards good practices or explain the design decisions. I would start with #mil.

[Philippe Duchon]

Indeed, Mathematics in Lean is among my bookmarks too. I've tried reading it from scratch at least twice, always having trouble when things start getting rough (around the "Structures" and "Hierarchies" chapters, which at least seems coherent with my preoccupations) - and I need to get to at least the "Topology" part, which won't be a walk in the park since I learned topology 35-40 years ago without the "filter" word ever being pronounced.

Now, maybe my idea of getting in by formalising some topic from scratch instead of some results from an established topic is not the best.

[Luigi Massacci]

It depends also on what you mean by "from scratch"

[Luigi Massacci]

But as a first project (though I'm hardly an expert myself) it's probably easier to prove some property of existing objects in mathlib as opposed to defining something altogether new and then proving stuff about it

[Eric Wieser]

(I need polynomials and power series in noncommutative variables, which I don't think is there at the moment).

I think the former is docs#TensorAlgebra ?

[Philippe Duchon]

Eric Wieser said:

(I need polynomials and power series in noncommutative variables, which I don't think is there at the moment).

I think the former is docs#TensorAlgebra ?

It might, but I'm not sure because I didn't pay enough attention in these algebra classes a long time ago.

I see the library assumes a commutative semiring for the coefficients; at least some of the theory I had in mind doesn't need commutativity (though most interesting examples will be commutative I guess).

Thanks for the replies anyway.