Syllabus

MA4N1 Theorem Proving with Lean tentative syllabus

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)	TBA
	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)	Finish limits questions, graphs questions.
	Week 7 (Nov 17-21)
Monday	Typeclasses and introduction to differences between def, structure and class.
Tuesday	Working with a structure and adding instances to it.
Thursday (support class)	Various possibilities: Induction on divisors of a natural number. Definitions and inductives in Mathlib, Calculations: calc, conv, gcongr. ℝ[i] is a field.
	Week 8 (Nov 24-28)
Monday	Finished Typeclasses.
Tuesday	Digression about PowerSeries and HasFPowerSeriesOnBall. Navigating Mathlib.
Thursday (support class)	Inaccessible room! Hopefully, this only affected this week.
	Week 9 (Dec 01-05)
Monday	Finiteness.
Tuesday	Pathologies, leading up to deriv-pathologies.
Thursday (support class)	Group work.
	Week 10 (Dec 08-12)
Monday	Advent of Code. Solution to Day 2, 2023: syntax parsing and running the input.
Tuesday	Quotients and setoids. Noncomputability and decidable instances.

 

 

 

What we have done so far: current syllabus

 

 

 

Last modified: Tuesday, Nov 11 2025

This site is open source. Improve this page.