Summer School:
Proof Engineering with 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.