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.
Attendance is limited to 30 participants, with a few spots reserved for highly motivated high school students.
Deadline: June 30.
Thank you! Your registration will be processed shortly. If you don't receive an email from the organizer within 3 days, please contact them directly.