Skip to main content
Logo image

Course Schedule

Section 1 Schedule

Subsection 1.1 March 12 – March 14

March 12
Introduction and Setup
March 14
Terms and Types
  • Theorem Proving in Lean, Ch. 2
     1 
    lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html
  • Hitchhiker’s Guide to Logical Verification, §1.1, § 1.2

Subsection 1.2 March 17 – March 21

March 17
Definitions, Variables, Sections, Namespaces
March 19
Logic, Structured Proofs
  • Theorem Proving in Lean, Ch. 3
     3 
    lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html
  • Hitchhiker’s Guide to Logical Verification, §4.1, §4.2
March 21
Classical Logic
  • Theorem Proving in Lean, Ch. 3
     4 
    lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html
  • Hitchhiker’s Guide to Logical Verification, §4.1, §4.2

Subsection 1.3 March 24 – March 28

March 24
Universal Quantifiers
  • Theorem Proving in Lean, Ch. 4
     5 
    lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html
  • Hitchhiker’s Guide to Logical Verification, §4.3
March 26
Existential Quantifiers
  • Theorem Proving in Lean, Ch. 4
     6 
    lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html
  • Hitchhiker’s Guide to Logical Verification, §4.3
March 28
Tactics
  • Theorem Proving in Lean, Ch. 5
     7 
    lean-lang.org/theorem_proving_in_lean4/tactics.html
  • Hitchhiker’s Guide to Logical Verification, §3.1 – 3.8

Subsection 1.4 March 31 – April 4

March 31
Basic Inductive Types
  • Theorem Proving in Lean, Ch. 7
     8 
    lean-lang.org/theorem_proving_in_lean4/inductive_types.html
  • Hitchhiker’s Guide to Logical Verification, §5.1 – §5.4
April 2
Constructing the Natural Numbers
April 4
Lists
  • Theorem Proving in Lean, Ch. 7
     11 
    lean-lang.org/theorem_proving_in_lean4/inductive_types.html
  • Hitchhiker’s Guide to Logical Verification, §5.1 – §5.4

Subsection 1.5 April 7 – April 11

April 7
  • Structures
    • Theorem Proving in Lean, Ch. 9
       12 
      lean-lang.org/theorem_proving_in_lean4/structures_and_records.html
    • Hitchhiker’s Guide to Logical Verification, §5.5
  • Type Classes
April 9
Sets
April 11
Sets

Subsection 1.6 April 14 – April 18

April 14
Set Functions
April 16
Set Functions
April 18
No Classes (University Closed for Easter)

Subsection 1.7 April 21 – April 25

April 21
No Classes (University Closed for Easter)
April 23
Algebraic Structures
 18 
external/pdf/algebraic_structures.pdf
April 23
Algebraic Structures in Lean I (Operations and Monoids)

Subsection 1.8 April 28– May 2

April 28
Class Cancelled (Jury Duty)
April 31
Algebraic Structures in Lean II (Groups)
May 2
Final Project proposals

Subsection 1.9 May 5 – May 9

May 5
Algebraic Structures in Lean II (Rings and Fields)
May 7
Morphisms
May 9
Subobjects

Subsection 1.10 May 12– May 16

  • 12 Logical Foundations of Mathematics
    • 12.1 Universes
    • 12.2 The Peculiarities of Prop
    • 12.3 The Axiom of Choice

Subsection 1.11 May 19– May 23

  • 12 Logical Foundations of Mathematics
    • 12.4 Subtypes
    • 12.5 Quotient Types

Warning 1.1.

The instructor reserves the right to modify the schedule as needed.
PrevTopNext