These directions assume that you already have LEAN, lake, and elan installed. So far this has only been done on a Mac, so you may need to set up a codespace if not on Linux (see https://github.com/Vilin97/autoformalization-with-llms-fork).
- Install poetry.
- Run
poetry install --no-root - To run a file run
poetry run python my/path/to/main.py
This project was done as part of UW's Math 480B (Spring 2025) course. A link to our presentation is here