natural2lean

Translation of natural language proofs to lean4 for verification. The objective was to make a proof of concept of the translation system. This project is developed for a master's thesis under the supervision of François Glineur and Sébastien Mattenet.

The project consists of a python package, natural2lean, giving access to a Translator class. This class contains the following methods:

• __init__(lean_project_directory: str = None); creates the object and makes sure that it has access to the needed lean-project-template. The optional lean_project_directory indicates to the program where to store the project template.
• new_theorem(string: str); parses the string into a new theorem and returns the state of the proof after the theorem was added.
• new_statement(string: str); parses the string into a new statement and returns the state of the proof after the statement was added.
• new(string: str); delegates new_theorem or new_statement depending on the context (whether or not there is a goal to be solved).
• backtrack(); removes the last theorem / statement added

Installation

1. Install lean4 (install guide)
2. Install the project (pip install .)

How the system works

The system will try to understand the meaning of the natural language sentences by matching specific keywords. Spaces are optional and the system will raise a TranslationError (natural2lean.utils.exceptions) if it could not parse the string, or a LeanError if the translated string was not accepted by lean.

Theorem statements

• A theorem statement is simply an implication you want to prove. if [...] then [...] will be matched, and hypotheses / theses will be extracted from that.
• You can also define a theorem name, by writing theorem [...] : if [...] then [...].

Statements

• For now, most statements need the have keyword. The system will try to match a substatement on the right of the have keyword and will try to find the proof of that substatement in the sentence. Any equation should be solved automatically, and in addition to that, the keys in natural2lean.text.have.PROOFS will also be understood.
• You can also conclude a goal by simply stating it (for example, if your goal is to prove that $m^2$ is even, then stating $m^2$ is even will work).
• You can add words to make your proof more readable, such as Hence, $m^2$ is even, even though just writing $m^2$ even will have the same effect.

Working examples

• if $m \in \mathbb{N}$ is even, then $m^2$ is even
• if $q \in \mathbb{N}$ is not divisible by $3$, then $q^2 \mod 3 = 1$

Contributing

To install natural2lean along with the tools you need to develop and run the tests, run the following in your virtual environnment :

pip install -e .[dev]

Note that if you use zsh, you need to run the following instead :

pip install -e .'[dev]'