A few thoughts from talking to some of my favorite mathematicians (both for their work and, like, as people and friends) at the expMath meeting:

1. There is a big culture clash between math and AI, and it is really urgent that AI folks respect the mathematical culture if they want fruitful collaborations with math folks. (I remember this time in PL very well, in 2021-2022)

2. Never occurred to me that an emerging use case for proof repair is porting definitions, theorems, and proofs between ones mathematicians actually want to use and the ones autoformalization is good at (typically the mathlib ones)

3. What a time to be alive!

4. Lean's hegemony makes sense given community effects and need for a critical mass, but it's also worrying, and has implications for what kinds of math are represented. We need more work for other proof assistants

5. We have FROs, institutes, big commercial labs, startups, government labs, nonprofits, government funders, and academics who all care about this a lot. How can we work smoothly together? This is a hard problem without a single answer

6. Mathematicians want to create benchmarks by and for mathematicians, but they are also learning that doing this is a hard skill that needs to be developed

7. There is widespread agreement that collecting more of the data on thought processes and mistakes along the way to writing a proof is necessary. (This is an interest of mine dating back to the REPLICA paper in 2019)

Probably more can go here but I need to collect more thoughts first

Today, thanks to a former PhD student, I learned that LLMs are terrible at generating Whitespace code: https://arxiv.org/pdf/2603.09678

Also today, I was invited (and I am accepting) to join a group on redesigning our undergraduate curriculum, which includes discussions on our choice of first programming language.

I am not saying that these things are related. I just happen to be mentioning them both at once because I saw them both today. You get a lot of characters in one toot after all.

What?

New draft of Principles of Dependent Type Theory with @danielgratzer:
https://www.carloangiuli.com/papers/type-theory-book.pdf

This is a minor release with a lot of small improvements and typo fixes, and a sneak preview of a forthcoming appendix 🤫