on being wrong about ai mathematics

on being wrong about ai mathematics

A few weeks ago, I wrote about OpenAI’s proposed solution to the forced Navier–Stokes problem.

My argument was basically that AI seemed especially good at problems that could be turned into search: find an idea for a construction, build a counterexample, check it, throw it away if it fails, and repeat that a stupid number of times.

I thought universal statements would take longer.

Today, I learned that I was just completely wrong!

OpenAI just released 722 manuscripts across 372 problem families, mostly produced by an internal model.

And these are not just counterexamples.

They claim results on Goldfeld’s conjecture, the irrationality of Catalan’s constant, the hot spots conjecture, De Giorgi’s conjecture in dimension eight, and global existence and uniqueness for relativistic Vlasov–Maxwell.

Looking at that last one was great for me!

A month ago I was literally using Navier–Stokes regularity as an example of the kind of thing that seemed much harder than finding one construction.

Alas, four weeks later, here we are.

I thought this would take longer, but I was just completely wrong.

I still think I was right about the search part, though. I was just thinking about the search space too narrowly. I suppose with Lean and formal verification in the loop, a much larger part of mathematics can be searched and checked than I expected.

But this also makes me more confident about the second half of what I wrote.

If proofs become cheap, understanding them matters more.

So one thing I’m still optimistic about is the last part:

Humans will still be producing explanations.

Perhaps I will last another 4 four weeks.