An interface between Lean and Oscar. To see what is already working take a look at test.lean. I added the write up of my master's thesis for more detailed information. Feedback and questions are always welcome!
You need to install Lean and install Oscar
Clone the repository:
git clone https://github.com/todbeibrot/Lean-Oscar.git
Navigate to the project directory:
cd Lean-Oscar
Build the project:
lake exe cache get
and
lake build
Then, open test.lean and see if everything compiles.