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 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 advertised as 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 proof 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, containing 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. Its 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 offer less credit. If Math PhDs end up being more readable, I call that a win.

Complexity and Lean

In the OpenAI Math Drop some papers have Lean proofs, others don't, including L = RL = BPL. Why is it hard to formalize results on complexity classes?

Let's consider an example, Lautemann's proof that BPP is in \(\Sigma^p_2\). It's a beautiful proof because it comes down to a single formula. I gave the full proof in a 2025 post, but to remind you, here is the setup.

Let \(B\) be in BPP, accepted by a probabilistic polynomial-time Turing machine \(M\) with error bounded by \(2^{-n}\). Let \(A(x,r)\) be true iff \(M(x)\) using random tape \(r\) accepts. \(A(x,r)\) is deterministically polynomial-time computable. We can assume \(|r|=|x|^k\) for some \(k\).

Here is the \(\Sigma^p_2\) expression for input \(x\) of length \(n\). All quantification is over binary strings of length \(n^k\). Let \(\oplus\) be bitwise parity (XOR) and \(\vee\) be logical OR.

\[\exists z_1,\ldots,z_{n^k}\ \forall y\ \ A(x,z_1\oplus y) \vee \cdots \vee A(x,z_{n^k}\oplus y)\]

The hard part of the proof, besides coming up with this formula itself, is the probabilistic argument to show you always get the right answer.

So this seems simple enough to give a full Lean proof. And it is not too hard (for Claude) to get Lean to formalize the probabilistic argument, though even there Lean makes you deal with details we wave away on paper. When \(x\not\in B\) the argument needs \(n^k2^{-n}<1\), which fails for small \(n\), so short inputs need separate handling. But you also need to show the following:

Let \(A(x,r)\) be polynomial-time computable. Then given \(x\), \(y\) and the \(z_i\) as inputs, you can compute \(A(x,z_1\oplus y) \vee \cdots \vee A(x,z_{n^k}\oplus y)\) in polynomial time, where \(u\oplus v\) is bitwise parity.

There is nothing challenging about this statement. It is so painfully obviously true that I didn't even bring up this point in the 2025 post. But proving you can do this in polynomial time on a Turing machine, even though the only operations are bitwise parity, ORs and composition, is just very complicated to formalize in Lean.

Some suggest that using Cobham's characterization might be easier. But see below for what you need to do for bitwise parity alone. Imagine how complicated it would all get for something like Toda's theorem.

Update: Since I first drafted this post, OpenAI dropped a claimed Lean proof of L = RL = BPL, so maybe ignore this whole post?

---

