Syllabus

MA4N1 Theorem Proving with Lean

Autumn 2025

	Week 1 (Oct 06-10)
Monday	Overview of assessment. Introduction to formalization and to Lean.
Tuesday	Difference between Bool and Prop, basic tactics: exact?, apply, constructor, cases. Tactics, structuring proofs (L00_intro.lean)
	Week 2 (Oct 13-17)
Monday	Infoview, preliminary discussion about project topics. Begin with polynomials, cases, type ascriptions.
Tuesday	More polynomials.
Thursday (support class)	Cancelled due to illness.
	Week 3 (Oct 20-24)
Monday	Coordinate projects. Continue polynomials.
Tuesday	How to find the multiplication instance on Polynomials. Coordinate projects. Start forming groups. Begin generalizations.
Thursday (support class)	Proofs with $\varepsilon$ and $\delta$. Archimedean property of the real numbers.
	Week 4 (Oct 27-31)
Monday	Creating a new project (and failing on Windows). Comments about the project outline. Continuing generalizations: tactic mode and term mode.
Tuesday	Generalizations. Differences between simp? and exact?. Comparison between convert and exact/apply.
Thursday (support class)	Individual work on Natural Numbers Game. Individual work on Glimpse of Lean.
	Week 5 (Nov 03-07)
Monday	Generalizations.
Tuesday	Generalizations and "exotic" typeclasses. More on groups formation.
Thursday (support class)	Finding results in Mathlib. Breaking up proofs with have.
	Week 6 (Nov 10-14)
Monday	Breather week. Sample formalisation of an inequality: avoid Nat-subtraction, absorb inequalities, write more lemmas. Informal introduction to aesop and grind. Tactic cheat sheet.
Tuesday	Continue with the inequality. Discuss how to formalise the notion of subnormal subgroups.
Thursday (support class)	Installation issues: git and github. Independent work.
	Week 7 (Nov 17-21)
Monday	Sets vs Types: differences with set theory. Set.univ vs the type itself.
Tuesday	Navigating Mathlib.
Thursday (support class)	More on Sets vs Types. Coercions. Group work.
	Week 8 (Nov 24-28)
Monday	Integer polynomials in an extension of the breather week file. Mentioned ext for polynomials and simp [field] as a simp-based version of field.
Tuesday	Covered definitions, structure and inductives. Digression about presentations of groups by generators and relations and universal properties in category theory.
Thursday (support class)	More on induction. Equivalences in Mathlib.
	Week 9 (Dec 01-05)
Monday	Using the variable command. Beginning with pathologies.
Tuesday	Difference between apply, refine, exact and specialize. Pathologies, leading up to deriv-pathologies.

 

 

 

What we may be doing in the coming lectures: tentative syllabus

 

 

 

Last modified: Tuesday, Dec 02 2025

This site is open source. Improve this page.