Literate Lean

Stream: general

[Joseph Corneli]

Is anyone working on a way to produce more mathematically-typical summaries of Lean theories? This is an important part of the workflow in Mizar: see Bancerek (2006) "Automatic translation in formalized mathematics"; Bancerek et al (2018) "The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar". I notice that the basic style in mathlib doesn't include a lot of comments, e.g., continuity.lean includes 7 doc strings and 120 lemmas.

[Simon Hudon]

I think you can find some of that documentation here: https://github.com/leanprover/mathlib/tree/master/docs/theories

[Joseph Corneli]

@Simon Hudon Thanks, that's a good starting place for me to read, anyway!