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)	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.

 

 

 

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

 

 

 

Last modified: Tuesday, Nov 11 2025

This site is open source. Improve this page.