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	Difference between Bool and Prop, preliminary discussion about project topics.
	Week 2 (Oct 07-11)
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 14-18)
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 21-25)
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 (Oct 28-Nov 01)
Monday	Generalizations.
Tuesday	Group questions.
Tuesday (support class)	limits questions.
	Week 6 (Nov 04-08)
Monday	Breather week. Quick introduction to Filters, limits questions.
Tuesday	graphs questions.
Tuesday (support class)	Finish limits questions, graphs questions.
	Week 7 (Nov 11-15)
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. deriv-pathologies.
	Week 8 (Nov 18-22)
Monday	Finished Typeclasses.
Tuesday	Digression about PowerSeries and HasFPowerSeriesOnBall. Navigating Mathlib.
Tuesday (support class)	Inaccessible room! Hopefully, this only affected this week.
	Week 9 (Nov 25-29)
Monday	Navigating Mathlib.
Tuesday	Finiteness. Classical, noncomputable, Prop, Bool.
Tuesday (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.
Tuesday (support class)	Group work? Week-end setoids?

 

 

 

What we have done so far: current syllabus

 

 

 

Last modified: Thursday, Nov 21 2024

This site is open source. Improve this page.