# Lean for the Curious Mathematician

Mathematics

Audience: | Researchers in the topic |

Conference dates: | Mon Jul 13 to Fri Jul 17 |

Organizers: | Johan Commelin*, Patrick Massot |

*contact for this listing |

Lean is a proof assistant. This means that you can use it to explain mathematics to a computer, and the computer will check everything makes sense. This workshop is intended for mathematicians who use Lean or wish to learn Lean. We will have introductory tutorials, presentations, and break-out sessions for specific areas of interest as directed by the attendees. Experienced users will be available to answer questions, supervise exercises sessions, and participate in pair programming.

There is no initial knowledge needed; everyone is welcome. Intermediate users will be able to start pair programming immediately while beginners will first learn the basics, including installing the software and its supporting tools.

Upcoming talks

Past talks

Your time | Speaker | Title | |||
---|---|---|---|---|---|

Wed | Jul 15 | 08:00 | Floris van Doorn | Structures and classes | |

Wed | Jul 15 | 11:00 | Kevin Buzzard | Rebuilding an algebraic hierarchy | |

Wed | Jul 15 | 13:00 | Alex J. Best | Rebuilding a topological hierarchy | |

Thu | Jul 16 | 08:00 | Kevin Buzzard | “Order”, including Galois connections | |

Thu | Jul 16 | 09:00 | Johan Commelin | “Groups, rings and fields” | |

Thu | Jul 16 | 11:00 | Anne Baanen | "Linear algebra" | |

Thu | Jul 16 | 13:00 | Scott Morrison | “Category theory” | |

Fri | Jul 17 | 08:00 | Patrick Massot | “Topology”, including filters | |

Fri | Jul 17 | 09:00 | Yury Kudryashov | “Calculus” | |

Fri | Jul 17 | 11:00 | Yury Kudryashov | “Measure theory and integration” | |

Fri | Jul 17 | 13:00 | Sébastien Gouëzel and Heather Macbeth | “Differential geometry” |

Your time | Speaker | Title | |||
---|---|---|---|---|---|

Tue | Jul 14 | 14:30 | Jeremy Avigad | Dealing with sets and operations on them | |

Tue | Jul 14 | 13:00 | Robert Y. Lewis | Dealing with numbers: ℕ, ℤ, ℚ, ℝ, ℂ | |

Tue | Jul 14 | 11:00 | Jeremy Avigad | Mathematics in Lean: logic | |

Tue | Jul 14 | 08:00 | Patrick Massot | Mathematics in Lean: basics | |

Mon | Jul 13 | 11:30 | Kevin Buzzard | Natural number game (demo and exercises) | |

Mon | Jul 13 | 11:30 | Robert Y. Lewis | Meta-programming and tactic writing | |

Mon | Jul 13 | 11:00 | Scott Morrison | Welcome + 1st Lean proof | |

Mon | Jul 13 | 05:00 | Lean community | Tech support (installing Lean, using git + GitHub) |

Export series to