ABCDEFGHIJKLMNOPQRSTUVWX
1
DateTimeTopicLink to recordingRecommended ResourcesComments
2
July 9, 20241-3 pm ETIntroduction to Lean and proofs
https://umbc.webex.com/umbc/ldr.php?RCID=e91c7b67a5dbc8aab81c9175669068b2
MoP Ch. 1.1-1.2Welcome!
3
July 10, 20241-3 pm ETEqualities and inequalities
https://umbc.webex.com/umbc/ldr.php?RCID=484469c27cc717724335ffc8c542549d
MoP Ch. 1.2-1.5
4
July 16, 20241-3 pm ETProofs with structure
https://umbc.webex.com/umbc/ldr.php?RCID=6be1e5636d1d1e42952bf1b073c53be0
MoP Ch. 2, MIL Ch 1-2
5
July 17, 20241-3 pm ETProofs with structure II
https://umbc.webex.com/umbc/ldr.php?RCID=94c58c20d9de582087a0ae839c8f2903
MoP Ch. 4, MIL Ch 3
6
July 23, 20241-3 pm ETProofs about functions; types
https://umbc.webex.com/umbc/ldr.php?RCID=ebffa8e475a29d30868ba78c0ff4e477
MoP Ch. 8, MIL Ch 4.2, TPIL Ch. 2
7
July 24, 20241-3 pm ETCalculus-based-proofs
https://umbc.webex.com/umbc/ldr.php?RCID=589e20326023c8f254f781cb9d961194
MIL Ch. 10, MIL Ch. 9 to learn about limits
8
July 30, 2024Prof. Josephson traveling
9
July 31, 2024Prof. Josephson traveling
10
August 6, 20241-3 pm ETFunctions, recursion, structures
https://umbc.webex.com/umbc/ldr.php?RCID=303f1f86ec0bdc0cdfa675683bb5a6ca
FPIL 1.1 - 1.4
11
August 7, 20242-4 pm ETPolymorphic functions for floats and reals; lists
https://umbc.webex.com/umbc/ldr.php?RCID=256a905852ce8c9b2552ed7697fc4b3f
FPIL 1.3 - 1.5Moved an hour later for REU celebration
12
August 13, 20241-3 pm ETLists, indexing, input / output, compiling Lean to C
https://umbc.webex.com/umbc/ldr.php?RCID=ffa9f673da7d5f51c0845178bb502220
FPIL Ch 2, 3, 4, 5, 10CSV parser
13
August 14, 20241-3 pm ETNo class!
14
August 20, 20241-3 pm ETLeanMD & BET Analysis in Lean
https://umbc.webex.com/umbc/ldr.php?RCID=fe9a35f2373d174b78c08a44745abde2
Special thanks to David Ugwuanyi, John Velkey, Colin Jones
15
August 21, 20241-3 pm ETSciLean
https://umbc.webex.com/umbc/ldr.php?RCID=fdb070fac47f174fcecf60a96960eacc
SCiLGuest instructor Tomas Skrivan!
16
17
Logic and proofs for scientists and engineersMoP: Mechanics of Proofhttps://hrmacbeth.github.io/math2001/
18
Functional programming in Lean 4MIL: Mathematics in Lean
https://leanprover-community.github.io/mathematics_in_lean/
19
Provably-correct programs for scientific computingFPIL: Functional Programming in Lean
https://lean-lang.org/functional_programming_in_lean/
20
SCIL: Scientific Computing in Lean
https://lecopivo.github.io/scientific-computing-lean/
21
TPIL: Theorem Proving in Lean
https://leanprover.github.io/theorem_proving_in_lean4/introduction.html
22
23
Register here!
https://docs.google.com/forms/d/1yC-Ct2Iun_E2ztSaUPxfyJNvJRNR0hkiFJW1R2m3qR0/edit
24
Link to join online will appear after registration.
Additional topics
25
Join the chat forum on Zulip!
https://leanprover.zulipchat.com/#narrow/stream/445230-Lean-for-Scientists-and-Engineers-2024
Syntax vs. semantics
26
Formalization philosophy: bottom-up (i.e. Hilbert's 6th) vs. start in the middle
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100