Zulip Chat Archive

Stream: general

Topic: Natural language translation


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

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 09:58):

There was just a talk about this at CICM

view this post on Zulip Kenny Lau (Jul 31 2020 at 10:00):

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

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

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

view this post on Zulip Gihan Marasingha (Jul 31 2020 at 10:19):

Thanks!

view this post on Zulip Gihan Marasingha (Jul 31 2020 at 10:23):

Are there recordings of the talks?

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

view this post on Zulip Jason Rute (Jul 31 2020 at 10:49):

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

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