Natural language translation

Stream: general

[Gihan Marasingha]

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]

There was just a talk about this at CICM

[Kenny Lau]

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

[Utensil Song]

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]

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

[Gihan Marasingha]

Thanks!

[Gihan Marasingha]

Are there recordings of the talks?

[Jason Rute]

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]

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

[Jason Rute]

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

[Barrie Cooper]

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]

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]

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.