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-standard-prover-qwen3-8b-reasoning-grpo
Text Generation • 8B • Updated • 1.42k
EPFL-LARA/lean-world-model-qwen3-8b-reasoning-grpo
Text Generation • 8B • Updated • 1.47k
EPFL-LARA/lean-standard-prover-qwen3-8b-grpo
Text Generation • 8B • Updated • 1.43k
EPFL-LARA/lean-world-model-qwen3-4b-grpo
Text Generation • 4B • Updated • 1.4k
EPFL-LARA/lean-world-model-qwen3-8b-grpo
Text Generation • 8B • Updated • 1.44k
EPFL-LARA/lean-standard-prover-qwen3-8b-sft
Text Generation • 8B • Updated • 1.34k • 1
EPFL-LARA/lean-world-model-qwen3-8b-sft
Text Generation • 8B • Updated • 1.34k
EPFL-LARA/lean-feedback-qwen3-4b
Text Generation • 4B • Updated • 1.52k
EPFL-LARA/lean-one-token-qwen3-8b
Text Classification • 8B • Updated • 41
EPFL-LARA/lean-encoder-modernbert-large
Text Classification • 0.4B • Updated • 36
datasets 7
EPFL-LARA/lean-refactor-arena-assets-20261104
Updated • 73
EPFL-LARA/ProofOpt-Reasoning-Tools
Viewer • Updated • 7.58k • 97
EPFL-LARA/lean-evaluation-benchmark
Viewer • Updated • 68.9k • 699
EPFL-LARA/lean-compiler-training-corpus
Viewer • Updated • 4.84M • 190
EPFL-LARA/lean-world-model-reasoning-sft
Viewer • Updated • 178k • 268 • 1
EPFL-LARA/lean-world-model-sft
Preview • Updated • 811
EPFL-LARA/lean-world-model-cpt
Viewer • Updated • 470k • 170 • 1