An LLM-based Lean4 Theorem Prover, augmented with Monte-Carlo Tree Search, Reinforcement Learning, and Lean4 Verification.
This project is a part of the GDSC UTM Reading Course CSC392, and the approach is predominantly based on https://github.com/deepseek-ai/DeepSeek-Prover-V1.5, following the analysis from https://medium.com/@haitham.bouammar71/new-grounds-in-theorem-proving-with-deepseek-prover-v1-5-681c4e41caba.
Currently a work in progress.