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)	Implicit vs explicit variables. Dependent Cartesian Product < , >. Addition of two even numbers is even. Negation. Contradiction (absurd).
	Week 4 (Oct 27-31)
Monday	Discussion about structure, class Working with two topologies on the same set/type.
Tuesday	Generalizations.
Thursday (support class)	Solve polynomial questions. The <;> tactic combinator.
	Week 5 (Nov 03-07)
Monday	Generalizations.
Tuesday	Group questions.
Thursday (support class)	limits questions.
	Week 6 (Nov 10-14)
Monday	Breather week. Quick introduction to Filters, limits questions.
Tuesday	graphs questions.
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, Oct 21 2025

This site is open source. Improve this page.