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 (Monoids and Groups)
May 9
Morphisms (Rings)
  • Mathematics in Lean, § 8.2.1
     24 
    leanprover-community.github.io/mathematics_in_lean/C08_Groups_and_Rings.html#rings-their-units-morphisms-and-subrings

Subsection 1.10 May 12– May 16

May 12
Final Project Working Session
May 14
Final Project Working Session
May 16
Final Project Working Session

Subsection 1.11 May 19

May 19
Final Project Presentation

Warning 1.1.

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