Topic: Literate Lean
Joseph Corneli (Aug 02 2018 at 15:21):
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 (Aug 02 2018 at 15:53):
I think you can find some of that documentation here: https://github.com/leanprover/mathlib/tree/master/docs/theories
Joseph Corneli (Aug 02 2018 at 18:05):
@Simon Hudon Thanks, that's a good starting place for me to read, anyway!
Last updated: May 16 2021 at 05:21 UTC