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):
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.
Last updated: May 14 2021 at 23:14 UTC