Math Heaven Day Three

So this is late

• I am writing a late post because I got to bed around midnight and then got up at 3am. After the workshop, I ended up visiting a lifelong friend of mine, who I met when I moved out to Los Angeles years ago, and we went out for tacos! Anyways, this post is not about that :)
• On Day Three, we continued with several talks, including one by Micaela on Coq and defining real numbers in theorem provers. Some possibilities for this she mentioned were by using axiomatisation, Cauchy, Cantor, Dedekind cuts, 1st order / 2nd order or classical intuitionistic logic. She also demonstrated how several theorem provers dealt with this issue. She mentioned Coquelicot, which depends on total functions in place to dependent types for limits, derivates, etc…
• I loved Assia’s talk, which was on verifying computational mathematics, which in essence was distinguishing how computation is very different in that we may not obtain what we expect. She gave some fantastic examples, drawing from the Ternary Goldbach Conjecture, the paper by Kauers and Koutschan called Guessing with Little Data to show that cross-verification is not enough. She gave an example of a paper where the proof was wrong, but where it could be repaired. One of the examples that absolutely blew my mind was verification of plots. Having published a few ML papers, it’s something that I have come across but admit I haven’t thought deeply about, but it’s absolutely true; plots have issues, and in particular, as she calls it, “faithful plotting is hard”. An example is when the sampling is wrong, so that the plot is not correct. She showed several examples. She mentioned this paper by Melquiond.
• That was followed by an exceptional talk by Patrick, in which he showed readable proofs, making the distinction between formal verification, where the proof does not have to be readable, and the way we communicate ideas in Mathematics via readable proofs. He then gave a demo of a prototype using Lean in which a proof is generated using a variable degree of specificity. It was really exciting. I think that this is a great example of a tool that is made with the Mathematics community, and just for it, without their input. I really liked that he said that we should let the reader choose the degree to which they want to understand the proof. In his view, he said, “trying to make proof scripts readable is hopeless and counter-productive in general”.
• In the afternoon, we took a group photo, and I had lunch with a mathematician friend who works in software and programming language design. We then were able to see a talk by Tony on using large language models for auto-formalization, which is work being done by the N2Formal team. What was interesting was how formalization was done, particularly the Draft Sketch Prove paper. Finally, there was a panel with Emily, Sophie and Akshay, moderated by Jordan, who I just realized is the same professor who broke down the Mathematics scenes in movies (okay, that is random that I had that bookmarked).
• Finally, we had introductions, and I did mine. I was very nervous, but it went incredibly well, and we all felt supported. What was even better was that afterwards, I was encouraged to apply for another opportunity, in support of my research! I messaged my Maths advisor and at first thought her brief silence might have been disapproving (what is my dear student up to now lol), but she responded with a “YES” in all caps, when I asked if she would help and support me in doing this. By the end of the day, I was incredibly happy.
• Finally, I wrapped the day off chatting with a new friend, an undergrad who was about to embark on his PhD career. I had nostalgia instantly about one of my last interactions in San Francicso, where a friend who completed their PhD had reached out to me, and we had randomly met on the way out of a 400-person Twilio tech conference featuring a Mackelmore concert (yes, very strange, but very Bay-area tech-scene and yes, there was a point in which he body-surfed over the crowd apparently, and I was the only one who seemed to not know any lyrics to these songs). His last words to me were that he knew that some of these systems weren’t made for people like us, but that he was rooting for me. And I was immediately propelled back to staring at this excited soon-to-be PhD student in front of me, feeling the same for him, and wishing the same for his journey. It was an incredible day.
• Oh, and then I went out for tacos and met my long-time friend’s pets again, after four years of not seeing them, and they recognized me and I was bombarded!

Here are some photos

• My friend’s cat has a new shelf!

• We went to Newhall, which is in Santa Clarita, to get tacos! No Magic Mountain today though (yet haha).

• Oh yeah! I’ve missed you my “avocado-on-everything” State :)

• Lunch with my other Mathematician friend who writes software and designs functional languages with strong types!

• A snapshot of the demo by Patrick. I highly recommend watching his talk. Also, thanks to Kevin for the link! :)

• A snapshot from Assia’s talk on “Verifying Computational Mathematics”, where she shows how issues in sampling can result in incorrect plots, or where the periodicity is wrong.

And that’s it