igl2020

Lean project for Illinois Geometry Lab @ University of Illinois at Urbana-Champaign. This project started in Fall 2020 and is continuing in Spring 2021.

Aim

We formalize languages, structures, terms, formulae, sentences, first-order logic, Model theory, and O-minimality in the Lean theorem prover.

Participants

1. Tyler Behme
2. Eion Blanchard
3. Scott Harman
4. Philipp Hieronymi
5. Vaibhav Karve
6. Nikil Ravi
7. Joel Schargorodsky
8. Kay Thompson
9. Noble Wulffraat
10. Tianfan Xu
11. Andrew Yin
12. Fenglong Zhao

Installation

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.

Updating the project

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.

Files

All working code can be found in the src/ folder. No changes will be made to files outside the src/ folder.