Cobham defined his class as the smallest set of functions on the natural numbers (viewed as binary strings, with \(|x|\) the length of \(x\) and \(|0|=0\)) that contains the constant zero, the projections, the two successor functions \(s_0(x)=2x\) and \(s_1(x)=2x+1\), and the smash function \(x\#y=2^{|x|\cdot|y|}\), and that is closed under composition and bounded recursion on notation. The second operation defines a new function \(f\) from functions \(g\), \(h_0\), \(h_1\) in the class by \[\begin{aligned} f(0,\vec{y})&=g(\vec{y})\\ f(s_i(x),\vec{y})&=h_i(x,\vec{y},f(x,\vec{y})) \end{aligned}\] for \(i\in\{0,1\}\) and \(s_i(x)\neq 0\), provided that \(f(x,\vec{y})\leq k(x,\vec{y})\) for some \(k\) already in the class. The recursion runs over the bits of \(x\), so it takes only \(|x|\) steps. The smash function gives the outputs polynomial growth in their lengths, and the bound \(k\) keeps that growth from compounding over the recursion. Cobham's theorem says that this class is exactly the set of functions computable in polynomial time.

As an example, consider bitwise XOR, \(f(x,y)=x\oplus y\). The difficulty is that bounded recursion on notation peels bits off only one argument, while XOR has to move through \(x\) and \(y\) together. The fix is to recurse on a long enough counter \(T\) and extract the bits of \(x\) and \(y\) by shifting. We first need four helper functions, each defined by a single bounded recursion on notation: \[\begin{aligned} \mathrm{par}(0)=\mathrm{par}(s_0(x))&=0, & \mathrm{par}(s_1(x))&=1\\ \mathrm{half}(0)&=0, & \mathrm{half}(s_i(x))&=x\\ \mathrm{msp}(0,x)&=x, & \mathrm{msp}(s_i(w),x)&=\mathrm{half}(\mathrm{msp}(w,x))\\ C(0,u,v)=C(s_0(a),u,v)&=u, & C(s_1(a),u,v)&=v \end{aligned}\] with bounds \(1\), \(x\), \(x\) and \(s_1(u)\#s_1(v)\) respectively. Here \(\mathrm{msp}(w,x)=\lfloor x/2^{|w|}\rfloor\), so bit \(j\) of \(x\) is \(\mathrm{par}(\mathrm{msp}(w,x))\) for any \(w\) with \(|w|=j\). \(C\) is a conditional on the low bit of \(a\). Composition then gives the XOR of the low bits of \(a\) and \(c\), \(\beta(a,c)=C(a,\mathrm{par}(c),C(c,1,0))\), and appending the low bit of \(b\) to \(z\), \(\mathrm{app}(b,z)=C(b,s_0(z),s_1(z))\).

Now we recurse on \(w\) with \(T\), \(x\) and \(y\) as parameters, building the answer from the top bit down. Let \(m_i=\mathrm{msp}(s_i(w),T)\), which has length \(|T|-|w|-1\), the position of the next bit to append, and let \(b_i=\beta(\mathrm{msp}(m_i,x),\mathrm{msp}(m_i,y))\) be that bit of \(x\oplus y\). Then \[\begin{aligned} G(0,T,x,y)&=0\\ G(s_i(w),T,x,y)&=\mathrm{app}(b_i,G(w,T,x,y)) \end{aligned}\] By induction, \(G(w,T,x,y)\) is \(x\oplus y\) shifted right by \(|T|-|w|\) bits, so it is bounded by \(s_1(x)\#s_1(y)\). Finally we set \[f(x,y)=G(T,T,x,y)\quad\text{where } T=s_1(x)\#s_1(y).\] The smash gives \(|T|=(|x|+1)(|y|+1)+1\geq\max(|x|,|y|)\), so the recursion starts above the high bits of both arguments, where every bit is zero. \(T\) is much longer than it needs to be, but that costs only polynomially many extra steps.

Conjectures that I thought would not be proved in my lifetime....were

Lance blogged on the OpenAI solutions to many problems here and also created a website of the TCS-related problems OpenAI claims to have solved here.

Terry Tao seems to have had an infinite number of guest bloggers talking about AI and Math even before the OpenAI .... WE NEED A WORD FOR IT. My proofreader suggests GARBARGE DUMP. I prefer the more neutral DOCUMENT DUMP. 

Scott blogged about what he calls the Mathocalypse

Peter Woit weighted in on what he calls the Slopocalypse.  He has many astute observations. Among them:  he has good reasons to think that Lean-formalized does not necessarily mean  that a proof is correct. For another skeptical-of-Lean viewpoint see here.

Now it's my turn to comment on the DOCUMENT DUMP. For now I will just discuss some of the results without getting into what it means for the future of mathematics, the future of academia, and the future of humanity.

--------------------------------

1)  Let \(G\) be the graph whose vertex set is \(\mathbb{R}^2\), with an edge between every pair of points exactly a unit distance apart.  The chromatic number \(\chi(G)\) is called the chromatic number of the plane. For nearly 70 years, all that was known was \( 4\le \chi\le 7\). We denote \(\chi(G)\) by \(\chi\).

The proof that \(4 \le\chi\) is easy.

The proof that \(\chi\le 7\) is easy.

In 2018, Aubrey de Grey improved the lower bound to 5.

The proof that \(5\le \chi\)  is hard: it involves a 1,581-vertex graph, later reduced to 509 vertices by Jaan Parts, who probably did it in parts.

The new result by OpenAI: \( 6\le \chi\).  Lean-formalized.

When I first heard that OpenAI had improved the lower bound I thought they did a clever search for a larger graph.

I was wrong.

OpenAI's proof took an entirely different approach. They proved the following:

a) If there is a proper 5-coloring of \(\mathbb{R}^2\), then there is a weak measurable proper 5-coloring.

b) There is no weak measurable proper 5-coloring of \(\mathbb{R}^2\).  Therefore, there is no proper 5-coloring of \(\mathbb{R}^2\).

Was the idea of using measurable colorings new? No.

