Week 6: Tactic-Based Proving II — Forward Proofs & Induction

Overview

Guest Lecturer

  • Daniel Dia — Course creator, primary instructor & organizer (American University of Beirut); Computer & Communications Engineering (CCE) and Mathematics dual-degree student (AUB).

Session Information

Core Concepts

  • Approaching mathematical theorems: from paper to Lean4 workflow (reading theorem, identifying dependencies, translating mathematical notation to Lean syntax)
  • Navigating Mathlib and CSlib: organization (modules, namespaces, hierarchies), using online documentation, finding existing theorems, search strategies and common patterns
  • The Blueprint system: what Blueprint is and why it matters, how large Lean projects use Blueprint for coordination (tracking progress, dependencies), reading and contributing to Blueprint documentation, real examples from major formalization projects
  • The formalization workflow: writing (breaking down proofs into manageable pieces), testing (checking intermediate steps), documenting (clear docstrings and comments), refining (incorporating community feedback)
  • Interacting with the Lean community: Lean Zulip (asking questions effectively), getting feedback on contributions, understanding review processes, learning from others’ contributions
  • Finding good projects: identifying contribution opportunities, matching projects to interests and skill level, understanding what makes a good first contribution
  • Real-world examples: examining actual Mathlib contributions, common patterns and best practices, learning from merged pull requests

Slides

Week 6 Slides: Download PDF

We have covered a lot of different Mathlib PRs in the hands-on session with Rida, but one particularly stood out (with an interesting proof by induction). Here it is for the students’ reference: https://github.com/leanprover-community/mathlib4/pull/33506

Readings

  1. Undergraduate Mathematics in Mathlib

Programming Assignment

Assignment 5: Tactic-based Theorem Proving in Lean

Objective: Progress from warm-up tactic exercises to inductive proofs on natural numbers, lists, and binary trees.

Assignment: PROOF101 Programming Assignment 5

Note: If you haven’t finished Programming Assignment 4, i.e. The Natural Number Game (Lean Game Server), from weeks 4 and 5, please do!

Questions? Reach out on the course Zulip!