Talia Ringer

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

If people are wondering what class prep looks like on my end for Build Your Own Proof Assistant, it's mostly organizing GitHub issues based on progress for the last sprint, and then writing specific goals for teams for the upcoming sprint that align with those issues and have concrete outcomes. So, basically, software engineering management.

My niece, who is 10 years old, is two years ahead in math (this does not surprise me, because I watched her put together puzzles stating at 6 months). I'm visiting her now. In their math class, apparently they meet to discuss famous mathematicians once in a while. "That's so cool, I just came from a big meeting with a bunch of mathematicians!"

I asked her if she remembered any they had spoken about and she couldn't remember lol

Should I feel complimented or annoyed that proof repair (which I introduced in my Ph.D. thesis work) has become so commonplace that people don't even bother citing my work anymore when they do proof repair work?

Found a bug in our synthetic layer of axioms, then asked Gemini 3 Pro to see if it could find any bugs in our axioms just by comparing our `env.txt` file with the source PDF we are formalizing. It did, without being pushed towards the particular axiom, even though there are like 40 axioms in this system. That is promising. (No idea if the rest of what it says is meaningful, will investigate.)

https://github.com/nicegeo/nicegeo/issues/125

Whom will I see at the expMath kickoff?

Nobody warned me that humans can be this cute