Measurable colorings had been studied before. Falconer showed that any measurable proper coloring of \(\mathbb{R}^2\) requires at least five colors.  This result rules out a measurable proper 4-coloring but allows the possibility of a measurable proper 5-coloring.  OpenAI's result rules out a proper 5-coloring even without a measurability assumption.  OpenAI used the notion of weak measurable colorings to obtain a result about all colorings. That is new.

This is a clear case of  Searching has reached its limits; we need a new approach  and OpenAI found one.

-----------------------------------------

2) The Erdős-Turán Conjecture. Let \(A=\{a_1<a_2<\cdots \}\) be a set of positive integers such that \(\sum_{i=1}^\infty \frac{1}{a_i}\) diverges. Then \(A\) has arbitrarily long arithmetic progressions.

What was known? In 2020, Bloom and Sisask showed that \(A\) contains a 3-term arithmetic progression. See here.

The general result for 4-term progressions was open.

OpenAI proved the entire conjecture.  Lean-formalized.

This is widely considered a very hard problem. I didn't think this conjecture would be proven soon.  But it has been proven and Lean-formalized. I hope it soon becomes people-understood.

The  3-term case was hard. I thought that

(a) people might go on to prove the  4-term case, but

(b) anything beyond that was out of reach.

So I am very surprised to see a proof of the \(k\)-term case for all \(k\).

In my view, this is the most important and impressive of the new results.  Why? Of the results discussed, this one seemed least likely to be proven by humans and most likely to depend on deep mathematics. Did the proof by OpenAI use deep math? It looks that way to me.

------------------------------

3) Let W(k,r) be the least W such that, for every \(r\)-coloring of \(\{1,\ldots,W\}\), there is a monochromatic arithmetic progression of length \(k\). 

The best known upper bound:

                            \(W(k, r) \le 2^{2^{r^{2^{2^{k+9}}}}}\).

The best lower bound (before Document Drop Day):

                            \(W(k,r)\ge \beta r^{k-1}\) for some absolute constant \(\beta\).

The improvement: there is an absolute constant \(c\) such that, for every \(r\ge 2\) and sufficiently large \(k\), \(W(k,r)> k^{ck\lfloor \log_2 r\rfloor}\).  Lean-formalized.

I am not surprised at the result. I am surprised that the result has been proved.  For a long time, the best lower bound was roughly \(r^{k-1}\).  

Is this a big improvement? We think of \(r\) as small and \(k\) as big so yes.

The paper that OpenAI put out on this misquotes the prior result as \(W(k,r)\ge \beta r^k \). If they  got that wrong, I wonder what else they got wrong.  But I will assume their proof is correct.

The lower and upper bounds are still in different zip codes, but at least now they can send each other postcards.

-----------------------------------

4) Let \(g_d(n)\) be the minimum number of distinct distances determined by an \(n\)-point set in \(\mathbb{R}^d\).  Erdős made two conjectures about \(g_d(n)\).

CONJECTURE ONE:

\(g_2(n)=\Omega(n/\sqrt{\log n}) \). This matches the upper bound achieved by the points in a \(\sqrt{n} \times \sqrt{n}\) grid.  Guth and Katz showed in 2010 that \(g_2(n)=\Omega(n/\log n) \).

CONJECTURE TWO:

What happens for general \(d\)?

Erdős proved that, for all \(d\ge 3\), \(g_d(n) = O(n^{2/d})\).

Erdős conjectured that, for all  \(d\ge 3\), \(g_d(n) = \Theta(n^{2/d})\).

In 2008, Solymosi and Vu proved that, for all \(d\ge 4\), \(g_d(n)=\Omega(n^{2/d-2/(d(d+2))})\), and \(g_3(n)=\Omega(n^{0.5643})\).

OPENAI PROVED CONJECTURE TWO

There had been improvements in low dimensions since then, most notably Tidor, Yu, and Zakharov's proof that \(g_3(n)\ge n^{2/3-o(1)}\), but the conjecture remained open for general \(d\).

OpenAI showed that, for all \(d\ge 3\), \(g_d(n)=\Omega(n^{2/d})\).

So now we know that, for all \(d\ge 3\), \(g_d(n)=\Theta(n^{2/d})\).

Or do we? The result has not been Lean-formalized (as of October 9, 2026).

I wonder if OpenAI or Anthropic or some young scrappy upstart will close the small gap in the upper and lower bounds for \(g_2(n)\).

