How to design math libraries

Stream: general

[Kevin Sullivan]

Dear Lean Provers:

A colleague and I have a newly (about to be) funded project involving the mapping of objects of a certain type to physical quantities, represented by terms in the language(s) of mathematical physics formalized in Lean. We'll need libraries that will allow us to represent things like vector, affine, and Euclidean spaces, including objects and transformations, tensors of various kinds, Minkowski spaces, etc. To our knowledge, such libraries don't yet exist.

That leads to the question, what are the best practices for, and what are the most useful resources for informing, the design of mathematical libraries in Lean? Ideally we'd like to have what we produce have a life beyond our lab. I know that numerous of you on this list have been deeply involved in the development of math libraries for the Lean prover. Any informative discussion of what's involved principles, design guidelines, etc. would be much appreciated.

[Simon Hudon]

There's a lot to learn, I think the mathlib community learned a lot from building mathlib. There is still improvement to be had. When you don't know how to do something, find a project (maybe mathlib) and see if they had to solve the same problem. If no Lean project has had to solve the same problem, look at the Coq community or the Isabelle community or any other.

[Simon Hudon]

More specifically, make your types as simple as you can, don't use dependent types if you don't have to.

[Simon Hudon]

And be ready to use simp and meta-programming to make modules easier to use in your proofs.

[Jesse Michael Han]

That leads to the question, what are the best practices for, and what are the most useful resources for informing, the design of mathematical libraries in Lean? Ideally we'd like to have what we produce have a life beyond our lab. I know that numerous of you on this list have been deeply involved in the development of math libraries for the Lean prover. Any informative discussion of what's involved principles, design guidelines, etc. would be much appreciated.

This is one of the topics we wanted to focus on when organizing the Hanoi Lean workshop. @Floris van Doorn is scheduled to deliver two lectures specifically about best practices for Lean library development.

[Kevin Sullivan]

This is one of the topics we wanted to focus on when organizing the Hanoi Lean workshop. Floris van Doorn is scheduled to deliver two lectures specifically about best practices for Lean library development.

That's a great pointer. If the workshop materials are to be made more broadly available (even maybe videos?), I'd be first in line to check them out. Thank you.

[Scott Morrison]

Please record Floris' talks!

[Floris van Doorn]

The pressure is on... :anxious:

[Scott Morrison]

(My experience of recording many of my crappy talks is the following --- the very few people who ever watch the recordings are exactly the tiny subset of people who are really interested in what you're doing, and so they are happy and grateful that the talk was recorded, no matter how badly you messed up explaining things. :-)

[Kevin Buzzard]

That's an interesting point. I've certainly enjoyed your YouTube talks Scott!

[Floris van Doorn]

There is no video of the talk. Someone did make a voice recording, but it might be hard to know what was going on since I was jumping around files in VSCode. (I now realize I could have easily recorded my screen + voice with OBS. I didn't think of that before :oops: )
To give you an idea, during my talk I went through (and wrote parts of) this file:
https://github.com/jesse-michael-han/hanoi-lean-2019/blob/master/src/floris/lecture-library-building.lean
I also did an introduction to mathlib:
https://github.com/jesse-michael-han/hanoi-lean-2019/blob/master/src/floris/lecture-mathlib.lean