In December 2023 I went to the the Workshop on
Open-source cyberinfrastructure supporting mathematics research
organized by Robert Beezer,
Steven Clontz,
and David Lowry-Duda at the American Instittue of Mathematics (AIM), CalTech, Pasadena. There was a report on the workshop activities and some Workshop videos were recorded.
For me it was very good to meet a whole community that I wasn't aware of. This community is committed to thinking about the accesssibility of learning mathematics, and everyone is trying to think about how to use digital tools for that. But of course the experiences, the tools and the approaches are all very different.
There are people interested in computer algebra systems and in theorem provers, just like in the Dagstuhl Seminar 23401 "Automated mathematics: integrating proofs, algorithms and data" that I went to in October 2023. But there were also people interested in visualizations, in publishing textbooks and on all sorts of teaching systems. The emphasis was definitely on the teaching aspects, more than on the research side that I tend to concentrate on.
However, there was a momentous little story that I should write down now, or I will forget it. Kim Morrison was giving a tutorial on Lean for Mathematics on Tuesday morning at 9 am. When they went to explain Lean's blueprint and show an example of its action, Kim stopped and said: oh well, when I was writing my slides last night after dinner, this (the "blueprint" for the proof of the theorem Gowers, Tao, Green and Manners had proved recently) was still blue. But now there's nothing to show, it's green!
The theorem had been proved by someone in Lean while we were sleeping! It felt somewhat magical, the dawn of a different kind of mathematics. It was a bit like when, on a tip of a number theorist friend in Cambridge, I went to hear Wyles talk about the proof of Fermat's last theorem. His formal announcement in the Isaac Newton Institute, that many years ago. I didn't understand anything of Wyles proof and I still hardly understand what a Lean blueprint is, but the magical side of maths just happens!
If you want to understand the history behind the theorem the Quanta magazine article ‘A-Team’ of Math Proves a Critical Link Between Addition and Sets by Leila Sloman explains it very well!
I confess that instead of enjoying the magic, I went directly to the Lean Zulip to check that there were no reports of vandalism or hacking on mathlib, no triggering of the green, by mistake. Only when everything seemed normal over there, I managed to enjoy the moment! Proofs more than 20 years in the making are like fine wine.
