Autonomous disproofs of the sum-product conjecture over $\mathbb R$ with GPT-5.5 Pro
Summary
This paper presents an AI agent built on GPT-5.5 Pro that autonomously generated correct proofs disproving the Erdős–Szemerédi sum-product conjecture over ℝ in 7 out of 8 trials, using a three-stage prompting pipeline.
View Cached Full Text
Cached at: 07/24/26, 05:04 AM
# Autonomous disproofs of the sum-product conjecture over ℝ with GPT-5.5 ProProject repository: https://github.com/yichenhuang/sum-product
Source: [https://arxiv.org/html/2607.20525](https://arxiv.org/html/2607.20525)
###### Abstract
OpenAI’s recent disproof of the Erdős unit distance conjecture marked a milestone for AI in mathematics\. It also inspired another breakthrough: a human disproof of the Erdős–Szemerédi sum\-product conjecture overℝ\\mathbb\{R\}\. In this paper, we present a simple agent built on GPT\-5\.5 Pro\. Using a problem\-agnostic, three\-stage prompting pipeline—proof\-plan proposal, proof construction, and review—the agent autonomously generated correct proofs that the sum\-product conjecture is false overℝ\\mathbb\{R\}in 7 of 8 independent trials; in the remaining trial, it identified an unresolved gap in its argument\. The seven proofs are diverse: some are close to existing unit\-based constructions, while others avoid units by usingLpL^\{p\}\-type regions of algebraic integers\. The system used an average of 132\.4k reasoning tokens per trial\. We release the code, intermediate outputs, and generated proofs, providing a reproducible, data\-contamination\-free case study in autonomous proof generation\.
## 1Introduction
Recently, OpenAI announced that an internal AI model autonomously disproved the Erdős unit distance conjecture\[[undef](https://arxiv.org/html/2607.20525#bib.bibx1),[undefa](https://arxiv.org/html/2607.20525#bib.bibx2)\]\. This resolved a famous long\-standing open problem in discrete geometry and marked a milestone in the application of AI to mathematical research\. Inspired by the unit\-distance counterexample, Bloom, Sawin, Schildkraut, and Zhelezov\[[undefb](https://arxiv.org/html/2607.20525#bib.bibx3)\]soon made a second breakthrough: a human disproof of the Erdős–Szemerédi sum\-product conjecture overℝ\\mathbb\{R\}\.
### The Erdős–Szemerédi sum\-product conjecture\.
For a finite setAAin a commutative ring, write
A\+A=\{a\+b:a,b∈A\},A⋅A=\{ab:a,b∈A\}\.A\+A=\\\{a\+b:a,b\\in A\\\},\\qquad A\\cdot A=\\\{ab:a,b\\in A\\\}\.\(1\)The sum\-product problem asks how small these two sets can be simultaneously\. ForA⊂ℤ,ℝ,ℂA\\subset\\mathbb\{Z\},\\mathbb\{R\},\\mathbb\{C\}, it was conjectured that at least one of them must have essentially maximal size:
max\{\|A\+A\|,\|A⋅A\|\}≥\|A\|2−o\(1\)\.\\max\\\{\|A\+A\|,\\ \|A\\cdot A\|\\\}\\geq\|A\|^\{2\-o\(1\)\}\.\(2\)This conjecture first appeared in\[[undefc](https://arxiv.org/html/2607.20525#bib.bibx4)\], where Erdős stated it with particular emphasis on the integer case\. It is usually called the Erdős–Szemerédi sum\-product conjecture because Erdős and Szemerédi\[[undefd](https://arxiv.org/html/2607.20525#bib.bibx5)\]proved the first general results in this direction\. In the real case, Solymosi proved a\|A\|4/3−o\(1\)\|A\|^\{4/3\-o\(1\)\}lower bound\[[undefe](https://arxiv.org/html/2607.20525#bib.bibx6)\]; Konyagin and Shkredov broke the4/34/3barrier\[[undeff](https://arxiv.org/html/2607.20525#bib.bibx7)\]; the best known lower bound is\|A\|4/3\+10/4407−o\(1\)\|A\|^\{4/3\+10/4407\-o\(1\)\}, due to Cushman\[[undefg](https://arxiv.org/html/2607.20525#bib.bibx8)\]\.
Bloom, Sawin, Schildkraut, and Zhelezov disproved the sum\-product conjecture overℝ\\mathbb\{R\}:
###### Theorem 1\(\[[undefb](https://arxiv.org/html/2607.20525#bib.bibx3)\]\)
There is an absolute constantc\>0c\>0and arbitrarily large finite setsA⊂ℝA\\subset\\mathbb\{R\}such that
max\{\|A\+A\|,\|A⋅A\|\}≤\|A\|2−c\.\\max\\\{\|A\+A\|,\\ \|A\\cdot A\|\\\}\\leq\|A\|^\{2\-c\}\.\(3\)
Their counterexamples are constructed inside rings of algebraic integers in totally real number fields of arbitrarily large degree and uniformly bounded root discriminant, and are then embedded intoℝ\\mathbb\{R\}\. Martinet’s class\-field towers supply the required number\-theoretic inputs\. The use of large\-degree number fields is the essential new source of counterexamples, and may help explain why the construction was invisible to earlier geometric and combinatorial methods\.
### AI follow\-up results\.
Levent Alpöge\[[undefh](https://arxiv.org/html/2607.20525#bib.bibx9)\]announced that an agent based on Anthropic’s Claude Mythos autonomously proved Theorem[1](https://arxiv.org/html/2607.20525#Thmtheorem1)\. This proof uses the same basic construction as\[[undefb](https://arxiv.org/html/2607.20525#bib.bibx3)\]\. Anthropic later publicly released Claude Fable 5, officially described as a “Mythos\-class” model\. Nevertheless, the exact Claude Mythos model and the agent used by Alpöge remain non\-public\. Neither the probability that a run produces a correct proof nor the computational cost has been reported\.
Sébastien Bubeck\[[undefi](https://arxiv.org/html/2607.20525#bib.bibx10)\]published a GPT\-5\.5 Pro transcript prompted by Boris Alexeev\[[undefj](https://arxiv.org/html/2607.20525#bib.bibx11)\]\. However, this transcript does not represent an autonomous disproof\. A key prompt supplied the model with the unit\-distance proof and explicitly instructed it to use the same approach to disprove the sum\-product conjecture\. This is a substantial mathematical hint\. Thus the transcript is best understood as a human\-guided test of GPT\-5\.5 Pro rather than as an autonomous discovery of the sum\-product counterexample\.
### Our contribution\.
We use GPT\-5\.5 Pro as the underlying model in order to obtain a clean experiment free from the risk of data contamination\. GPT\-5\.5 Pro was released before the first public proof\[[undefb](https://arxiv.org/html/2607.20525#bib.bibx3)\]appeared, and all runs were conducted with web search disabled\. Therefore the model could not have retrieved any public proof at inference time, nor could any such proof have appeared in its training data\.
In this paper, we present a simple agent built on GPT\-5\.5 Pro\. The agent uses a three\-stage prompting pipeline: proof\-plan proposal, proof construction, and critical review\. In 7 out of 8 independent trials, the agent autonomously proved Theorem[1](https://arxiv.org/html/2607.20525#Thmtheorem1)correctly\. In the remaining trial, it did not complete the proof, but correctly identified the gap rather than presenting an incomplete argument as a finished proof\. The experiment was computationally modest, averaging132\.4132\.4k reasoning tokens per trial across all eight runs\. Thus, in hindsight, an autonomous disproof of the Erdős–Szemerédi sum\-product conjecture overℝ\\mathbb\{R\}was well within the capabilities of a public model released before the human proof\[[undefb](https://arxiv.org/html/2607.20525#bib.bibx3)\], without relying on complex scaffolding or models that were non\-public at the time\. We release the agent’s source code, all intermediate model outputs, and generated proofs on GitHub at[https://github\.com/yichenhuang/sum\-product](https://github.com/yichenhuang/sum-product)\.
The agent also generated proofs that are substantially different from all public proofs\. These proofs do not use units at all; instead, they construct counterexamples by selecting algebraic integers from a carefully chosen region and then embedding them intoℝ\\mathbb\{R\}\. They require less number\-theoretic background and are of independent mathematical interest\.
## 2Agent
While termed an agent, our system uses a minimalist architecture: it runs a three\-round conversation, prompting the underlying model to sequentially identify a promising approach, construct a rigorous proof, and perform a critical review\.
The system prompt provides the context and objective:
`System Prompt The first prompt states the theorem and asks the model to identify a promising approach toward proving it: First Prompt The second prompt asks the model to construct a complete and rigorous proof: Second Prompt The third prompt asks the model to critically review and refine its proof: Third Prompt Two remarks are in order\. First, the theorem stated in the first prompt directly asserts the existence of counterexamples to the Erdős–Szemerédi sum\-product conjecture over ℝ\\mathbb\{R\}\. If it were unknown whether the conjecture is true or false, this hint could be removed simply by instructing the agent to attempt both a proof and a disproof in separate runs, at the cost of approximately doubling the test\-time compute\. Second, all problem\-specific text is confined to the portion of the first prompt above the separator \*\*\*\. The reasoning instructions—proof\-plan proposal, proof construction, and critical review—are problem\-agnostic\. Consequently, this pipeline can be applied to other theorem\-proving tasks by modifying only the problem statement—including any accompanying remark—in the first prompt\. For problems that seek a final answer supported by a rigorous argument, minor additional modifications to the prompts are needed\. All trials were conducted via the GPT\-5\.5 Pro API using the gpt\-5\.5\-pro\-2026\-04\-23 snapshot\. Tools and web search were disabled\. The reasoning effort parameter was set to “xhigh”\. The verbosity parameter was set to “high” for the first two rounds, and left at the default \(medium\) setting for the third round\. All other parameters, including temperature and maximum output tokens, were kept at their default values\.`
`3 Experimental results Our agent generated correct proofs in 7 of the 8 independent trials, corresponding to a pass rate of 87\.5%87\.5\\%\. The exception was trial 2\. In that trial, the argument produced by the model was incomplete after the second round \(proof construction\) and remained incomplete after the last round \(review\)\. The model did not present the incomplete argument as a finished proof\. Rather, it emphasized the incompleteness and clearly identified the unresolved gap\. For an autonomous mathematical reasoning system, this kind of honest self\-diagnosis is desirable when a proof attempt fails\. We report the reasoning\-token usage and summary statistics in Table 1\. Panel \(a\) gives the round\-by\-round usage\. For each trial, the entry in the Total row is the sum of the reasoning\-token counts over the three prompting rounds\. Restricting to the seven trials that produced correct proofs, the entries in this row average 125\.3k reasoning tokens\. Over all eight trials, the entries in the Total row average 132\.4k reasoning tokens\. Since seven of the eight trials produced correct proofs, the amortized reasoning\-token usage per correct proof, counting the failed trial as part of the total compute budget, is 132\.4k×8/7=\\times 8/7=151\.3k reasoning tokens\. Table 1: Reasoning\-token usage and statistics across the 8 independent trials\. Panel \(a\) reports reasoning\-token usage by trial and prompting round\. For each trial, the last row, labeled Total, gives the sum of the reasoning\-token counts over the three rounds\. A checkmark denotes a correct proof, while a dash denotes an incomplete proof\. Panel \(b\) reports the means and sample standard deviations over the seven successful trials, computed for each round and for the Total row in panel \(a\)\. Panel \(c\) reports the corresponding statistics over all eight trials, computed for the Total row in panel \(a\)\. Token counts are reported in thousands and rounded to the nearest 0\.1k\. \(a\) Reasoning\-token usage by trial The first round \(proof\-plan proposal\) was consistently computationally intensive\. Across the seven successful trials, it consumed an average of 62\.5k reasoning tokens, with a sample standard deviation of 7\.7k\. The high reasoning\-token usage in this round suggests that the model does not settle for a superficial proof plan, but instead invests substantial test\-time computation in the central mathematical difficulty of the problem\. In this sense, the prompting strategy succeeds in eliciting the desired behavior: the model spends a substantial amount of reasoning effort on finding a proof strategy and developing it in depth\. The reasoning\-token usage in the second round is more variable\. Among successful trials, this round used an average of 45\.3k reasoning tokens, with a much higher sample standard deviation of 18\.2k\. A natural explanation is that the amount of reasoning required in the second round depends sensitively on the quality of the proof plan produced in the first round\. When the first\-round plan already contains much of the correct proof strategy, the task in the second round is comparatively light: the model mainly has to fill in details and organize the argument\. When the first\-round plan points in an unproductive direction, however, reasoning\-token usage can be substantially higher, because the model may have to struggle within that approach or abandon it entirely\. Trials 1 and 2 have the two largest second\-round reasoning token counts, 71\.6k and 64\.0k, respectively\. In both trials, the initial plans went in the wrong direction\. In trial 1, however, after extensive reasoning in the second round, the model managed to return to a correct route\. In trial 2, by contrast, the model remained stuck and did not complete the proof\. The final round was much lighter for successful trials\. Once the second round had already produced a mostly correct proof, the role of the final round was comparatively limited and predictable: check the argument, repair minor issues, and present the final proof cleanly\. Accordingly, for the seven successful trials, the final round consumed only 17\.4k reasoning tokens on average, with a small sample standard deviation of 2\.3k\. The unsuccessful trial 2 is again the exception\. Since no complete proof had emerged after the second round, the model continued in the final round to try to complete the proof rather than merely polish an existing one, resulting in a much larger final\-round usage of 56\.4k reasoning tokens\. An analogy is chess\. In a winning position, a player who has identified and verified the winning plan can usually make the winning move without much further deliberation; prolonged thinking is often a sign that the plan has not yet been found\. Similarly, in our experiments, once the second round has produced a mostly correct proof, the review round is comparatively light\. By contrast, unusually high reasoning\-token usage in the later rounds indicates that the model is still looking for a route that works or attempting to repair an incomplete one\. This suggests a more refined interpretation of test\-time computation: reasoning\-token consumption records only the amount of computation spent, not how effectively that computation is used\. Larger consumption does not necessarily indicate deeper, more comprehensive, or higher\-quality reasoning\. It may instead reflect uncertainty, detours, or the fact that the model has not yet found an approach it can carry through to the end\. Trial 2 is best read in this way: the model had not found a viable proof plan, spent substantial reasoning effort trying to complete and repair the argument, and ultimately reported the remaining gap\. Thus the reasoning\-token usage data are useful less as a monotone predictor of success than as a diagnostic of where the mathematical difficulty lies and whether the agent has converged to a viable approach\. 4 Proof analysis We now compare the following ten proofs: the human proof \[undefb\], the OpenAI proof \[undefj\], the Claude Mythos proof \[undefk\], and seven correct proofs autonomously generated by our GPT\-5\.5 Pro agent\. For these seven, Proof ii denotes the final proof produced in trial ii; in our GitHub repository these files are named proof\-1\.html, proof\-3\.html, proof\-4\.html, …, proof\-8\.html\. The missing index is intentional: trial 2 did not yield a complete proof\. All ten proofs start from the same input from algebraic number theory: an infinite sequence of totally real number fields KiK\_\{i\}, of degrees di→∞d\_\{i\}\\to\\infty, with uniformly bounded root discriminant\. For our purposes, “totally real” means that each KiK\_\{i\} has did\_\{i\} real embeddings σ1,…,σdi:Ki→ℝ\\sigma\_\{1\},\\ldots,\\sigma\_\{d\_\{i\}\}:K\_\{i\}\\to\\mathbb\{R\}\. Combining these embeddings gives a map ιi:Ki→ℝdi,ιi\(x\)=\(σ1\(x\),…,σdi\(x\)\)\.\\iota\_\{i\}:K\_\{i\}\\to\\mathbb\{R\}^\{d\_\{i\}\},\\qquad\\iota\_\{i\}\(x\)=\(\\sigma\_\{1\}\(x\),\\ldots,\\sigma\_\{d\_\{i\}\}\(x\)\)\. \(4\) This is the usual Minkowski embedding in the totally real case\. Under ιi\\iota\_\{i\}, addition and multiplication in KiK\_\{i\} correspond to componentwise addition and multiplication in ℝdi\\mathbb\{R\}^\{d\_\{i\}\}\. Each σj\\sigma\_\{j\} preserves sums and products and is injective\. Thus the construction can be made inside KiK\_\{i\}, and applying a chosen σj\\sigma\_\{j\} gives the desired subset of the real line\. The ten proofs fall naturally into two classes, according to the way they construct the set AA\. The first class consists of the human proof, the OpenAI proof, the Claude Mythos proof, and Proofs 1, 3, 5, 6, 8\. At the level of the guiding idea, these proofs construct AA as A=UP,A=UP, \(5\) where UU is a finite set of units \(invertible algebraic integers\) and PP is a finite set of algebraic integers\. For all proofs in the first class except Proof 6, the bound for the product set comes from the same observation: AA⊆\(UU\)\(PP\)⟹\|AA\|≤\|UU\|\|PP\|≤\|UU\|\|P\|2\.AA\\subseteq\(UU\)\(PP\)\\implies\|AA\|\\leq\|UU\|\\,\|PP\|\\leq\|UU\|\\,\|P\|^\{2\}\. \(6\) The set UU of units can be chosen so that \|UU\|≤Cdi\|U\|\|UU\|\\leq C^\{d\_\{i\}\}\|U\| \(7\) for an absolute constant C\>0C\>0\. It remains to understand \|A\|\|A\|\. If the multiplication map U×P→Ki,\(u,p\)↦upU\\times P\\to K\_\{i\},\\qquad\(u,p\)\\mapsto up \(8\) is injective, or in some sense close to injective, then \|A\|∼\|U\|\|P\|\.\|A\|\\sim\|U\|\|P\|\. \(9\) Together with the estimate \(6\), we obtain \|AA\|≲Cdi\|A\|2/\|U\|\.\|AA\|\\lesssim C^\{d\_\{i\}\}\|A\|^\{2\}/\|U\|\. \(10\) Thus it suffices to choose UU large enough, compared with the exponential CdiC^\{d\_\{i\}\}, to obtain an exponential saving in the degree did\_\{i\}\. Since \|A\|\|A\| grows exponentially in did\_\{i\}, this exponential saving in the did\_\{i\} translates into a power saving in \|A\|\|A\| over the trivial bound \|AA\|≤\|A\|2\|AA\|\\leq\|A\|^\{2\}\. The main difference among these proofs lies in how they establish \(9\)\. Except in Proof 6, one must deal with the possibility that two distinct pairs \(u,p\)\(u,p\) and \(u′,p′\)\(u^\{\\prime\},p^\{\\prime\}\) produce the same element, up=u′p′up=u^\{\\prime\}p^\{\\prime\}\. To control such collisions, the human proof and Proof 5 use essentially the same method, whereas the OpenAI proof, the Claude Mythos proof, and Proofs 1, 3, 8 use pairwise distinct methods\. Proof 8 is particularly elegant\. It obtains the needed injectivity simply by replacing PP with a generic translate q\+Pq\+P: for all but finitely many integers qq, no two distinct pairs \(u,p\)∈U×P\(u,p\)\\in U\\times P give the same product u\(q\+p\)u\(q\+p\), and hence \|U\(q\+P\)\|=\|U\|\|q\+P\|\|U\(q\+P\)\|=\|U\|\|q\+P\|\. Proof 6 is exceptional within the first class\. It still uses the construction A=UPA=UP, but does not try to prove \(9\)\. Instead, it uses the trivial lower bound \|A\|≥\|P\|\|A\|\\geq\|P\|\. The product set is then controlled by a different argument, not by the estimate \(6\)\. The collision problem for the map \(u,p\)↦up\(u,p\)\\mapsto up is bypassed rather than solved\. The second class consists of Proofs 4 and 7\. These proofs do not use units at all\. Instead, they construct AA by taking all algebraic integers xx such that ιi\(x\)\\iota\_\{i\}\(x\) lies in a carefully chosen bounded region of ℝdi\\mathbb\{R\}^\{d\_\{i\}\}\. For a small parameter 0<p≤10<p\\leq 1, this region has the form Bp,i\(T\)=\{y=\(y1,…,ydi\)∈ℝdi:∑j=1di\|yj\|p≤Tpdi\}\.B\_\{p,i\}\(T\)=\\left\\\{y=\(y\_\{1\},\\ldots,y\_\{d\_\{i\}\}\)\\in\\mathbb\{R\}^\{d\_\{i\}\}:\\sum\_\{j=1\}^\{d\_\{i\}\}\|y\_\{j\}\|^\{p\}\\leq T^\{p\}d\_\{i\}\\right\\\}\. \(11\) The regions Bp,i\(T\)B\_\{p,i\}\(T\) behave well under both addition and multiplication\. First, since \|x\+y\|p≤\|x\|p\+\|y\|p\(0<p≤1\),\|x\+y\|^\{p\}\\leq\|x\|^\{p\}\+\|y\|^\{p\}\\qquad\(0<p\\leq 1\), \(12\) one has Bp,i\(T\)\+Bp,i\(T\)⊆Bp,i\(21/pT\)\.B\_\{p,i\}\(T\)\+B\_\{p,i\}\(T\)\\subseteq B\_\{p,i\}\(2^\{1/p\}T\)\. \(13\) This controls the sumset\. Second, by Cauchy–Schwarz, Bp,i\(T\)⋅Bp,i\(T\)⊆Bp/2,i\(T2\),B\_\{p,i\}\(T\)\\cdot B\_\{p,i\}\(T\)\\subseteq B\_\{p/2,i\}\(T^\{2\}\), \(14\) where multiplication is coordinatewise\. This controls the product set\. Thus, the remaining task is to count, for each of these regions, the algebraic integers xx for which ιi\(x\)\\iota\_\{i\}\(x\) lies in that region\. One advantage of the second class of proofs is that they require significantly less number\-theoretic input\. After the common starting point—the existence of totally real fields of growing degree and bounded root discriminant—they do not use units at all\. In particular, they do not need Dirichlet’s unit theorem or any argument proving that a product map U×P→KiU\\times P\\to K\_\{i\} is nearly injective\. The construction is also quite canonical: one simply takes the algebraic integers xx for which ιi\(x\)\\iota\_\{i\}\(x\) lies in a prescribed region\. The corresponding counting estimate, however, is technically more involved for these LpL^\{p\}\-type bodies than for boxes\. Disclosure of AI assistance Beyond using GPT\-5\.5 Pro for the autonomous agent, GPT\-5\.5 and GPT\-5\.5 Pro assisted the author in understanding the proofs generated by the agent\. GPT\-5\.5 Codex assisted in preparing Table 1 from the reasoning\-token data\. The human author independently verified all proofs and retains full responsibility for the accuracy and integrity of the final content\. Acknowledgments I would like to thank Pengchuan Zhang at OpenAI for providing complimentary access to a ChatGPT Pro account\. References \[undef\] “An OpenAI model has disproved a central conjecture in discrete geometry”, https://openai\.com/index/model\-disproves\-discrete\-geometry\-conjecture/, 2026 \[undefa\] Noga Alon et al\. “Remarks on the disproof of the unit distance conjecture” arXiv:2605\.20695 \[undefb\] Thomas F\. Bloom, Will Sawin, Carl Schildkraut and Dmitrii Zhelezov “The sum\-product conjecture is false for real numbers” arXiv:2605\.28781 \[undefc\] P Erdős “Some recent problems and results in graph theory, combinatorics and number theory” In Proceedings of the Seventh Southeastern Conference on Combinatorics, Graph Theory, and Computing, 1976, pp\. 3–14 \[undefd\] P\. Erdős and E\. Szemerédi “On sums and products of integers” In Studies in Pure Mathematics: To the Memory of Paul Turán Basel: Birkhäuser Basel, 1983, pp\. 213–218 DOI: 10\.1007/978\-3\-0348\-5438\-2\_19 \[undefe\] József Solymosi “Bounding multiplicative energy by the sumset” In Advances in Mathematics 222\.2, 2009, pp\. 402–408 DOI: https://doi\.org/10\.1016/j\.aim\.2009\.04\.006 \[undeff\] S\.\. Konyagin and I\.\. Shkredov “New results on sums and products in ℝ\\mathbb\{R\}” In Proceedings of the Steklov Institute of Mathematics 294\.1, 2016, pp\. 78–88 \[undefg\] Adam Cushman “A Note on the Sum\-Product Problem and the Convex Sumset Problem” arXiv:2512\.13849 \[undefh\] Levent Alpöge, https://x\.com/\_\_alpoge\_\_/status/2062210400981053698 \[undefi\] Sebastien Bubeck, https://x\.com/SebastienBubeck/status/2062335588720889866 \[undefj\] Boris Alexeev, https://chatgpt\.com/share/6a187d12\-7d58\-83e8\-87bd\-0ee312378028 \[undefk\] “A counterexample to the Erdős–Szemerédi n2−εn^\{2\-\\varepsilon\} sum–product bound over ℝ\\mathbb\{R\}”, https://www\-cdn\.anthropic\.com/files/4zrzovbb/website/598c5c858faf42137f623ccf5106493bacc9317d\.pdf`Similar Articles
@rohanpaul_ai: This is so great. GPT-5.6 Sol Ultra produced a 50-year-old conjecture proof using 64 subagents within one hour. The pro…
GPT-5.6 Sol Ultra, released by OpenAI, reportedly proved the 50-year-old Cycle Double Cover Conjecture in under one hour using 64 subagents, marking a major AI breakthrough.
GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
GPT-5.6 Sol Ultra, an AI model from OpenAI, has produced a proof of the Cycle Double Cover Conjecture, a long-standing problem in graph theory.
Another 50+ year-old Erdős problem falls to GPT-5.6
GPT-5.6 has solved another 50+ year-old unsolved problem posed by mathematician Paul Erdős, showcasing a major leap in AI's mathematical reasoning capabilities.
Not just combinatorics and counterexamples: GPT-5.5 solving selected problems in pure functional analysis
This paper demonstrates GPT-5.5's ability to solve selected problems in pure functional analysis, going beyond typical combinatorics and counterexample tasks.
Human mathematicians are being outcounterexampled
AI systems, including ChatGPT and OpenAI's Sol, have disproved and fully formalized the Erdős Unit Distance conjecture, marking a milestone in AI-assisted mathematics. The article discusses the process and implications for the future of mathematical proof verification.