Sunday, September 22, 2024

Hausdorff Institute of Mathematics: the beginning of our trimester

 


Summer 2024 was the summer of the Hausdorff Institute of Mathematics programme on formalized mathematics. The programme was a whole trimester 6th May til 9th August, but I was a bit late as Eric graduated from Law School in St Louis, MO and I didn't know when that was going to happen exactly. So I could only promised to leave the US in June and I arrived in Bonn as soon as I could, on the 2nd June.

I hope to produce several blog posts about the programme, but indeed I am starting late. The arrival in Bonn was not without problems. Thank goodness Davide Trotta was already there and he able to get my keys for me and be up until midnight or so, when I finally managed to arrive. By contrast, arriving at the Institute was easy and it's a very pleasant place.


My office was very much the first thing you see when entering the the building. I've posted the picture before, but here it goes again. It's nice to have an office of your own, with your name on the door. Very rare in industry these days: it's all open plan settings, so I've enjoyed it.

Shame the huge electronic "whiteboard" didn't work very well with Macs, and I didn't feel like harassing IT to get to work for me. I was very surprised that macs weren't considered the default option, but there you go.  Also shame I forgot to take pictures of the flat (that was nice and modern) and of the next door building (some sort of offices for the University of Bonn) that I mistook for my accommodation when I arrived. I'm glad I didn't persevere in trying to call the porter/superintendent as there wasn't one and I was on the wrong building, number 57 instead of the intended 59. I blame Grothendieck and the lateness of the hour. But of course the keys didn't work in the wrong building, but when I realized my mistake all was fine.

Sunday, September 15, 2024

Topos-Chapman Collaboration

In May 2024  Topos Institute and the University of Chapman came together to launch an official partnership. Our main aim is to explore joint research projects and expand our role mentoring and teaching the next generation of technologists working in the public interest, as Brendan Fong wrote in the Topos blog post. The official announcement from Chapman can be found in the Doctor of Science in Mathematics, Physics and Philosophy (MPP) program  and here.

We celebrated our partnership with a workshop where talks were given both by Topos and Chapman scientists. The schedule is attached, and the recordings are available in YouTube in this playlist. This collaboration came about, after several months of articulation, after I gave a talk in Chapman's OCIE seminar in April 2023 on Dialectica constructions.



Wednesday, April 10, 2024

Pasadena Last December

 


 

 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.

Sunday, March 3, 2024

Dagstuhl in the Fall (2023)

 

In the spring of 2022 I got sick, not as sick as I thought then, but sick enough to end up in the emergency room of the hospital in Stanford twice in the same week in May. So the whole year of 2022 got pear-shaped and many of my plans had be cancelled. I had a small procedure at the end of the year--on the day before Thanksgiving exactly-- and this made the year of 2023 a year of recovery.

The year of recovery meant I was going to try to do  three trips (since I had to cancel many in 2022): one simply to Chapman, South California, one to Bloomington, Indiana and one to  Pisa and Padova, in Italy.  All of them went well, mostly: I got covid when returning from Indiana. So I  decided to do another three trips: to St. Louis, Missouri, to Dagstuhl, Germany and to Pasadena, CA.

The one I was most worried about was the one to Dagstuhl, as I do not speak German and Dagstuhl can be fairly inaccessible. But I partnered with Jacques Carrette and Stefania Dumbrova and all went well getting there and getting back home. And being at Dagstuhl is always a pleasure! I have met several people who, like me, are concerned about using digital tools to make mathematics more accessible.

The schedule of the talks and discussions is in https://www.dagstuhl.de/23401/schedule.pdf. I really need to read a bit more about some of the work that I did not manage to grasp while there.

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.



Sunday, December 31, 2023

Ada Lovelace Day in December?

 

 

My Ada Lovelace heroine of 2023 is
Andrée C. Ehresmann from the
Université de Picardie Jules Verne 

(Photo by Rabatakeu CC BY-SA 3.0, Wikimedia)

"Better late, than never," I say. Yes, Ada Lovelace Day (ALD) is in October, and it varies a little each year, a convenient leeway, for chronically late people, like myself. This year I have less of an excuse, as I had decided to honour Andrée in July already. But the year was hectic, in a good way, so I didn't get around to posting my ALD "hommage" so far. But today is the last day of the year, so here it goes, before the clock chimes, and we change back into pumpkins.

Andrée has been a role model for me in many ways. She's been a mathematician for longer than I have been alive, and I am very old indeed. She has this awesome description of her research work in her webpage. I share with her a diversified academic career (I will try to imitate the lovely graph below) and a love for category theory and its explanatory power.


I have meant to write about Andrée before. In 10/27/2016 I posted a message of Marta Bunge's in the blog "Women in Logic". Like today's post, that one was hastily written, rushing to some function or something else. But at least it was written and records my indebtedness to Marta and her friendship to me and to Andrée. So I could write lots about Andrée's work, but you can look at her pages, the "Cahiers" work for more than 40 years, and the lovely diagram above. So I'd rather leave you with Marta's words in 2016 and a picture of Marta, since I have not mourned her absence enough. The volume celebrating her work is now almost totally ready, so I will be writing more about Marta soon. She wrote:

"There is recently an article in the journal Nature about the presence of women in science and on how to improve what seems to be an unfair situation, which I believe. I hope that someone more qualified than I can do this since I believe it is important for our field. Without a shadow of a doubt I consider Andree C. Ehresmann as someone who has done a lot for our field - not just by continuing the work of Charles Ehresmann by publishing his Oeuvres Completes and continuing with the journal Cahiers de Topologie et Geometrie Differentielle (Categoriques), but by encouraging many researchers in our field - both men and women. She certainly deserves mention as a woman and a mathematician. I leave you with that. All the best."


Happy New Year!