Aim to make an open source replication of the AlphaProof paper
In addition to replicating AlphaProof we aim to hit some other ai theorem proving landmarks along the way as well as some additions.
- pretrain a SLM (small language model) on lean4 code (eg proof-pile-2).
- RAG (retrevial augmented) SLM for premise selection and integrate with Lean Copilot
- RL based self-supervised curriculumn based theorem proving using MCTS/rmax (alpha proof paper)
- few shot curriculumn based theorem proving on utm undergraduate math content (mat137/mat139, mat157/mat159/mat257, csc236)
- make llm predict aesop rule applications rather than tactic applications (this will allows us to train directly on mathlib4 rather than on custom curated dataset for the pretraining knowledge aquisition phase)