Translation of proofs from Natural Language to Lean
Project description
natural2lean
Proof of concept of a natural language interactive theorem prover
This project was developed for my Master's Thesis at UCLouvain (under the supervision of Pr. François Glineur and T.A. Sébastien Mattenet). The problem this project attempts to solve is the feedback on exercice proofs written by students, as this feedback comes either in the form of one correct version of the proof (although a theorem can be proved in many different ways), or taking up valuable T.A. time to correct simple proofs. The aim is therefore to bring machine verification to natural language proofs. This is done by translating natural language to lean4
and returning the feedback to the user.
How this project works
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 optionallean_project_directory
indicates to the program where to store the project.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 tonew_theorem
ornew_statement
depending on the context (whether or not there is a goal to be solved).interpretation_feedback()
; gives a feedback what parts of thestring
were used and what parts were ignored.backtrack()
; removes the last theorem / statement added.
How to install
You will need to first install lean4
(install guide).
For an end user, the easiest way to use it is to use the natural2lean-cli package, gives access to an executable (natural2lean
) containing an interactive program and a file reader.
How to tweak this project for your own uses
This project is a proof of concept, feel free to fork and tweak it for your own uses.
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
File details
Details for the file natural2lean-0.0.6.tar.gz
.
File metadata
- Download URL: natural2lean-0.0.6.tar.gz
- Upload date:
- Size: 29.3 kB
- Tags: Source
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/4.0.1 CPython/3.9.12
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 | 0a1e5bd7a287f5e020d6c1a4b971fbc4439f79ccea888b28da03e24ffbcfbef3 |
|
MD5 | ba2e3808bec7b9f815ba38aeaed57ada |
|
BLAKE2b-256 | f7c7348187bbf22a72730ea983748bc17e2bd0a87d584cb554db3652d06268d0 |
File details
Details for the file natural2lean-0.0.6-py3-none-any.whl
.
File metadata
- Download URL: natural2lean-0.0.6-py3-none-any.whl
- Upload date:
- Size: 41.3 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/4.0.1 CPython/3.9.12
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 | 8fcb814a5388312e7dae6bfcd924f9c41cb6b398523c435dcf3648caf0143224 |
|
MD5 | d215e4bc94d2dbe4575cd12b8f0974fe |
|
BLAKE2b-256 | 1628c70c71c7c72a0e7e46413fee567f85992cf47fe6e7624daa48de3a7bcad6 |