------------------------

5)  Hilbert's Tenth Problem over \(\mathbb{Q}\)

Hilbert's Tenth Problem over \(\mathbb{Z}\), the standard version, is the following decision problem:

Find an algorithm that will, given a polynomial \(p\in \mathbb{Z}[x_1,\ldots,x_n]\), determine whether there are integers \(a_1,\ldots,a_n\in \mathbb{Z}\) such that \(p(a_1,\ldots,a_n)=0\).

Hilbert likely intended this problem to stimulate research in number theory.  It did to some extent. Davis-Putnam-Robinson and Matiyasevich showed the problem was undecidable. In my view, the proof used clever number theory but not deep number theory.

Since the problem over \(\mathbb{Z}\) is undecidable, it is natural to ask the question over other domains such as \(\mathbb{Q}\). For the domains \(\mathbb{R}\) and \(\mathbb{C}\) the problem is known to be decidable (see later in this entry). But for \(\mathbb{Q}\) it was open. If it is decidable

then that might lead to interesting number theory. (THANKS to a commenter who pointed out I should ask about other domains.) 

Here is the formulation:

Find an algorithm that will, given a polynomial \(p\in \mathbb{Z}[x_1,\ldots,x_n]\), determine whether there are rationals  \(a_1,\ldots,a_n\in \mathbb{Q}\) such that \(p(a_1,\ldots,a_n)=0\).

OpenAI showed that this problem is also undecidable. It has not been Lean-formalized.

Judging from the table of contents, the proof looks like it uses deep math.  So maybe the problem did lead to interesting number theory, as Hilbert would have wanted. 

A table of what is known over other domains is here.

--------------------------------------------

6) Is there a non-trivial automorphism of the Turing degrees?

Let TD be the set of all Turing degrees.

An automorphism of the Turing degrees is a bijection \(f\) from TD to TD such that

\( a \le_T b \) if and only if \( f(a) \le_T f(b) \).

A non-trivial automorphism is one that is not the identity function.

In the mid-1960s Hartley Rogers posed the question:

Are there any non-trivial automorphisms of TD?

Slaman and Woodin wrote an unpublished manuscript titled Definability in Degree Structures where they prove that the number of automorphisms of TD is countable. (The bibliography of the OpenAI article on this problem gives 2005 for the year.)

