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, preliminary discussion about project topics.
	Week 2 (Oct 13-17)
Monday	Syntax, infoview, rfl, inductives.
Tuesday	Tactics, structuring proofs (L00_intro.lean)
Tuesday (support class)	Functional programming, object oriented programming, more proofs.
	Week 3 (Oct 20-24)
Monday	Begin with polynomials.
Tuesday	Coordinate projects. Start assigning groups.
Tuesday (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.
Tuesday (support class)	Solve polynomial questions. The <;> tactic combinator.
	Week 5 (Nov 03-07)
Monday	Generalizations.
Tuesday	Group questions.
Tuesday (support class)	limits questions.
	Week 6 (Nov 10-14)
Monday	Breather week. Quick introduction to Filters, limits questions.
Tuesday	graphs questions.
Tuesday (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.
Tuesday (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.
Tuesday (support class)	Inaccessible room! Hopefully, this only affected this week.
	Week 9 (Dec 01-05)
Monday	Finiteness.
Tuesday	Pathologies, leading up to deriv-pathologies.
Tuesday (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: Friday, Sep 19 2025

This site is open source. Improve this page.