Lean for the Curious Mathematician

Mathematics

Audience:	Researchers in the topic
Conference dates:	13-Jul-2020 to 17-Jul-2020
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
Fri	Jul 17	13:30	Sébastien Gouëzel and Heather Macbeth	“Differential geometry”
Fri	Jul 17	11:00	Yury Kudryashov	“Calculus and integration”
Fri	Jul 17	08:00	Patrick Massot	“Topology”, including filters
Thu	Jul 16	13:00	Scott Morrison	“Category theory”
Thu	Jul 16	11:00	Anne Baanen	"Linear algebra"
Thu	Jul 16	09:00	Johan Commelin	“Groups, rings and fields”
Thu	Jul 16	08:00	Kevin Buzzard	“Order”, including Galois connections
Wed	Jul 15	13:00	Alex J. Best	Rebuilding a topological hierarchy
Wed	Jul 15	11:00	Kevin Buzzard	Rebuilding an algebraic hierarchy
Wed	Jul 15	08:00	Floris van Doorn	Structures and classes
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)

Embed this schedule

Export series to