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

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.

 

 

 

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

 

 

 

Last modified: Tuesday, Oct 21 2025