Lean project for Illinois Geometry Lab @ University of Illinois at Urbana-Champaign. This project started in Fall 2020 and is continuing in Spring 2021.
We formalize languages, structures, terms, formulae, sentences, first-order logic, Model theory, and O-minimality in the Lean theorem prover.
Install leanproject
from this
link
following the instructions for your OS.
Navigate to the folder where you would like to clone this project.
Run the following $ leanproject get vaibhavkarve/igl2020
in your
terminal or command prompt. This will create a new folder called
igl2020
and it will copy mathlib oleans into it.
You do not need to run leanproject get ...
after the first time. To
get updated versions of all the files in this repository, you can run
standard git commands like git pull
as often as you want.
All working code can be found in the src/
folder. No changes will be
made to files outside the src/
folder.