Companion resources for "Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs": three models and two datasets.
AI & ML interests
AI for mathematics, including formal mathematics and theorem proving in Lean, and AI for verified software engineering.
Recent Activity
Organization Card
LARA — Lab for Automated Reasoning and Analysis (EPFL)
We build AI for mathematics and verified software: formal mathematics and theorem proving in Lean 4, and AI for verified software engineering.
🌐 lara.epfl.ch · 🏛️ EPFL
Lean compiler emulation
Learned models that predict whether a Lean 4 program compiles, and what the compiler would say, without running Lean.
| Model | Size | What it does |
|---|---|---|
| lean-encoder-modernbert-large | 395M | Fast validity scoring (~264 candidates/s on one H100) |
| lean-one-token-qwen3-8b | 8B | One-token validity scoring (0.905 AUROC) |
| lean-feedback-qwen3-4b | 4B | Generates predicted goal states and compiler diagnostics |
| Dataset | Description |
|---|---|
| lean-compiler-training-corpus | 4.8M compiler-labelled Lean 4 programs with verdicts and feedback |
| lean-evaluation-benchmark | Evaluation benchmark for Lean validity prediction |
📄 Paper: Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs
Publications
- Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs. Lazar Milikic, Etienne Bamas, Emmanuel Abbe, Viktor Kunčak. arXiv:2610.21881
- LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization. Lazar Milikić, Simon Guilloud, Khanh Nguyen, Viktor Kunčak. arXiv:2607.20503