Day Two of the Math Heaven!

Second Day

• So today there were quite a few talks on Machine Learning, including Marc’s talk on using ML to formulate conjectures, which had to do with knot theory (I don’t know a lot about this, except barely what a trefoil is, and I just learned a teeny bit about Seifert Surfaces today). Then Leo gave an incredibly inspiring talk on Lean; I attended a talk by him about two weeks ago online for a completely different community interestingly, but he is always so passionate and it’s crazy to see how much the community has grown. I loved that he made the point that when we say a proof is “trivial” or obvious, that can’t work in formal verification. He also spoke about issues of scalability.
• I loved the commutatitive diagram usability feature, and he mentioned some interesting papers like that on Hypertree proof search and some great tools like Lean Chat, Lean Aide and the paper on SAT Solvers for Boolean Pythagorean Triples and interestingly, the first author was sitting next to me.
• There was also a really cool talk on using reinforcement learning for finding counterexamples, where we formulate our conjecture as a game, specify a policy and reward, and examples of what worked and what did not. Haniel gave a talk on SMT proofs which felt a lot closer to something I might expect to hear at POPL or something, and even mentioned Z3, which I had heard about in 2018 from Nadia at UCSD, I think. Finally, Anne gave a talk in computation which was fascinating, because they spoke about what it means to do computation as a mathematician vs a computer scientist. An example is something like 1 + 1 = 2 where we would have to unroll or unwrap the computation to obtain an equivalent result. They spoke about definitional equality and the fragility of definitional equality and proof by reflection. I loved the final message, which was that “clinging to one notion of computation causes tonnes of frustration. We should bridge the gaps flexibly”.

Unexpectedly

• So I was walking home, thinking I would settle in early evening, and for some strange reason, I thought maybe I should see if the lunch cafeteria was still open (they have a Veggie Grill!). As it turns out, I didn’t end up going there, but I did run into my friend who is an Algebraic Topologist and does Homotopy Type Theory and is doing their postdoc there. And I met another Homotopy Type Theorist, and then another, and we ended up hanging out in their office and then going out to eat Indian food together. So now I know two more Algebraic Topologists apparently now. And I got to see what the postdoc life looks like at UCLA, which looks amazeballs. They have blackboards and their own office, with a view. And hilariously a conversation started about whether Analysis would exist without Zorn’s Lemma. It was just a lot of fun today!

Here are some photos

• With some Homotopy Type Theory friends: Morgan, Josh and Hood!

Oh, one more thing!

• I’m literally the reason that country is on there! How cool!

And that’s it