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

OpenAI has produced proofs of long-open mathematics problems, including a result establishing that the chromatic number of the plane is at least 5 and a proof of the Erdős-Turán conjecture for arbitrarily long arithmetic progressions, according to a blog post by a computational complexity researcher citing Lance Fortnow's and Scott Aaronson's coverage. The plane-coloring proof rules out a proper 5-coloring of R^2 by showing no weak measurable proper 5-coloring exists, improving on the previous lower bound of 5 derived from Jaan Parts' 509-vertex graph, which itself reduced a 1,581-vertex construction. The author calls the Erdős-Turán result, which Bloom and Sisask had only established for 3-term progressions in 2020, the most important and impressive of the new results, while skeptics including Peter Woit question whether Lean-formalized proofs are necessarily correct.

Lance blogged on the OpenAI solutions to many problems here https://blog.computationalcomplexity.org/2026/10/open-no-more.html and also created a website of the TCS-related problems OpenAI claims to have solved here https://lance.fortnow.com/openai-math-tcs.htm . 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 https://scottaaronson.blog/?p=10169 Peter Woit weighted in on what he calls the Slopocalypse https://www.math.columbia.edu/~woit/wordpress/?p=15896 . 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 https://arxiv.org/abs/2610.08144 . 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. The proof that $5\le \chi$ is hard: it involves a 1,581-vertex graph, later reduced to 509 vertices https://arxiv.org/abs/2010.12665 by Jaan Parts, who probably did it in parts. 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 <https://doi.org/10.1016/0097-3165 81 90014-5 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 https://arxiv.org/abs/2007.03528 . The general result for 4-term progressions was open. 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$. $W k, r \le 2^{2^{r^{2^{2^{k+9}}}}}$. $W k,r \ge \beta r^{k-1}$ for some absolute constant $\beta$. The improvement https://github.com/openai/math/blob/main/preprints/Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026/paper.pdf : 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 https://github.com/openai/math/blob/main/lean/docs/160.md . 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 https://arxiv.org/abs/1011.4105 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 https://doi.org/10.1007/s00493-008-2099-1 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 https://arxiv.org/abs/2608.14454 that $g 3 n \ge n^{2/3-o 1 }$, but the conjecture remained open for general $d$. OpenAI showed https://github.com/openai/math/blob/main/preprints/The-higher-dimensional-Erdos-distinct-distances-conjecture-September-23-2026/paper.pdf 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 https://doi.org/10.2307/1970289 and Matiyasevich https://iopscience.iop.org/article/10.1070/RM1972v027n05ABEH001386/ 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$. 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 https://www.cs.umd.edu/~gasarch/BLOGPAPERS/H10-domains.pdf . -------------------------------------------- 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 https://math.berkeley.edu/~slaman/talks/sw.pdf . 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. There are very few people working on this problem. It may take a while to get it human-understood.