* Dates within the next 7 days are marked by a star.
Yaël Dillies
Formalisation in Lean: Why care?
* Monday 29 July 2024, 11:00, M3 (M234)
What's this craze about theorem proving? You must have heard of it, but do you know what it is actually about? Do we really care about absolute correctness? or is this some kind of gimmick to make the cover of popular science magazines?
In this talk, I will explain the basic principles of Lean and argue that the true reason behind the launch of formal mathematics as an established subject is neither a matter of informality crisis on the part of mathematicians nor a publicity stunt, but the manifestation of a much more fundamental background shift in the social practice of mathematics, and that now is the time to join the formalisation bandwagon.
I will illustrate my point with my personal journey through formal mathematics, from bored undergrad to collaborator of Terence Tao, sprinkled with examples from my own subject: additive combinatorics.
No Lean experience nor knowledge of additive combinatorics will be assumed.
Yaël Dillies
Lean: The basics (formalization workshop 1)
* Tuesday 30 July 2024, 14:00, M3 (M234)
In this first workshop, I will explain the fundamentals of using Lean: Basic syntax, how to install it, where to find learning material, how to read the documentation, differences to other programming languages...
I will also have additional exercises for more advanced learners.
ForAlli Lean tutorials
Yaël Dillies
Lean: The slightly less basic (formalization workshop 2)
* Thursday 01 August 2024, 14:00, M3 (M234)
In this second workshop, we will build on what we will have done on Tuesday (and on the homework you will hopefully have completed) to move to more advanced notions like the use of filters in topology.
Motivated learners will be able to join the ForAlli meeting happening right after.
ForAlli Lean tutorials
Show the events of the past year
Page content by: webmaster-math [at] list [dot] aalto [dot] fi