Zulip Chat Archive

Stream: new members

Topic: Controlled Natural Language

Lucas Teixeira (Oct 26 2021 at 09:36):

Has there been any work on creating a controlled natural language for lean??

Eric Wieser (Oct 26 2021 at 09:38):

I think @Patrick Massot experimented with something like this for teaching use (but in french), but I don't know if there's a writeup anywhere about it.

Scott Morrison (Oct 26 2021 at 09:40):

See https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/

Scott Morrison (Oct 26 2021 at 09:40):

http://aitp-conference.org/2020/abstract/paper_20.pdf

Scott Morrison (Oct 26 2021 at 09:41):

https://github.com/PatrickMassot/lean-bavard/blob/master/src/exemples/05_limite_suite_correction.lean

Scott Morrison (Oct 26 2021 at 09:41):

(This one is an example from Patrick's experiment.)

Lucas Teixeira (Oct 26 2021 at 10:27):

Scott Morrison said:

http://aitp-conference.org/2020/abstract/paper_20.pdf

Is Hale's project open source?? Is there anyway to experiment with it and/or contribute to it?

Johan Commelin (Oct 26 2021 at 11:50):

There is https://github.com/formalabstracts/CNL-CIC

Last updated: Dec 20 2023 at 11:08 UTC