Zulip Chat Archive

Stream: general

Topic: Literate Lean


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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