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
¹
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

Theorem Proving in Lean, Ch. 2
²
lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html
🔗

🔗

🔗

March 19 🔗

Logic, Structured Proofs

Theorem Proving in Lean, Ch. 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
⁴
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
⁵
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
⁶
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
⁷
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
⁸
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

Theorem Proving in Lean, Ch. 7
⁹
lean-lang.org/theorem_proving_in_lean4/inductive_types.html
🔗

🔗
Mathematics in Lean, §5.2
¹⁰
leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html#induction-and-recursion
🔗

🔗

🔗

April 4 🔗

Lists

Theorem Proving in Lean, Ch. 7
¹¹
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
  ¹²
  lean-lang.org/theorem_proving_in_lean4/structures_and_records.html
  🔗
  
  🔗
- Hitchhiker’s Guide to Logical Verification, §5.5
  🔗
  
  🔗
🔗
🔗
Type Classes
- Theorem Proving in Lean, Ch. 10
  ¹³
  lean-lang.org/theorem_proving_in_lean4/type_classes.html
  🔗
  
  🔗
- Hitchhiker’s Guide to Logical Verification, §5.6
  🔗
  
  🔗
🔗
🔗

🔗

April 9 🔗

Sets

Mathematics in Lean, § 4.1
¹⁴
leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html#sets
🔗

🔗

🔗

April 11 🔗

Sets

Mathematics in Lean, § 4.1
¹⁵
leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html#sets
🔗

🔗

🔗

Subsection 1.6 April 14 – April 18

April 14 🔗

Set Functions

Mathematics in Lean, § 4.2
¹⁶
leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html#functions
🔗

🔗

🔗

🔗

April 16 🔗

Set Functions

Mathematics in Lean, § 4.2
¹⁷
leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html#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

¹⁸

external/pdf/algebraic_structures.pdf

🔗

April 23 🔗

Algebraic Structures in Lean I (Operations and Monoids)

Mathematics in Lean, § 6.2
¹⁹
leanprover-community.github.io/mathematics_in_lean/C06_Structures.html#algebraic-structures
🔗

🔗

🔗

Subsection 1.8 April 28– May 2

April 28 🔗

Class Cancelled (Jury Duty)

🔗

April 31 🔗

Algebraic Structures in Lean II (Groups)

Mathematics in Lean, § 6.2
²⁰
leanprover-community.github.io/mathematics_in_lean/C06_Structures.html#algebraic-structures
🔗

🔗

🔗

May 2 🔗

Final Project proposals

🔗

Subsection 1.9 May 5 – May 9

May 5 🔗

Algebraic Structures in Lean II (Rings and Fields)

Mathematics in Lean, § 6.2
²¹
leanprover-community.github.io/mathematics_in_lean/C06_Structures.html#algebraic-structures
🔗

🔗

🔗

May 7 🔗

Morphisms (Monoids and Groups)

Mathematics in Lean, § 8.1.1
²²
leanprover-community.github.io/mathematics_in_lean/C08_Groups_and_Rings.html#monoids-and-their-morphisms
Mathematics in Lean, § 8.1.2
²³
leanprover-community.github.io/mathematics_in_lean/C08_Groups_and_Rings.html#groups-and-their-morphisms
🔗

🔗

🔗

May 9 🔗

Morphisms (Rings)

Mathematics in Lean, § 8.2.1
²⁴
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.

🔗

Prev TopNext