Introduction to Theorem Proving Using Lean 4 is an interactive workshop on formal reasoning and proof systems. Participants will learn the fundamentals of Interactive Theorem Proving (ITP) using Lean 4, a modern proof assistant widely used in mathematics, software verification, and formal methods research. The workshop introduces key concepts such as the Curry–Howard Correspondence and demonstrates how logical propositions can be represented as types and proofs as programs through hands-on exercises in propositional logic.
.jpg)
.jpg){kind=logo}