group.lean in natural language

Stream: maths

[Kevin Buzzard]

group.lean.pdf
group.lean.ftl

At Big Proof 2019, Peter Koepke talked about his work doing basic analysis in a proof verification system using a controlled natural language. During his time in Edinburgh he typed up the first half of group.lean into ForTheL and then pretty-printed it into a pdf file.

I know Tom Hales is interested in getting a controlled natural language to work with Lean as part of the Fabstracts project, because he (rightly, in my opinion) believes that more mathematicians will be attracted to his project if it looked like the attached pdf rather than the lean file (we lean-readers forget how intimidating Lean looks to regular mathematicians). This document is some evidence that the idea of getting human-readable text from Lean is perhaps not as far-fetched as one might initially guess.

I finish with a quote from Koepke answering my question about sharing the document.

Can I share it on the Lean chat? [I haven't done this yet]

Yes please, provided you could warn readers that this is just a dummy;
actually it would not even run in the Naproche-SAD version which is on
Github, since I used a slightly modified fork on my laptop.

[Kevin Buzzard]

[the .ftl file is a text file]

[Kevin Buzzard]

He also sent me some Sylow stuff: CNLforLean.ftl.pdf CNLforLean.ftl

[Kevin Buzzard]

Here he was not working with a file with Lean proofs, just statements of Sylow's theorems.

[Mario Carneiro]

Is there anything special being done to produce the ftl file? If it's just a hand translation into a CNL I don't see a major advantage

[Kevin Buzzard]

It's a glimpse of what lean might look like in the future, which is I guess a big deal for mathematicians

[Mario Carneiro]

My question is how can we generate this? I can see the benefit but just saying "wouldn't it be nice" doesn't achieve anything

[Mario Carneiro]

I could go through any file and write the statements in natural language, but that's a labor intensive thing. Unless this proposal is associated to some plan for doing this work automatically there isn't a lot of added value

[Johan Commelin]

I find the proofs even harder to read than the mathlib-proofs

[Kevin Buzzard]

Fabstracts currently has nothing. I guess the suggestion doing the rounds is that it ends up looking something like this.

[Kevin Buzzard]

And of course there won't be proofs in Fabstracts

[Tim Daly]

@Mario Carneiro There is an example of automatic natural language generation in this video: http://media.podcasts.ox.ac.uk/comlab/comsci/2017-09-04-ICFP2017/2017-09-04-ICFP2017-day2-pm-08.mp4 from the site: http://conal.net/papers/compiling-to-categories/

and also this PhD thesis which is somewhat related: http://icr.uni.lu/mcramer/downloads/doktor.pdf

[Tim Daly]

@Mario Carneiro also see: https://link.springer.com/content/pdf/10.1007%2Fs10817-016-9377-1.pdf A Fully Automatic Theorem Prover with Human-Style Output

[Johan Commelin]

@Tim Daly The tidy tactic is heavily inspired by the Ganesalingam–Gowers paper.

[Johan Commelin]

The proof scripts generated by tidy could probably be transformed into human readable proofs without too much effort.