Laboratory for Automated Reasoning and Analysis
LARA develops AI systems for mathematical reasoning and tools for constructing formally verified software. We work on autoformalization and neural theorem proving in Lean 4, deductive verification of Scala programs, and the logical foundations of proof assistants. The lab is part of the School of Computer and Communication Sciences at EPFL and is led by Viktor Kunčak.
-- 1 + 3 + 5 + ⋯ + (2n − 1) = n²
theorem odd_sum (n : ℕ) :
∑ i ∈ range n, (2 * i + 1) = n ^ 2 := by
induction n with
| zero => simp
| succ n ih =>
rw [sum_range_succ, ih]; ringResearch
AI for mathematics
We build agentic workflows, neural theorem provers, learned compiler feedback models, and benchmarks for formal mathematics in Lean 4. Together with colleagues across EPFL, we co-lead the AI for Math @ EPFL initiative on document-level autoformalization.
Verified software
We design deductive verification tools, decision procedures, and refinement type systems to prove that real-world Scala programs and libraries meet their specifications.
Logic & proof assistants
We study foundational proof systems based on first-order logic and set theory, polynomial-time proof normalization in ortholattices, and mechanized mathematics.
Recent work
People
- Simon Guilloud (PhD)
- Dragana Milovančević (PhD)
- Mario Bucev (PhD)
- Rodrigo Raya (PhD)
- Jad Hamza (PhD / Postdoc)
- Romain Edelmann (PhD)
- Georg S. Schmid (PhD)
- Nicolas Voirol (PhD)
- Andreas Pavlogiannis (Postdoc)
- Mikaël Mayer (PhD)
- Ravichandhran Madhavan (PhD)
- Etienne Kneuss (PhD)
- Andrew J. Reynolds (Postdoc)
- Eva Darulova (PhD)
- Ruzica Piskac (PhD)
- Philippe Suter (PhD)
Selected recent publications
Teaching & joining
Courses. We teach CS-550: Formal Verification (with lecture videos on SwitchTube) as well as undergraduate courses in logic, discrete mathematics, and software construction at EPFL.
Tutorials. For an introduction to verifying Scala programs with Stainless, see our ASPLOS tutorial and the Stainless documentation.
EPFL students. If you are looking for a BS/MS semester project or Master's thesis in AI for mathematics, Lean 4 autoformalization, or program verification, email Viktor Kunčak or one of the PhD students with your CV and transcript.
Prospective students. PhD admissions are handled through the EDIC doctoral program. For inquiries, contact viktor.kuncak@epfl.ch.