formalizing linear algebra done right

Stream: new members

[Vasily Ilin]

I want to go through (some of) Linear Algebra Done Right with a couple people next year and formalize it in Lean. Has anyone tried/done this for other textbooks? It would be cool to have an entire textbook formalized.

How much do you think we should rely on mathlib in this endeavor. One extreme is to take everything in mathlib as given and only do the exercises in the book. The other extreme is to only use abelian groups and fields, and redefine everything: vector spaces, linear independence, etc. Any advice on this?

[Eric Wieser]

Unless it's for your own learning or for teaching lean to students very familiar with that particular, rebuilding everything from scratch sounds like a particularly bad investment of time

[Eric Wieser]

Doing all the exercises feels like a much better project, especially if doing them reveals gaps in mathlib

[Kyle Miller]

I think it'd also be worth formalizing theorem statements using mathlib and trying to find the corresponding mathlib proofs.

[Kyle Miller]

This has probably been asked before, but would formalized textbooks be a good fit for the mathlib archive folder? The additional maintenance burden seems like it would be worth it:

• it's a test of whether mathlib's APIs are up to the task, and it can drive development of library improvements.
• it can stand in for some documentation, since it would be an entry point into mathlib from a potentially familiar point of view.
• when someone asks "how can I help?" we can point them toward working on a textbook formalization, which will naturally lead to helping with mathlib proper when gaps arise.
• when a textbook is complete, we can point to it and say "yes, mathlib does in fact know this," and since it's in the archive we know mathlib won't forget.

[Vasily Ilin]

What is the mathlib archive folder? I am not familiar with it.

[Kyle Miller]

In the mathlib repository, whereas the src folder contains the mathematics library, archive contains some other formalizations that for one reason or another aren't library code.

[Kyle Miller]

There's also counterexamples and roadmap, the latter which I only noticed recently and am not really sure what it's for.

[Eric Wieser]

Perhaps relevant to both the textbook and linear algebra aspects; I made an attempt at formalizing (<10% of) "the matrix cookbook", which contains only statements with no proofs and therefore is great for spotting holes in mathlib:

https://github.com/eric-wieser/lean-matrix-cookbook

I'm not certain how much it would benefit from being in mathlib itself

[Kevin Buzzard]

I think that the Hoskinson centre might be interested in formalised textbooks. @Jeremy Avigad ?

[Jeremy Avigad]

We should all be interested! There are really two questions here, (1) whether it should go in mathlib, and, (2) wherever it is, where we should record it (e.g. on the community web pages) so that people can find it.