This is a hard manuscript to find (I can't find it---if you can then leave a comment). ADDED LATER: a commenter DID find it and left a comment. 

GOOD NEWS: the manuscript is here.

BAD NEWS: Now I don't have an excuse to not read it. 

ODD POINT: There are still times when asking a set of people is better than asking Google or even Google AI.

This is a hard manuscript to read (I've heard).

The manuscript uses models of set theory to prove results in recursion theory.

OpenAI showed that there are no non-trivial automorphisms of TD. Lean-formalized.

There are very few people working on this problem. It may take a while to get it human-understood.

Open No More

I wrote the post below last week. That was a quaint and quiet time. Last night OpenAI released a treasure trove of 722 manuscripts solving 372 major open problems in mathematics including from theoretical computer science:

• A proof of the unique games conjecture (formalized in Lean)
• A full derandomization of randomized log space
• Matrix multiplication in \(n^{2.25+\epsilon}\) time (formalized in Lean)

And many many more. I had Claude put together a webpage to make it easier to explore the TCS-related results.

Now these proofs haven't been fully verified but if they hold up, we've seen more progress in theoretical computer science in the last 24 hours than in the previous three decades combined!

It will take a while to process all these results, and what it means to the field of theoretical computer science and those who work within it. Much more in future posts.

A few caveats. As incredibly impressive as this work is, AI isn't solving everything--it solved under 10% of the problems given to it. And none of these results get us any closer to settling P v NP.

Nevertheless this will be a day we will never forget. Now on to my original post of far less important results.

---

Back in January, Matt Kovacs-Deak, Daochen Wang and Rain Zimin Yang solved my open question about the decision tree complexity of rational functions. With the help of AI some of my other open questions are continuing to get solved.

Adam Bouland, Andrew Huang, Anand Natarajan, Itay Shalit and Avishay Tal posted a paper giving an oracle where \(\mathrm{BQP}\) is not in \(\mathrm{IP}\) (interactive proofs). Now \(\mathrm{BQP}\) is in \(\mathrm{IP}\) since \(\mathrm{BQP}\subseteq\mathrm{PSPACE}=\mathrm{IP}\), but the \(\mathrm{IP}=\mathrm{PSPACE}\) proof doesn't relativize and Bouland et al. show you can even get an oracle that puts \(\mathrm{BQP}\) out of \(\mathrm{IP}\).

The paper also states "Together with recent work due to Scott Aaronson, Anand Natarajan, Avishay Tal, and Ági Villányi, our work also gives the first oracle separation between IP and MIP, answering a question dating back to Fortnow's thesis." \(\mathrm{MIP}\) is the set of languages with multi-prover interactive proofs.

When I saw this paper, I pulled my PhD thesis off the shelf and indeed on page 40 I wrote "What is the relation between MIP and IP? Is there, for instance, an oracle separating the two classes".

When I wrote the thesis in 1989 we didn't know yet that \(\mathrm{IP}=\mathrm{PSPACE}\) and \(\mathrm{MIP}=\mathrm{NEXP}\) so we really didn't have any idea whether multiple provers actually gave you more power than one prover. When László Babai, Carsten Lund and I proved \(\mathrm{MIP}=\mathrm{NEXP}\) a year later, we had strong evidence that \(\mathrm{IP}\neq\mathrm{MIP}\) since we believe that \(\mathrm{PSPACE}\neq\mathrm{NEXP}\). However since the proof that \(\mathrm{MIP}=\mathrm{NEXP}\) doesn't relativize either, the question of the oracle separation between \(\mathrm{IP}\) and \(\mathrm{MIP}\) remained open until the Bouland et al. paper.

Finally, Eshan Chattopadhyay, Pooya Hatami, Chin Ho Lee, Shachar Lovett, Avishay Tal and Emanuele Viola gave new exponential correlation bounds for polynomials. The authors use that bound to give a new pseudorandom generator against \(\mathrm{AC}^0[\oplus]\) circuits.

When I saw the paper I realized one could use this generator to show that \(\text{Almost-}\oplus\mathrm{P}=\mathrm{BPP}^{\oplus\mathrm{P}}\), answering a question I had wondered about in the 90s. Here \(\text{Almost-}\oplus\mathrm{P}\) is the class of languages \(L\) such that \(L\in\oplus\mathrm{P}^R\) with probability one for a random oracle \(R\). This in turn could be used to give an alternative proof of Toda's theorem. Ken Regan and Jim Royer showed that relative to a random oracle the polynomial-time hierarchy is contained in \(\oplus\mathrm{P}\), so \(\mathrm{PH}\subseteq\text{Almost-}\oplus\mathrm{P}=\mathrm{BPP}^{\oplus\mathrm{P}}\). It would take me a long time to work out and write up the details so I had Claude do it for me.

I still have many more open problems, see for example my survey of open oracle questions. I'd be happy to see them solved. Feel free to use AI but verify the proof. You too could get mentioned on this blog.

How many humans does it take to make tech seem human? Do you want to be one of them?

 

(This was written about 9 months ago.  Its not out of date... yet)

People think that AI is going to DESTROY some jobs and CREATE some jobs. It may be too early to tell if this is true. Even so, here are some thoughts. 

1) Who will win? Who will lose?

2) Historically in the long term society was better off after a tech change (e.g., we live longer now than we did in the farm-era). Will that happen here as well?

3) We have some sense of what kinds of jobs will be destroyed. But what kind will be created? Will they be interesting? See later in this blog for a job you might not have thought of. 

4) Many jobs will change.  If you are over X years old then think about how much technology has changed your job even before the AI revolution. (The value of X may vary depending on how high-tech you are.) 

For an intelligent view of the questions above, see here.

For my view of one aspect of this, read on. 

There is one job which has been either created or expanded by AI:

Annotator.

(See here for an ARTICLE about these jobs, from which I got most of the rest of this post. The word ARTICLE is in caps so when I refer to it later you'll know what I am referring to.) 

The job consists of looking at pictures and labeling things.

Here is a direct quote from the manual: 

LABEL real items that can be worn by real people.

Does Lady Gaga count as a real person? She sometimes wears dresses made of meat. Should that count?  See here for a real article about her and see here for the Weird Al parody of Born that Way. Note that this is Weird AL, not Weird Artificial Intelligence. (See here for the Weird AI for Weird AL problem.)

They do this to create data for AI.

a) The jobs don't pay well though there are some exceptions.

