Lean Summer School 2026

Summer School:
Proof Engineering with Lean

Lean is an interactive theorem prover and functional programming language used for formalizing mathematics and formally verifying software. By bridging theoretical mathematics and software development, it empowers researchers and engineers to construct, collaborate on, and verify both complex mathematical proofs and critical code. Based on dependent type theory and supported by a growing community library (mathlib), Lean provides a practical framework for translating mathematical reasoning and software behavior into rigorous, machine-verified engineering artifacts.

calendar_month 21-24 September 2026
location_on Clădirea Mathematica, Cluj-Napoca
theorem hello_world (a b : Nat) :
  a + b = b + a := by
  simp [Nat.add_comm]
code

Materials & Community

Most of the material for the school lives in the GitHub repository. Discussions, questions and announcements happen on Zulip.

Discussions & announcements forum

Zulip

Ask questions, get help with your setup, and follow announcements before and during the school.

lean-cj-2026.zulipchat.com
Course material code

GitHub repository

Most of the material for the four days: exercises, Lean sources and setup instructions.

github.com/Lean-Cluj/summer-school-2026

Registration

Registration for the summer school closed on June 30. If you have any inquiries, please contact the organizers.