AI, Math, the document-drop. Non-Tech Thoughts

So what to make of OpenAI and the future of Math? Here are some points I've either:

thought of myself or heard from a human or read from an AI.

Throughout this post I use the term AI to mean an AI system that produces mathematical results.  I decline to say  OpenAI or  Anthropic as generic terms since about 20 years ago I used  Intrade  as a generic term for Betting Markets---then Intrade went out of business.  I wish I had bet on that happening. Oh well.

1) Some of the proofs were Lean-formalized and some were not.  If a proof is Lean-verified do we know the proof is valid?  The issue is not bugs in Lean.  The issue is that coding a theorem/proof into Lean may be done incorrectly. So Lean might be verifying a proof of a theorem different than what was intended.

Peter Woit, is a string-theory skeptic and a Lean-skeptic. See here

Alexander Bastounis, Fabian Circelli, Anders Hansen argue that the Lean formalization does not correspond to the natural-language proof. See here  

My impression/predictions are:

(1) Lean has a good track record BUT we are in uncharted territory here.

(2) In the end humans will read, understand, and fix the proofs if necessary. This will take time. 

(3) Humans will produce readable writeups that are enlightening. This will take time. 

(4) Some bugs in Lean will be discovered and fixed. This will take time.

(5) Humans will learn how to better code theorems and proofs into the Lean language. This will take time.

2) Most (all?) of the papers were hard to read, even by experts.  Lance asked Claude for a better written version of UGC and he got one: here.  Why didn't OpenAI ask Claude for better writeups?

3) A History of my thought on the Unique Game Conjecture:

In 2006 I thought the Unique Game Conjecture would be proved by 2011. I was wrong.

In 2016 I thought the Unique Game Conjecture would be proved by 2026.  I was right.

In 2026 I thought the Unique Game Conjecture would be proved by 2046. I was right literally but wrong really since in January 2026 I was thinking 10-20 years, not 7 months.

4) Right now AI is merely combining known ideas and writing up the proofs badly as opposed to most mathematicians who come up with new ideas and they write them up well. I am, of course, kidding.

5) There have been barrier results along the lines of  Technique X will not suffice to prove Y' Some papers say this informally, e.g.,  our methods cannot be extended and some papers say this formally, e.g.,  since there are oracles that force P=NP and oracles that force \(P\ne NP\), relativizing techniques do not suffice to resolve P versus NP  (My PhD is on oracles, yet I replaced  recursion-theoretic techniques with  relativizing techniques because ChatGPT is the boss of me.)

What we really want to prove is that known techniques won't solve a problem, hence we need to look for new techniques.

If problem X has not been solved within 10 years by AI, then is it safe to assume that known techniques will not suffice?

Probably not:

a) AI will not make all connections between all the parts of math within 10 years, maybe not ever.

b) AI companies might stop having their machines work on math problems. I'm surprised they are doing that now since mathematicians who want to solve open problems are not a big market. Then again, they could advertise as follows: Buy Our Theorem Prover and you Might Solve a $1,000,000 Math Problem!!! or a Salmon (see here)!!!

6) The notion that AI is combining known ideas is true but is not a problem. However, might the following happen: What if within 10 years all math that can be done with known techniques will have been done.  Then either

a) Humans will step up to the plate and come up with new ideas.  Let's hope they never stopped.

b) Humans will have lost the ability to come up with new ideas because they will have been spoiled by AI.  Like if Lance and I had to become hunter-gatherer. Lance's initials would then stand for Lion Food, and Bill's  initials would stand for Bear Grub. (I came up with Lion Food, but I asked Gemini for Bear Grub. I doubt you care. AI-disclosure can be stupid.)

c) AI will be able to come up with new ideas. The current LLM models probably can't do that but they may help design something that can.

d) As noted in comments 5, AI companies might give up on this line of work.

7) When Deep Blue beat Kasparov an ordinary citizen could not purchase a computer that would play grandmaster-level chess. Now an ordinary citizen can download for free a chess playing program that can beat the world chess champion.

Will this happen with AI for Math?  Will an ordinary citizen be able to download for free, or pay a reasonable price for, an AI program that can prove hard theorems?

8) AI-assisted vs AI-generated may be a big distinction. Or not. Or it may be hard to tell the difference.

I can imagine working on a project where I do some, an AI does some, and I don't really want to figure out and report on who did what part. Similar to human co-authors today. This comes up when one of my HS students enters the Regeneron Science Talent Search and the forms ask in 16 different ways What was their contribution  and  What was your contribution? In the future will they ask  What was the AI contribution? 

9) Hypothetical:

I ask  AI to prove \(P\ne NP\) and it gives me a proof that I rewrite to be readable.  I submit it to STOC, honestly acknowledging what my contribution was, which is mostly exposition.  Assume I meet the ACM authorship criteria.

a) Is the fact that I used AI held against me?

b) Should the paper get in?

c) Do I get the Millennium Prize and hence $1,000,000?

d) Do I win a Turing Award and hence another $1,000,000?

