This week I kept coming back to one idea: doing math is like going to the gym.
I posted that on X on Thursday, and it got more response than anything I've written there so far. I think that's because most of us already feel it. Nobody gets stronger by watching someone else lift. Von Neumann supposedly said that in mathematics you don't understand things, you just get used to them. I used to read that as a joke. Now I read it as advice about training.
Seeing what's already there
I spent part of the week with Giovanni Sambin's Per una dinamica nei fondamenti. In it he argues for foundations that are constructive and dynamic, built up rather than found. I find it really interesting, but I don't fully agree with it. My take: I lean realist. I don't think we build certainty. We train our minds to see, understand, use, and bend what is already there. The training is the hard part, and it's ours to do.
That's also why a line I've been thinking about all week matters to me: proofs can be produced, but understanding has to be exchanged.
Machines as equipment
Then there's AI. This week I read the 2025 AlphaEvolve paper by Georgiev, Gómez-Serrano, Tao, and Wagner, and Kevin Buzzard and colleagues' Xena post "How to Formalize All of Mathematics." I also quoted Terence Tao's "fast food" line. Put together, they leave me with a simple position. Machines can be excellent gym equipment, but they shouldn't lift the weights for me.
I try to live by that. I'm running a small team of bots now. They help me organize my reading, keep track of my work, and even write the first draft of posts like this one. But I edit everything I publish, and I read and answer every reply myself.
What I'm building
The main project this week was a Lean 4 formalization of the fundamental inequality for valued field extensions, e·f ≤ [L:K]. It follows Franz-Viktor Kuhlmann's draft book. I've ported it to Mathlib's current ValuativeExtension API, and it now includes a tower law and a lemma on immediate extensions. It has no sorrys and passes the linter. It's still a work in progress: there's an open draft pull request, and I'm deciding whether it belongs in Tau Ceti or Mathlib. The Xena post made one point clear to me: a formal library only matters if people build on it. So I want to put it wherever it will actually get used.
On the lighter side, I'm still working on Tabboz_mobile, my mobile port of an old cult game.
The library
I also merged my reading library, "Hot Stuff," with a large collection rescued from an old hard drive. I sorted it into shelves and wrote a README to map it all. This week's shelf went from Stillwell's Four Pillars of Geometry and Needham's Visual Complex Analysis to Wald on general relativity, Berndt's edition of Ramanujan's notebooks, Kunen's Set Theory, Dwyer and Friedlander's Topological Models for Arithmetic, Robert Brown's 1828 account of what we now call Brownian motion, and Feynman's The Pleasure of Finding Things Out. There was also Giusto Bellavitis's 1854 work on equipollences. Bellavitis is a distant relative on my grandfather's side, and reading him next to Hamilton's quaternions felt a bit like finding an old family letter.
If something here was useful to you, or you just want to keep me supplied with coffee for the next round of reps, thank you. ☕