Hugging Face's logo
Activity Feed Request to join this org

AI & ML interests

AI for mathematics, including formal mathematics and theorem proving in Lean, and AI for verified software engineering.

Recent Activity
Lemmy00  updated a collection about 10 hours ago
Proof Optimization
Lemmy00  updated a model about 10 hours ago
EPFL-LARA/Qwen3.8-Flash-Next-ProofOpt-BestPathSFT-20261103-epoch2-FP8
Lemmy00  published a model about 10 hours ago
EPFL-LARA/Qwen3.8-Flash-Next-ProofOpt-BestPathSFT-20261103-epoch2-FP8
View all activity

Organization Card
Community About org cards

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

Collections 3

Formal Theorem Proving with Lean World Models
Models and datasets for Formal Theorem Proving with Lean World Models: continued pretraining, proof repair, GRPO, and informal reasoning.
Formal Theorem Proving with Lean World Models
Models and datasets for Formal Theorem Proving with Lean World Models: continued pretraining, proof repair, GRPO, and informal reasoning.
View 3 collections