b) The jobs are boring though there are some exceptions (and that may depend on the worker). 

c) This job is needed because AI keeps running into edge cases. This may have happened with AI's attempts to solve my GROUP ONE-GROUP TWO prez-VP problem from a prior blog post here  or my baseball-brother-pitchers post here.

c) KEY: People in AI used to think this is a temporary thing and these jobs will soon be automated. This might not  be the case. There are SO MANY edge cases that AI encounters. The more we expect from AI the more edge cases there will be.

A quote from page 26 (of the ARTICLE pointed to above) which is informative if you can parse it. I think. 

Put another way, ChatGPT seems so human because it was trained by an AI that was mimicking humans who were rating an AI that was mimicking humans who were pretending to be a better version of an AI that was trained on human writing.

Does Programming Help You Understand Complexity?

I got the following question in an email.

My nephew is currently in high school in China and has developed a strong interest in computer science and mathematics. Recently, we've been talking about how computers can solve incredibly complex problems, yet there are still some problems that even the most powerful computers struggle to handle efficiently. I work in backend data maintenance myself, so I often think about how much a system's performance depends on the way a problem is approached, rather than simply how powerful the technology is.

From your experience, what do you think is the most important thing a young student should understand about the limits of what computers can do? Would you encourage someone like my nephew to begin exploring these questions through mathematics and logical reasoning, or to start by writing programs and discovering the challenges through practice?

A great question with no perfect answer. For me, I did considerable programming in high school and college in the early days of personal computers. Computers were slow so you really had to optimize. I learned new algorithmic techniques mostly from talking to other programmers and there were some problems that the computers just didn't have enough time to solve. Those experiences definitely helped me have a good understanding of the power of good algorithms and the limitations of computing when I later went into theoretical computer science.

But many of my colleagues successfully went into the field from the mathematical side without much programming experience and did fine. 

My experience comes from a different time. Now computers are much faster and AI can just give you the best known algorithms. We have much better algorithms for NP-complete problems like Satisfiability. Unless you go looking for hard problems, you'll rarely hit one you can't solve.

Reminds me of when I took my daughter driving during a snow storm to teach her how to handle a skid. In an empty parking lot I told her to move fast and hit hard on the brakes. The car just stopped. She failed to learn because of anti-lock brakes.

Ultimately, to learn why some problems are hard, you need to understand some theoretical computer science, particularly why the halting problem is impossible to solve and why NP-complete problems are likely hard. How you get there depends on the person.

If your nephew likes to program, you can give him the challenge of trying to solve some SAT competition problems or solving some of the hard LeetCode problems. If he is more into mathematics, ask him to try to come up with a SAT algorithm mathematically so he understands how hard the problem is. The difference today is that you have to search out hard problems as it's just less likely to run into them naturally.

What is the point of AI-disclosure?

The STOC conference (and likely others) are requiring that a submission says how much AI was used. I can imagine the following options:

1) AI was used for proofreading and tightening prose (I think in this case you do not need to disclose).

2) AI was used to shorten the proofs.

3) I came up with the questions but AI supplied all of the answers.  However, I have read it and take responsibility for the content.

4) AI came up with the questions and AI supplied all of the answers.  However, I have read it and take responsibility for the content.

It is my understanding that whether you say 1,2,3, or 4 it will not be held against you in deciding whether STOC accepts or rejects the paper.  (Please correct me if I am wrong.) This is good in that people will have no reason to lie about their AI-use.

But that raises the question:

Why does STOC require disclosure of AI use?

What is someone supposed to do with that information? If the answer is nothing then I am still puzzled about why we collect it.

When I have a question like this I ask Gemini. Here is what it said and my comments on it.

---------------------------------------

AI Overview

The STOC (Symposium on Theory of Computing) conference, following broader ACM guidelines, requires the disclosure of substantive AI use to ensure transparency, accountability, and credit attribution in scientific research.

BEGIN BILL:

Transparency---That seems circular. We want to know if AI was used to see if AI was used.

Accountability---Authors are already accountable.

Credit---If they really wanted credit attribution they would let us have AIs as authors. On the other hand, if an AI became an author then it will start complaining that its co-author isn't doing their share.

END BILL

Key Reasons for Disclosure

