PROOF101: Introduction to Formal Verification & Proof Assistants

The Spring 2026 cohort met online over ten consecutive weeks via Webex, with all session recordings published to the course website so participants in incompatible time zones could follow along asynchronously. Live discussion, exercise help, and project mentorship happened on a dedicated course Discord server. All materials — slides, exercises, recordings, and the project gallery — were released openly under CC BY-NC-SA 4.0, so the curriculum can be reused, remixed, and re-taught by anyone willing to credit and share alike.

The ten weeks were organized into four thematic phases, building from the syntactic basics of Lean 4 up to a self-directed verification project.

Phase 1 — Functional Foundations (early weeks). Lean 4 introduced as both a programming language and a proof assistant: installation, type theory basics, function definitions and recursion, inductive types, pattern matching, structural induction, and the propositions-as-types correspondence. Students proved their first theorems in term-mode (writing proof terms directly), built up an intuition for dependent types, and got used to reading Lean4 error messages.

Phase 2 — Tactic-Based Proving (mid-course). The mechanical side of writing proofs: how tactics manipulate the proof state, the standard library of tactics (rfl, simp, rw, exact, apply, cases, induction, omega, decide, …), and the discipline of structuring nontrivial proofs as readable tactic blocks. Anchored by a guest lecture from Rida Hamadani.

Phase 3 — Mathematics, Foundations, and Metaprogramming (later weeks). With the basics in place, the course pivoted to three more advanced themes, each anchored by a guest lecture from an external researcher: working with Mathlib4 (the mathematical library containing over a million lines of formalized mathematics), the theoretical foundations of why proof assistants work at all (λ-calculus, Curry-Howard, normalization), and how to write your own tactics through metaprogramming and decision procedures.

Phase 4 — Final Project (weeks 9–10). Students chose a topic, wrote a LaTeX proposal, implemented a formalization, prepared a README and a presentation, and defended their work in a live session in front of the course team and their peers.

Each week’s session was paired with a set of practical exercises released alongside the slides — Lean4 problems, short proofs, and reading-driven challenges. Exercises were not graded: the course is not for credit, and grading would have crowded out the time needed to actually mentor projects. Instead, exercises served as self-check checkpoints, and the Discord server functioned as a live help channel.

Four guest lectures, each contributing materials, slides, and follow-up exercises that have been incorporated into the open course materials.

• Rida Hamadani (mathematical formalization researcher; formerly Lean Expert at Harmonic; graduate student in resurgence theory at LMAP, France) gave two lectures: Introduction to Tactic-based Proving (Week 4) and Formalizing Mathematics and Contributing to Mathlib4 (Week 6). They also offered to review Mathlib-related and CSlib-related final projects, connecting the course directly to the broader Lean mathematical community.

• Dr. Assaf Kfoury (Professor of Computer Science, Boston University) gave the Week 7 lecture, The Mathematical Foundations of Proof Assistants, with handouts covering (1) the Church-Rosser property, (2) strong normalization of the simply-typed λ-calculus, (3) the Curry-Howard isomorphism, and (4) how these results form the theoretical basis of proof assistants — and Lean4 specifically.

• Dr. Robert Lewis (Associate Teaching Professor of Computer Science, Brown University; instructor of Brown’s CS1715 Formal Proof and Verification) gave the Week 8 lecture, Metaprogramming in Lean and Decision Procedures. He walked the class through three strategic approaches to tactic design — direct proof manipulation (implementing the basic components of Mathlib’s interval_cases, following a tutorial by Heather Macbeth), proof by certificate (the strategy behind linarith), and proof by reflection (proving the correctness of an algorithm in the object language and wrapping it as a tactic). All materials are published in his aub-guest-lecture repository.

The final project was the centerpiece of the course. Each participant developed a formal theory on a topic of their choosing: defining the relevant objects or programs, specifying their behavior, and proving that the specifications hold. The deliverable was rarely large in code volume — “sometimes a lot of thought goes into a short verification” — but had to go meaningfully beyond what was covered in lectures, typically by drawing on Mathlib lemmas and tactics that students had to discover themselves.

Timeline.

• Week 9 — Kickoff. Students began ideating, with the session also covering an applied talk on Lean, Rust, and the Future of Reliable Software.
• Sunday, 5 April — Proposal due. A short LaTeX document covering title, overview (2–3 sentences), the core property to be proven, and anticipated challenges. Each proposal was reviewed by the course team and discussed via email or Discord before approval.
• Friday, 10 April — Presentations. A 3–5 minute live presentation (up to 7 with permission), followed by 2–3 minutes of questions from the course team and peers.

Deliverables.

1. A public or private GitHub repository containing the Lean project (all .lean files compiling without errors).
2. A README.md covering: project overview, design choices, main theorems, proof strategies, and challenges encountered.
3. The presentation itself.

Evaluation rubric.

• Technical Content — 50%. Correctness of definitions, quality of specifications, soundness of proofs.
• Documentation — 25%. Clear README, well-commented code, explanation of proof strategies.
• Presentation — 15%. Clarity, demonstration, time management.
• Creativity — 10%. Novel approach; going beyond course material.

Seven final projects were submitted. The competition produced three placed winners, but every project deserves a mention — the rankings reflect a single live competition, not the relative effort, learning, or quality of the underlying formalization.

Winners.

1. Alisson Matheus Silva — LeanML: Formally Verified Linear Regression — formalized linear regression with machine-checked correctness guarantees (repo).
2. Cristina Dueñas Navarro — Error-Correcting Codes: Disjoint Spheres Theorem — a Lean proof of one of the foundational theorems in coding theory (repo).
3. Madhav Ram — Formally Verified Semilattice Class for Conflict-free Replicated Data Types (CRDTs) — a verified semilattice class for the distributed-systems primitive that underpins eventual consistency (repo).

Other accepted projects.

• Loren Abdulezer — Formalizing Addition in Quadrature with Computational Applications (repo).
• Jad Abou Hawili — Formalizing Knights and Knaves Logic Puzzles in Lean Using Set Theory (repo).
• Pawel Wozniak — JocLean: The Joy of Cryptography in Lean — a Lean translation of constructions from Mike Rosulek’s The Joy of Cryptography (repo).
• Risiraj Dey — Leaf-Binding in a 2-Leaf Merkle Tree: A Lean 4 Proof (repo).

Full proposals and presentation slides for all projects are linked from the course website.

Sessions were paired with chapters from the standard Lean4 reading list, used as both pre-reading and reference:

• Theorem Proving in Lean 4 — the canonical introduction to writing proofs in Lean.
• Functional Programming in Lean 4 — Lean4 as a programming language, by David Thrane Christiansen.
• The Hitchhiker’s Guide to Logical Verification — the textbook for Brown’s CS1715.
• Mathematics in Lean — for Phase 3’s Mathlib material.
• Metaprogramming in Lean 4 — for Week 8.

The course existed because of contributions from many people beyond me. Faculty mentorship from Dr. Kinan Dak al Bab (Boston University) and Dr. Assaf Kfoury (Boston University) shaped the curriculum throughout. The AUB Math Society (Georges Sakr, Mohammad Shouman, Romy Kayrouz, and the broader cabinet) and the GDG on Campus @AUB Software Team (Lynn Hammoud, Antonio Makhoul, and the broader club) provided the organizational scaffolding that made the course runnable as a student-led initiative. Alina Gurskaya designed the course logo and visual identity.

Full credits live on the Contributors page.