Tuesday, February 27, 2024

Preparing for Network Mathematics 2023

 

 

(source: Twitter/X account Stonehenge UK)


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.

Not exactly like the picture below, but close:












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!) 

In 12th October we had Dominic Orchard talking on           Programming for the Planet























 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!





































Sunday, February 25, 2024

Formal Math: are we there yet?


 I have not touched my blog much this last year. A shame. I need to write more and I need to try to correct pictures and links that stopped working. Now the programme in Bonn, on Prospects of Formal Mathematics is coming closer, so writing should help me decide to organize my time in Germany. But first things first. I need to email a few more people about our arrangements.