This post is a continuation of Preparing for Networked Mathematics.
During 2023 we had a few more talks on theorem provers and automated deduction. And on how the work in math provers can impact the world.
On the 27th April we heard Georges Gonthier on Foothills and cathedrals: organising the libraries behind big proofs
Foothills and cathedrals: organising the libraries behind big proofs
Not exactly like the picture below, but close:
On the 4th May we had Michael Barany on
How Categories Come to Matter: On the history and sociology of categories in modern mathematics
which wasn't so much about math provers, but about why category theory matters so much right now. And, as usual with Michael, how to study the `relationship between abstract knowledge and the modern world'.
On 18th May we had Clark Barrett on
and on the 31st August we had Nat Shankar on
Then we had Leonardo de Moura on the 7th September talking about
Lean 4: Empowering the Formal Mathematics Revolution and Beyond
Yes, we already had Jeremy Avigad, Kevin Buzzard and Johan Commelin talking about LEAN in 2022, but it was good to hear from the main creator of the Lean prover too!
(He even talked on the 7th September, a Brazilian National Holiday, and neither of us noticed it!)
Tom Leinster from Edinburgh University on
and then in November we had Minhyong Kim with a beautiful talk on
Of course these last three talks say more about how I feel about the role of mathematics in the world than about how we can use provers to do more mathematics. But I think this is essential too!