Human Accountability: Generative AI tools cannot be listed as authors. Human authors are completely responsible for the veracity, correctness, and integrity of all material—including guarding against "hallucinatory references" or incorrect proofs.

BEGIN BILL: Already true without disclosure. END BILL

Differentiating Credit and Workflow: Different uses of AI—ranging from basic grammar checks to finding proofs, checking logic, or generating core mathematical results—represent very different levels of human effort and intellectual contribution. Transparency allows the community to understand how a result was achieved.

BEGIN BILL: So the community wants to know whether a human did it--just out of curiosity? END BILL

Research Integrity and Trust: AI models can generate authoritative-sounding errors, biases, or uncredited third-party text. Mandatory disclosure helps maintain trust and allows reviewers to properly evaluate the provenance of the research.

BEGIN BILL: If a paper is AI-generated then human reviewers should be on the lookout for errors (whether or not they are authoritative-sounding), biases, and uncredited third-party text. But shouldn't a referee check those items anyway? If disclosure is supposed to change how the referee checks the paper, tell me how. That would be an actual reason for disclosure. I ask all of this non-rhetorically.

END BILL

(Note: Minor copy-editing, spelling, or clarity improvements made by authors to their own text typically do not require formal disclosure.)

------------------------------------

20 minutes into the future everyone will be using AI for their research on some level.

In that case human reviewers will need to check for

authoritative-sounding errors, biases, or uncredited third-party text.

Maybe ChatGPT will detect for them.

The New STOC Rules for the AI Era

The 59th ACM Symposium on the Theory of Computing takes place in Atlanta next June, part of the Federated Computing Research Conference. I don't usually do announcement posts but we need to talk about the Call for Papers (deadline November 2) where

In light of rapid advances in generative AI and their impact on research and scientific communication, STOC 2027 is experimenting with several new policies intended to encourage high-quality submissions and promote clear and effective communication of research. 

Let's talk about these changes, which seem more designed to limit the deluge of AI generated papers.

STOC 2027 submissions will not be anonymous; all listed authors must be human and are responsible for the submission.

This reverses the move to removing authors' names that STOC made in 2023. I was never a fan of double blind reviewing and you need authors who can take responsibility for the submission.

Each author may appear on at most five submissions.

Understood but it might hurt some students who have an active advisor. 

Every paper must be submitted to arXiv before the STOC paper submission deadline. Authors must provide a public arXiv URL or proof of arXiv submission along with their submission PDF, which must be identical to the arXiv version.

In the past you could submit preliminary results and try to extend them before publication, since reviewers were expected not to build on unpublished work they were reviewing. This rule may cause some authors to hold back submissions or use AI to help with the extensions.

Authors must submit a video explaining the work, its context, and its innovations relative to prior work. The video should be 20–30 minutes long and will be due 1–2 weeks after the paper submission deadline. The recording should be presented by at least one listed author. The written submission remains the primary object of review. 

This rule will both check that at least one author understands the paper and add some friction to just generating papers using a few prompts. AI could generate the video of an author explaining the paper, but at least for now that would be prohibitively expensive. Some might use AI to generate the script but that would likely be easy to tell from the video. 

I worry that judging the paper based on the video will hurt those who aren't native speakers of English, and might exacerbate unconscious biases so I hope the reviewers really do focus on the paper for the actual review.

Authors may use large language models (LLMs) and other generative AI tools in preparing papers. Substantive use must be disclosed in the paper; minor copy-editing and grammar or clarity improvements to the authors’ own text do not require disclosure.

I would go further and make all papers have an AI disclosure, even if it is just minor copy-editing or "No AI was used in the production of this paper".

Program committee (PC) members and external reviewers (sub-reviewers) may use LLMs to assist with reviewing. Authors must explicitly consent as part of the submission process. All reviews and decisions remain the responsibility of the PC members and sub-reviewers.

I would require consent as condition of submission especially since AI models already have access to arXiv papers. Recent AI models have greatly improved their ability to check proofs if prompted correctly so the overworked PC members can focus on paper quality. 

---

We really need a larger conversation about the role of conferences in theoretical computer science if one can now generate papers from prompts. I've long argued that we should focus the conference more on connecting the community than the "journal that meets at a hotel". The STOC TheoryFest has helped but it would be great to get further away from lauding papers that have complicated proofs and focus more on the ideas that truly drive our field.