5 Comments
User's avatar
Kai Williams's avatar

This is a good summary of the current state of math! I just finished a slightly different roundup (trying to talk to mathematicians directly) so this has been top of mind for me. (I hope you don't mind the link: https://www.understandingai.org/p/mathematicians-are-grappling-with)

One thing that surprised me when I talked with a bunch of mathematicians is that some of them believe that AI will eat the rest of the ladder of abstraction fairly quickly. Humans can jump up a level, but only so many times. AI may end up being better at digestion as well as problem solving and verification. This may seem unlikely today, but I think it's a possibility worth considering seriously. Especially as AI systems grow more autonomous.

Alberto Romero's avatar

Thanks Kai, I actually cited your post (as well as your earlier one). Super interesting stuff - changed my mind in a couple of ways and I ended up including the view that maybe there are no "safe harbors" within or outside mathematics. If Al eats the entire ladder anyway, then mathematicians - and all of us next - need to prepare even more (I agree saying "just go up" sounds exactly like "goalpost moving").

Kai Williams's avatar

Sorry if I was being annoying with the link! Thanks for the citation.

I definitely did some grieving on Saturday with the Astra results (I long thought I was going to become a mathematician; Saturday might have been the day I decided for good not to go to math grad school), but the experience also felt like something that everyone will have to go through at some point.

Though I'm not sure that "just go up" is actually goalpost moving (in a pejorative sense). One of the beautiful things about moving goalposts is that we learn more about what we actually want. For many people, that may continue to be rising on the ladder of abstraction

Hugo's avatar

The $2,000 and the proof indigestion are the same fact. Generation got cheap and verification didn't, so the ratio between them collapsed, and everything in section VIII follows from that alone. Which also explains the counterexample bias you flag: a counterexample carries its own verification, a proof outsources it. The asymmetry isn't about abduction being hard. It's that AI is producing exactly the results whose checking cost stayed near zero, and stalling where the cost sits on us.

Firewall's avatar

Very true, if you didn’t get to the UC Berkeley Agentic AI Summit you may benefit from my summary: https://substack.com/@thefirewall/note/c-307976585?r=5dv35z&utm_source=notes-share-action&utm_medium=web