BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Scott Morrison (Australian National University)
DTSTART:20200713T110000Z
DTEND:20200713T113000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/1
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 1/">Welcome + 1st Lean proof</a>\nby Scott Morrison (Australian National U
 niversity) as part of Lean for the Curious Mathematician\n\nAbstract: TBA\
 n
LOCATION:https://researchseminars.org/talk/LeanCurious/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lean community
DTSTART:20200713T050000Z
DTEND:20200713T100000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/2
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 2/">Tech support (installing Lean\, using git + GitHub)</a>\nby Lean commu
 nity as part of Lean for the Curious Mathematician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kevin Buzzard (Imperial College London)
DTSTART:20200713T113000Z
DTEND:20200713T160000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/3
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 3/">Natural number game (demo and exercises)</a>\nby Kevin Buzzard (Imperi
 al College London) as part of Lean for the Curious Mathematician\n\nAbstra
 ct: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robert Y. Lewis (Vrije Universiteit Amsterdam)
DTSTART:20200713T113000Z
DTEND:20200713T160000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/4
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 4/">Meta-programming and tactic writing</a>\nby Robert Y. Lewis (Vrije Uni
 versiteit Amsterdam) as part of Lean for the Curious Mathematician\n\nAbst
 ract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Patrick Massot (Université Paris-Sud)
DTSTART:20200714T080000Z
DTEND:20200714T100000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/5
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 5/">Mathematics in Lean: basics</a>\nby Patrick Massot (Université Paris-
 Sud) as part of Lean for the Curious Mathematician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jeremy Avigad (Carnegie Mellon University)
DTSTART:20200714T110000Z
DTEND:20200714T130000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/6
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 6/">Mathematics in Lean: logic</a>\nby Jeremy Avigad (Carnegie Mellon Univ
 ersity) as part of Lean for the Curious Mathematician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robert Y. Lewis (Vrije Universiteit Amsterdam)
DTSTART:20200714T130000Z
DTEND:20200714T143000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/7
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 7/">Dealing with numbers: ℕ\, ℤ\, ℚ\, ℝ\, ℂ</a>\nby Robert Y. Le
 wis (Vrije Universiteit Amsterdam) as part of Lean for the Curious Mathema
 tician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jeremy Avigad (Carnegie Mellon University)
DTSTART:20200714T143000Z
DTEND:20200714T160000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/8
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 8/">Dealing with sets and operations on them</a>\nby Jeremy Avigad (Carneg
 ie Mellon University) as part of Lean for the Curious Mathematician\n\nAbs
 tract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Floris van Doorn (University of Pittsburgh)
DTSTART:20200715T080000Z
DTEND:20200715T100000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/9
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 9/">Structures and classes</a>\nby Floris van Doorn (University of Pittsbu
 rgh) as part of Lean for the Curious Mathematician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kevin Buzzard (Imperial College London)
DTSTART:20200715T110000Z
DTEND:20200715T130000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/10
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 10/">Rebuilding an algebraic hierarchy</a>\nby Kevin Buzzard (Imperial Col
 lege London) as part of Lean for the Curious Mathematician\n\nAbstract: TB
 A\n
LOCATION:https://researchseminars.org/talk/LeanCurious/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex J. Best (University of Boston)
DTSTART:20200715T130000Z
DTEND:20200715T150000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/11
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 11/">Rebuilding a topological hierarchy</a>\nby Alex J. Best (University o
 f Boston) as part of Lean for the Curious Mathematician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kevin Buzzard (Imperial College London)
DTSTART:20200716T080000Z
DTEND:20200716T090000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/12
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 12/">“Order”\, including Galois connections</a>\nby Kevin Buzzard (Imp
 erial College London) as part of Lean for the Curious Mathematician\n\nAbs
 tract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Johan Commelin (Albert-Ludwigs-Universität Freiburg)
DTSTART:20200716T090000Z
DTEND:20200716T100000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/13
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 13/">“Groups\, rings and fields”</a>\nby Johan Commelin (Albert-Ludwig
 s-Universität Freiburg) as part of Lean for the Curious Mathematician\n\n
 Abstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/13/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Anne Baanen (Vrije Universiteit Amsterdam)
DTSTART:20200716T110000Z
DTEND:20200716T130000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/14
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 14/">"Linear algebra"</a>\nby Anne Baanen (Vrije Universiteit Amsterdam) a
 s part of Lean for the Curious Mathematician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Scott Morrison (Australian National University)
DTSTART:20200716T130000Z
DTEND:20200716T160000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/15
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 15/">“Category theory”</a>\nby Scott Morrison (Australian National Uni
 versity) as part of Lean for the Curious Mathematician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Patrick Massot (Université Paris-Sud)
DTSTART:20200717T080000Z
DTEND:20200717T100000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/16
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 16/">“Topology”\, including filters</a>\nby Patrick Massot (Universit
 é Paris-Sud) as part of Lean for the Curious Mathematician\n\nAbstract: T
 BA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Yury Kudryashov (University of Toronto)
DTSTART:20200717T110000Z
DTEND:20200717T133000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/18
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 18/">“Calculus and integration”</a>\nby Yury Kudryashov (University of
  Toronto) as part of Lean for the Curious Mathematician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sébastien Gouëzel (University of Nantes) and Heather Macbeth (Fo
 rdham University)
DTSTART:20200717T133000Z
DTEND:20200717T160000Z
DTSTAMP:20260503T024633Z
UID:LeanCurious/19
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanCurious/
 19/">“Differential geometry”</a>\nby Sébastien Gouëzel (University o
 f Nantes) and Heather Macbeth (Fordham University) as part of Lean for the
  Curious Mathematician\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanCurious/19/
END:VEVENT
END:VCALENDAR