Zulip Chat Archive

Stream: general

Topic: Natural language translation


Gihan Marasingha (Jul 31 2020 at 09:27):

Has there been any work on translation of Lean proofs into natural language proofs (or vice-versa)? A colleague of mine at Exeter is interested in pursuing the idea.

Kevin Buzzard (Jul 31 2020 at 09:58):

There was just a talk about this at CICM

Kenny Lau (Jul 31 2020 at 10:00):

I think the "vice versa" part will be a bit difficult

Utensil Song (Jul 31 2020 at 10:04):

Heard on CICM Slack:

https://github.com/leanprover/lean4/blob/master/tests/playground/forthelean/ForTheLean/Demo.lean : directly parse a controlled natural language in Lean 4

https://github.com/adelon/naproche-cic : a working (experimental) translation from a controlled natural language to Lean.

Mario Carneiro (Jul 31 2020 at 10:07):

Also, parsing of natural language directly into formal mathematics (of some description) was in part the topic of Szegedy's talk

Gihan Marasingha (Jul 31 2020 at 10:19):

Thanks!

Gihan Marasingha (Jul 31 2020 at 10:23):

Are there recordings of the talks?

Jason Rute (Jul 31 2020 at 10:48):

The vice versa approach (natural to formal) would require significant advancements in AI, but nonetheless that is what Szegedy’s N2Formal group at Google research is pursuing. The talk is not recorded, but there is a paper. Note, the paper and talk are more vision than results. However Szegedy’s does argue that a lot of related technologies already exist.

Jason Rute (Jul 31 2020 at 10:49):

Controlled natural language is of course another story since it is formal and can be parsed.

Jason Rute (Jul 31 2020 at 10:54):

Urban is also working on machine learning assisted auto-formalization. Here are some slides.

Barrie Cooper (Jul 30 2021 at 16:59):

Just wondering if there have been any further developments on this ... particularly the first part: Lean proof to Natural Language, like Mizar does in terms of producing a stylised human-readable translation. (I was the colleague at Exeter to whom @Gihan Marasingha was referring.)

At the very least, from the viewpoint of teaching Lean and teaching students to write better (non-Lean) proofs, I think it would be very useful (e.g. parallel presentation of materials). It potentially (but not necessarily) assists with the other direction also ... Natural Language to Lean proofs.

Patrick Massot (Jul 30 2021 at 17:22):

It's fairly easy to teach Lean how to read proofs in fake controlled natural language. If you can read French math then you can have a look at https://github.com/PatrickMassot/lean-bavard, especially the example file https://github.com/PatrickMassot/lean-bavard/blob/master/src/exemples/05_limite_suite_correction.lean

Patrick Massot (Jul 30 2021 at 17:22):

This was used for real with first year undergrads. The goal of this pseudo-natural language was to make it easier to go from Lean to paper.


Last updated: Dec 20 2023 at 11:08 UTC