Syllabus

MA4N1 Theorem Proving with Lean tentative syllabus

Autumn 2026

	Week 1 (Oct 05-09)
Monday	Overview of assessment. Introduction to formalization and to Lean. The Natural numbers.
Tuesday	Preliminary discussion about project topics.
	Week 2 (Oct 12-16)
Monday	Infoview. Basic tactics: exact?, constructor, cases. Type ascriptions, structuring proofs (L00_intro.lean)
Tuesday	Finish L00_intro.lean. Proof obligations, forward and backward reasoning.
Thursday (support class)	Overview of available resources. Installation troubleshooting.
	Week 3 (Oct 19-23)
Monday	Polynomials, constants, basic lemmas.
Tuesday	Finish polynomials. Groups of order 6 vs groups of order pq.
Thursday (support class)	Proofs with $\varepsilon$ and $\delta$. Archimedean property of the real numbers.
	Week 4 (Oct 26-30)
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 02-06)
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 09-13)
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 16-20)
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 23-27)
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 (Nov 30-Dec 04)
Monday	Using the variable command. Beginning with pathologies.
Tuesday	Difference between apply, refine, exact and specialize. Pathologies, leading up to deriv-pathologies.
Thursday (support class)	First meeting.
	Week 10 (Dec 07-11)
Monday	Calculations, in particular conv and calc.
Tuesday	Coercions, gcongr, general discussion on proof style and automation.
Thursday (support class)	Group work.

 

 

 

What we have done so far: current syllabus

 

 

 

Last modified: Tuesday, Oct 20 2026

This site is open source. Improve this page.