Computer-Assisted Formalization of Mathematics

Announcements

Sep 23

Today's class will meet on Zoom. Join the meeting.

Aug 26

The first class is Wednesday, September 2. Join on Zoom. Bring a laptop. Before class, you can try to install Lean and the VS Code extension, but we will not need it on the first day. We will begin with the Natural Number Game.

Schedule and course materials

Lecture files and course worksheets will be linked from the corresponding week as the semester runs.

Fall 2026 course schedule
Date	Lean concepts	Applications	Course work
Sep 2	Introduction to LeanExpressions, definitions, theorem statements, the editor, and Infoview.	Elementary arithmetic with the Natural Number Game.	Lean setup
W1 `Lecture01.lean`GitHub repo · Live Lean Lecture slides Lean Game Server Lean installation guide You may find these slides interesting as well
Sep 9	Logic, proof terms, and tacticsProofs as terms; logical connectives; forward and backward reasoning.	Proofs in elementary logic and combinatorics. Two ways of writing proofs in Lean.	Homework 1
W2 `Lecture02.lean`GitHub repo · Live Lean Lecture slides Discussion Section (Completed) Strongly recommended reading, not specifically for Week 2 but for understanding mathematics in the times of formalization.
Sep 16	Dependent type theoryDependent functions, definitional equality, polymorphism, and universes.	Types as specifications: subtypes, vectors, matrices, & continuous functions.	Quiz 1
W3 `Lecture03.lean`GitHub repo · Live Lean Lecture slides Discussion Section
Sep 23	Inductive types, recursion, and inductionInductive data and propositions; structural recursion and induction.	Proving theorems about lists and trees.	Homework 2
W4 `Lecture04.lean`GitHub repo · Live Lean Lecture slides Discussion Section Live Lean
Sep 30	Structures, typeclasses, and algebraic structuresInstances, inheritance, synthesis, and generic theorems.	Build a small hierarchy of algebraic structures.	Quiz 2
W5 `Lecture05.lean`GitHub repo · Live Lean Discussion Section Live Lean
Oct 7	Error-correcting codes in LeanBuild a small mathematical theory from definitions: Hamming distance, finite codes, linear maps, decoders, and counting bounds.	Repetition, parity-check, and the [7,4,3] Hamming code.	—
W6 `Lecture06.lean`GitHub repo · Live Lean
Oct 14	No classLegislative Day: NYU follows a Monday schedule.	—	—
Materials Lean at scale: caching, reproducible projects, and tooling (slides)
Oct 21	Introduction to monadsOption, bind, do notation, and the monad laws.	Safe arithmetic evaluation and a stateful counter.	Homework 3
W7 `Lecture07.lean`GitHub repo · Live Lean Discussion Section Live Lean
Oct 28	Functors, applicatives, and IOMapping, accumulating validation, monadic sequencing, and loops in do notation.	Read, validate, and evaluate a table of calculations.	—
W8 `Lecture08.lean (Problems)`GitHub repo · Live Lean `Lecture08_Solution.lean (Solutions)`GitHub repo · Live Lean Lecture slides Running the worksheet
Nov 4	Metaprogramming I: Lean under the hoodNotation, syntax trees, macros, and the first steps in TacticM.	Extend our arithmetic language and write small tactics.	Homework 4 (triangle) Quiz 3
W9 `Lecture09.lean (Problems)`GitHub repo · Live Lean `Lecture09_Solution.lean (Solutions)`GitHub repo · Live Lean Lecture slides
Nov 11	Metaprogramming II: Asking another computerExpressions, metavariables, tactic construction, and external results.	Call a Python sum-of-squares library and verify its certificate in Lean.	—
W10 Lecture10.lean (Problems) Lecture10_Solution.lean (Solutions) Lecture10_Instructor.lean (Instructor) Lecture slides Python setup and class instructions Python setup script Python SOS adapter
Nov 18W11	Metaprogramming III: Trusted proof automationReflection, certificates, and the boundary between trusted and untrusted computation.	Build a small sum-of-squares certificate checker.	Make-up quizzes
Nov 25W12	Program verificationSpecifications, correctness, termination, and inductive semantics.	Operational semantics and Hoare logic.	Project work
Dec 2W13	Agentic Lean proof generation I	Explore a generate–check–retry proof agent.	Project work
Dec 9W14	Agentic Lean proof generation II	Run and evaluate an existing prover-training system.	Project work

Weeks 10–14. The discussion section may split into an advanced mathematics track (for example, topology and measure theory) and an AI4Lean track (proof search, agents, and reinforcement learning).

The plan may change slightly as the semester progresses.

Course work

Homework 1–4. Lean worksheets due at the end of weeks 2, 4, 7, and 9. Submission is through Gradescope.
Quizzes 1–3. Short in-person quizzes in lab during weeks 3, 5, and 9.
Final project. Project instructions and the due date will be posted here.

Books and Lean files

The course draws from these online books and their accompanying Lean repositories.

Main references

Mathematics in Lean(MiL) — Jeremy Avigad and Patrick Massottext · GitHub repo
Theorem Proving in Lean 4(TPiL) — Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich, with contributions from the Lean Communitytext · GitHub repo
Functional Programming in Lean(FPiL) — David Thrane Christiansentext · GitHub repo
Metaprogramming in Lean 4(MPiL) — Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, and Siddharth Bhattext · GitHub repo

Additional references

The Mechanics of Proof(MoP) — Heather Macbethtext · GitHub repo
The Hitchhiker's Guide to Logical Verification — 2026 edition(LoVe) — Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Xavier Généreux, Johannes Hölzl, and Jannis Limpergtext · GitHub repo

Setup and reference

Course information

Instructor: Jaume de Dios Pont · jdedios@nyu.edu
Office hours: Tuesdays, 4–5 pm · 60 Fifth Avenue, office 615
Teaching assistant: Niket Patel · nnp5656@nyu.edu
TA office hours: Fridays, 2–3 pm · 60 Fifth Avenue, CDS room 244 · No office hours Friday, Nov 6
Discussion section: Thursdays, 11:15 am–12:05 pm · Tisch Hall (40 W 4th St), room LC9
Zoom: Join meeting
Syllabus: PDF