Skip to main content

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 optional lean_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 to new_theorem or new_statement depending on the context (whether or not there is a goal to be solved).
  • interpretation_feedback(); gives a feedback what parts of the string 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

natural2lean-0.0.6.tar.gz (29.3 kB view details)

Uploaded Source

Built Distribution

natural2lean-0.0.6-py3-none-any.whl (41.3 kB view details)

Uploaded Python 3

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

Hashes for natural2lean-0.0.6.tar.gz
Algorithm Hash digest
SHA256 0a1e5bd7a287f5e020d6c1a4b971fbc4439f79ccea888b28da03e24ffbcfbef3
MD5 ba2e3808bec7b9f815ba38aeaed57ada
BLAKE2b-256 f7c7348187bbf22a72730ea983748bc17e2bd0a87d584cb554db3652d06268d0

See more details on using hashes here.

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

Hashes for natural2lean-0.0.6-py3-none-any.whl
Algorithm Hash digest
SHA256 8fcb814a5388312e7dae6bfcd924f9c41cb6b398523c435dcf3648caf0143224
MD5 d215e4bc94d2dbe4575cd12b8f0974fe
BLAKE2b-256 1628c70c71c7c72a0e7e46413fee567f85992cf47fe6e7624daa48de3a7bcad6

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page