Syllabus

MA4N1 Theorem Proving with Lean tentative syllabus

Autumn 2024

	Week 1 (Sep 30-Oct 04)
Monday	Overview of assessment. Introduction to formalization and to Lean.
Tuesday	Syntax, infoview, tactics, structuring proofs (L00_intro.lean).
	Week 2 (Oct 07-11)
Monday	Begin polynomials.
Tuesday	Coordinate projects.
TBA (support class)	Solve polynomial questions. The <;> tactic combinator.
	Week 3 (Oct 14-18)
Monday	More on polynomials. Go over beginning of generalizations.
Tuesday	Assign (most) groups. Continue with generalizations.
TBA (support class)	Group questions.
	Week 4 (Oct 21-25)
Monday	Definitions in Mathlib.
Tuesday	Suggestions of topics. Definitions and inductives in Mathlib.
TBA (support class)	Two sets of exercises, covering graphs questions, and limits questions.
	Week 5 (Oct 28-Nov 01)
Monday	Typeclasses.
Tuesday	Calculations: calc, conv, gcongr.
TBA (support class)	ℝ[i] is a field.
	Week 6 (Nov 04-08)
Monday	Breather week. Using the fields of a structure. noncomputable. Decidable.
Tuesday	Breather week. More on Decidable. Discussion on sub-structures in Mathlib.
TBA (support class)	Induction on divisors of a natural number.
	Week 7 (Nov 11-15)
Monday	set_option autoImplicit false/true. aesop and rcases using the dvd_induction file.
Tuesday	Pathologies: Nat.sub, Nat.div, Div, deriv
TBA (support class)	deriv-pathologies.
	Week 8 (Nov 18-22)
Monday	Some syntax: variable/open ... in ..., explicit vs implicit arguments. Beginning of setoids.
Tuesday	Setoids.
TBA (support class)	Group work.
	Week 9 (Nov 25-29)
Monday	Navigating Mathlib.
Tuesday	Finiteness. Classical, noncomputable, Prop, Bool.
TBA (support class)	Group work.
	Week 10 (Dec 02-06)
Monday	Advent of Code. Solution to Day 2: syntax parsing and running the input.
Tuesday	Algebraic and tropical geometry in Mathlib. Type theory and category theory.
TBA (support class)	Group work? Week-end setoids?

 

 

 

What we have done so far: current syllabus

 

 

 

Last modified: Sunday, Sep 22 2024

This site is open source. Improve this page.