## Stream: maths

### Topic: group.lean in natural language

#### Kevin Buzzard (Jun 10 2019 at 21:50):

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 (Jun 10 2019 at 21:53):

[the .ftl file is a text file]

#### Kevin Buzzard (Jun 10 2019 at 21:57):

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

#### Kevin Buzzard (Jun 10 2019 at 21:58):

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

#### Mario Carneiro (Jun 10 2019 at 22:14):

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 (Jun 10 2019 at 22:57):

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

#### Mario Carneiro (Jun 10 2019 at 23:03):

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 (Jun 10 2019 at 23:05):

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 (Jun 11 2019 at 05:29):

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

#### Kevin Buzzard (Jun 11 2019 at 06:56):

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

#### Kevin Buzzard (Jun 11 2019 at 06:56):

And of course there won't be proofs in Fabstracts

#### Tim Daly (Jun 12 2019 at 15:56):

@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/

#### Tim Daly (Jun 12 2019 at 16:42):

@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 (Jun 12 2019 at 16:51):

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

#### Johan Commelin (Jun 12 2019 at 16:51):

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

Last updated: May 19 2021 at 03:22 UTC