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

Thursday

(support class)

  • Cancelled due to illness.
Week 3 (Oct 20-24)
Monday
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

Thursday

(support class)

Week 5 (Nov 03-07)
Monday
Tuesday

Thursday

(support class)

Week 6 (Nov 10-14)
Monday
Tuesday

Thursday

(support class)

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)

Week 8 (Nov 24-28)
Monday
Tuesday

Thursday

(support class)

  • Inaccessible room! Hopefully, this only affected this week.
Week 9 (Dec 01-05)
Monday
Tuesday

Thursday

(support class)

  • Group work.
Week 10 (Dec 08-12)
Monday
Tuesday

 

 

 

What we have done so far: current syllabus

 

 

 

Last modified: Tuesday, Oct 21 2025