Mathematics in Lean

Stream: general

[Jeremy Avigad]

Patrick Massot and I have simplified and documented the procedures we use to produce Mathematics in Lean. Almost all of the content is written in Lean files which are then used to generate the textbook, the example files (which contain exercises), and the solutions. See the documentation in the source repository.

In a few places, the names MIL and mathematics_in_lean are hardcoded into the scripts, but the setup can be straightforwardly modified to write other Lean-based books as well. We'd be glad to answer questions for anyone who wants to try it.

[Jireh Loreaux]

Thanks very much for this documentation!