Berlin Formal Methods & Software Verification Meetup

Meetup 2 — Type Classes & First Taste of Proofs
This session introduces type classes — Lean's mechanism for overloading and abstraction, and the foundation for almost everything that follows, including functors and monads. We'll cover how to define instances, how Lean searches for them, and the standard classes you'll reach for constantly. In the second half we take a first look at one of Lean's defining features: propositions as types, the idea that a proof is simply a value whose type happens to be a statement. These first proofs are kept small and approachable, so you can build intuition before the proving sessions that follow.
Reading (before the meetup)
FPiL: Overloading and Type Classes + Interlude: Propositions, Proofs, and Indexing
TPiL: Dependent Type Theory; skim Interacting with Lean as reference.
In session
Type classes vs. interfaces, instance search, coercions, standard classes.
First encounter with `Prop` and propositions-as-types.
Exercises — FPiL Ch 3 · Overloading and Type Classes
- Ex 1 (§3.1 Positive Numbers), Ex 6 (§3.3 Controlling Instance Search), Ex 8 (§3.5 Standard Classes)
Exercises — FPiL Interlude · Propositions, Proofs, and Indexing
- Ex 1, 2, 3 (chapter Exercises — the Interlude is unnumbered)

Meetup 3 — Propositions & Proofs (the Proving Core)
This is the conceptual core of the series: writing proofs in Lean. We'll work with the logical connectives — and, or, not, implication — together with the quantifiers and equality, and learn to construct proofs directly, by hand. Building proofs this way first gives a clear
sense of what a proof actually is before we automate the process with tactics in the next session. This is the most demanding material in the series, so the evening is paced deliberately, with plenty of room for questions and discussion. A little familiarity with the previous
session's introduction to propositions-as-types will help.
Reading (before the meetup)
- TPiL Ch 3–4: Propositions and Proofs → Quantifiers and Equality
In session
- Implication, And/Or/Not, ∀/∃, equality, Iff.
- Building proof terms by hand (tactics come next meetup).
Exercises — TPiL Ch 3 · Propositions and Proofs (§3.7)
- Exercise 1 (all parts), Exercise 3
Exercises — TPiL Ch 4 · Quantifiers and Equality (§4.6)
- Exercise 1, Exercise 3