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 30W5	Structures, typeclasses, and algebraic structuresInstances, inheritance, synthesis, and generic theorems.	Build a small hierarchy of algebraic structures.	Quiz 2
Oct 7W6	Linear algebra in MathlibMathlib's algebraic hierarchy, coercions, and generic theorems.	An application of linear algebra: Linear regression and least squares.	Homework 3
Oct 14	No classLegislative Day: NYU follows a Monday schedule.	—	—
Oct 21W7	Working effectively with MathlibFinding definitions and lemmas; namespaces, rewriting, and automation.	Analysis and optimization examples.	Quiz 3
Oct 28W8	Executable Lean and monadsOption, Except, State, do notation, and IO.	Turn the linear algebra and optimization examples into executable code.	Homework 4
Nov 4W9	Program verificationSpecifications, correctness, termination, and inductive semantics.	Operational semantics and Hoare logic.	Quiz 4
Nov 11W10	Lean under the hoodSyntax, macros, elaboration, expressions, and kernel checking.	Build a small language inside Lean.	Make-up quizzes
Nov 18W11	Tactic metaprogrammingGoals, metavariables, expressions, and recursive tactics.	Build a small positivity tactic.	Project work
Nov 25W12	Trusted proof automationReflection, certificates, and the boundary between trusted and untrusted computation.	Build a small sum-of-squares certificate checker.	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, 6, and 8. Submission is through Gradescope.
Quizzes 1–4. Short in-person quizzes in lab during weeks 3, 5, 7, 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
Discussion section: Thursdays, 11:15 am–12:05 pm · Tisch Hall (40 W 4th St), room LC9
Zoom: Join meeting
Syllabus: PDF