Week 6: Formalizing Mathematics and Contributing to Mathlib (Guest Session, AUB Math Society)

Overview

Co-organized with the AUB Math Society, this hands-on session by Rida Hamadani will show you the complete workflow of mathematical formalization in Lean4: from reading a theorem on paper to contributing verified mathematical proofs to Mathlib or CSlib. Learn how to navigate the library, find existing theorems, use the Blueprint system for large-scale formalization projects, and interact with the Lean community effectively.

Guest Lecturer

• Rida Hamadani (they/them) — Mathematical formalization researcher, former Lean Expert at Harmonic, Graduate student in resurgence theory (LMAP, France) | Website

Session Information

• Date and Time: Wednesday 25 February, 15:00 — 17:00 (Beirut time)
• Place: Online
• Online Meeting Link (Meeting Number: 2391 464 2135; Password: UqpxacU*385)

Please note: This session will not be recorded as the guest lecturer has requested that no recording be made during the presentation.

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!

Navigation

• ← Previous Week: Proofs & Semantics
• Back to Course Overview
• Next Week: Mathematical Foundations of Proof Assistants →

Questions? Reach out on the course Discord!