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: Engineering Lecture Hall (ELH)
• Online Meeting Link
• Recording

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

Readings

1. Undergraduate Mathematics in Mathlib

Weekly Quiz

Quiz 6: Mathlib and Community

Quiz Link: Take Quiz 6

Deadline: Before Week 7 session
Passing Score: 60%

Programming Assignment

Assignment 5: Your First Mathlib Exploration

Objective: Navigate Mathlib or CSlib, find relevant theorems, and consider contributing!

Navigation

• ← Previous Week: More on Tactics & Inductive Predicates
• Back to Course Overview
• Next Week: Mathematical Foundations of Proof Assistants →

Questions? Reach out on the course Discord!