This project develops an agent system that translates natural-language mathematics into Lean4 code,
fills by sorry, and verifies correctness through theorem checking,
REPL feedback, and other tools via iterative refinement. The system will be extended to support
full theorem proving.
Here is the GitHub repo.
If the poster does not display, you can open it in a new tab.