10) How is OpenAI making money on this? Three sources that I know of, New Scientist, Science Magazine, and Crypto Briefing (I am having trouble getting the links to work) put the cost at around 15 million dollars.  After OpenAI spent that much money solving a Millennium problem, they stated that they would not try to collect the $1,000,000 (it's not clear they would have qualified for it). That seems odd.  What is their business model? To generate buzz? If so then note the following:

I have asked my non-math friends (Lance is surprised I have non-math friends) if they have heard about the OpenAI Document Drop.  No. Some had vaguely heard that AI solved an important problem that was worth some money, I assume that's Navier-Stokes, but that's it. No buzz.

The Atlantic Monthly has published an article about this titled OpenAI Just Carpet-Bombed Mathematics (see here)   This will give OpenAI more publicity.  Is it good or bad publicity?  There is a famous quote there is no such thing as bad publicity.  Is it true? See here.

As I finish this post (Translation: As I argue with Chatty about this post) OpenAI has announced that it will give $5 million to the Simons Foundation initiative to help mathematicians examine, understand, and build on results produced by AI.  That may help explain its community engagement, but the existence of a business model is still an open question.

As I finish this post (Translation: As I argue with my AI-skeptical proofreader) my proofreader announced that he knows OpenAI's business model:

Delusion and IPO or Delusion plus PR to get more funding. The IPO is looking less likely.

Is he right? Is that really a business model?  

Here is a link about the business model: here.

I wrote most of this blog post  on Tuesday Oct 13, 2026. I posted it on Oct 18, 2026. Between Oct 13 and Oct 18 the post aged: at a funeral I went to today (Oct 16, 2026-Boss's day!) non-math people asked me  Now that OpenAI can solve open math problems, how do you stop your students from cheating on homework? So non-math people have heard the news, though they don't quite understand it.

11)  I told my Mom that AI had solved some problems that I cared about and that I was happy about that. She asked  Can  AI  fix my answering machine and then have Lean verify that it works?

12) On  Scott's blog (see here), comment number 12 by Tristan, perhaps unintentionally, raised an interesting question. Here are some quotes from Tristan's comment:

But perhaps the occasion calls for a little reflection. If a pattern-interpolating autocomplete can produce your theorem quite so readily, one is entitled to wonder how intellectually demanding the enterprise was to begin with. Perhaps what you took for creativity and insight was, on closer inspection, neither.

Algebraic geometry [Tristan's field] is, mercifully, a field in which genuine creativity remains indispensable: one must actually conceive and construct new mathematical objects, rather than rearrange familiar patterns and dignify the exercise with the word `discovery'. It is precisely this sort of work that lies beyond the capacities of a glorified autocomplete.

a) Such elegant arrogance! Such elegant nonsense! Such arrogant nonsense!

b) This is the kind of quote that will age badly once OpenAI begins solving problems in Algebraic Geometry.

c) I disagree with him: there are easy and hard problems in all fields of math. Algebraic Geometry is an older field, so perhaps there is less low-hanging fruit. But this is a minor point and not the fundamental difference he makes it out to be. And I hardly call the Unique Game Conjecture or L=RL low hanging fruit.

d) Still, to turn his thoughts into  an intelligent question: What types of math problems are more prone to have AI solve them?

e) Scott later left the comment:

LOL! That was a delightful parody (at least, I assume it's a parody) of what I've now heard dozens of times in earnest.

Bill here: I FELL FOR IT.

f) Anon later left a comment that flagged Tristan's post as AI-generated by running it through an AI program to detect AI-generated writings: here.

Bill here: I NEVER SUSPECTED IT WAS AI. FROM NOW ON I WILL SUSPECT EVERYTHING IS AI.

13) A 1985 article in Kvant, a Soviet Mathematics Magazine, by Uspenskii and Semenov, titled Solvable and Unsolvable Algorithmic Problems, contained the following quote:

Tarski's result [that elementary geometry is decidable] appears to be, and actually is, extremely powerful and even paradoxical.  There is a very extensive area of classical mathematics (namely elementary geometry) which is traditionally thought to require a subtle intellect and which can by no means be reduced to carrying out routine computations, and yet, at the same time, there is an algorithm that can verify the truth of theorems in the area (and provide the proofs). We can console ourselves only in the fact that Tarski's algorithm is not realistic: it requires an inconceivably great amount of time for its implementation.

I leave it to the reader to adapt this quote to the current situation. Or not.

14) So what now for mathematicians? For Math grad students?

a) OpenAI says its model attempted roughly 4000 problems and reported results for 372 families, some full and some partial. So there is still plenty that OpenAI can't do.  But who knows what the future will bring?

b) There are plenty more problems that OpenAI was not given.

c) There is a lot more to research than research. (Both ChatGPT and my proofreader think the last sentence was a typo. It's not.) There are surveys, blogs, raising questions, and rewriting proofs so they are readable.  Will Tenure committees, the NSF,  and others,  see it that way?

e) I wonder if in the future the quality of exposition may be more important since the journals and conferences will just assume that the brilliant ideas were done by AI and give the human less credit. If Math dissertations end up being more readable, I call that a win.