Monday schedule

(The schedule for the Monday is easier then the rest of the week 😉)

Times are all UTC.

Getting Lean and VScode up and running.
Installation videos (prerecorded)
Volunteers available on Zulip + screensharing.
Git + github demo (prerecorded talk)
Make a PR to participants.md that adds your name (we can fix all the merge conflicts later)

Resources

Make sure that we have an up to date list of helpful resources.

What is a Type? What is a Prop? (15 minute talk)
- Top-down approach to type theory for mathematicians
What is a type? What is a set? What is a subtype?
- How to think about them, how to use them.
Set/finset/set.finite whut?
- What's the difference? How to use them?
- How to navigate between them.
Dealing with numbers
- nat subtraction/division
- int division
- norm_cast and friends
Defeq vs Provable eq
Totalizing functions "0¯¹ = 0, shock! horror!" (15 minute talk)
- Why do we totalize functions?
- Why is this not a problem?
What's with all those crazy brackets??
- Explain (), {}, [], {{}} for assumptions
- Explain <,> and \f<,\f> for use in terms
Library overview "Algebra" (?)
- Point out that we totalize inv
Library overview "Order" (?)
Library overview "Linear algebra" (?)
Library overview "Topology" (@Reid?)
Library overview "Category theory" (@Scott?)
Analysis "What is a filter?" (@Patrick?) (45 minute talk?)
- Why does mathlib use filters?
- How do you work with filters?
Library overview "Analysis" (?)
Library overview "Measure theory" (?)
Library overview "Geometry" (@Sébastien?)
- Manifolds in Lean.
Library overview "Number theory" (15 minute talk)
- We don't have that much. But the theorems have cool names attached!
Library overview "meta code" (@Rob? @Mario?)
How to write a baby tactic