Skip to content

EdAyers/lean-humanproof-thesis

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

15 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Implementation of the HumanProof prover system, accompanying https://edayers.com/thesis.

Please note that the system is a prototype.

Installation

Install Lean 3

Make sure that you have installed elan, Visual Studio Code and leanproject. Up-to-date information on how to do this can be found on the leanprover-community website.

Set up the project

git clone https://github.com/EdAyers/lean-humanproof-thesis.git
cd lean-humanproof-thesis
leanpkg configure
leanproject get-mathlib-cache
leanpkg build

Then open the project in VSCode to view the examples.

Usage

The analysis examples used in the thesis can be found in examples/analysis.lean. The equational reasoning examples were generated from a different project https://github.com/EdAyers/lean-subtask. At the time of submission I did not integrate these two modules in to a single system to the extent that I am confident to release the code.

About

Implementation of HumanProof system from https://www.edayers.com/thesis

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages