Models and datasets for Formal Theorem Proving with Lean World Models: continued pretraining, proof repair, GRPO, and informal reasoning.
AI & ML interests
AI for mathematics, including formal mathematics and theorem proving in Lean, and AI for verified software engineering.
Recent Activity
View all 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
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
models 10
EPFL-LARA/lean-feedback-qwen3-4b
Text Generation • 4B • Updated • 820
EPFL-LARA/lean-one-token-qwen3-8b
Text Classification • 8B • Updated • 34
EPFL-LARA/lean-encoder-modernbert-large
Text Classification • 0.4B • Updated • 25
EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo
Text Generation • 8B • Updated • 614
EPFL-LARA/lean-world-model-qwen3-8b-reasoning-grpo
Text Generation • 8B • Updated • 600
EPFL-LARA/lean-standard-prover-qwen3-8b-grpo
Text Generation • 8B • Updated • 592
EPFL-LARA/lean-world-model-qwen3-4b-grpo
Text Generation • 4B • Updated • 607
EPFL-LARA/lean-world-model-qwen3-8b-grpo
Text Generation • 8B • Updated • 599
EPFL-LARA/lean-standard-prover-qwen3-8b-sft
Text Generation • 8B • Updated • 587 • 1
EPFL-LARA/lean-world-model-qwen3-8b-sft
Text Generation • 8B • Updated • 595
datasets 5
EPFL-LARA/lean-world-model-reasoning-sft
Viewer • Updated • 178k • 45 • 1
EPFL-LARA/lean-world-model-sft
Preview • Updated • 38
EPFL-LARA/lean-world-model-cpt
Viewer • Updated • 470k • 41 • 1
EPFL-LARA/lean-evaluation-benchmark
Viewer • Updated • 68.9k • 239
EPFL-LARA/lean-compiler-training-corpus
Viewer • Updated • 4.84M • 50