Recently Solved Math Problems

What changed

Erdős conjectured that if A ⊆ {1,…,N} has n elements with all subset sums distinct, then N ≫ 2ⁿ (i.e. N ≥ c·2ⁿ for a universal c > 0), a $500 prize problem. GPT-6 Astra (OpenAI, pre-release), working with Epoch AI's Tom Adamczewski, produced sum-distinct sets with N ≤ ε·2ⁿ for every ε > 0, disproving the conjecture; the proof is Lean-verified and erdosproblems.com records the problem as disproved.

AI contribution

Found in 2 of 4 exploratory runs outside the formal FrontierMath Erdős benchmark; construction via rational matrices with small determinant, integral changes of basis and a binary-block construction. Lean-verified (~4,600 lines). Thomas Bloom updated the problem's status to disproved.

Date basis

Solution date per Epoch AI / community trackers (28 Aug 2026); announced with the FrontierMath Erdős benchmark on 1 Sep 2026; status changed on erdosproblems.com / Tao's database 3 Sep 2026

Tools

GPT-6 Astra

What changed

Whether a Hadamard matrix of order 668 exists was the smallest open case of the Hadamard conjecture for ~21 years. Levent Alpöge, Philippe Voinov and Saul Reynolds-Haertle with Claude produced explicit Hadamard matrices for order 668 and for every previously unknown admissible order up to 2000.

AI contribution

Announced by Alpöge crediting 'a team of three humans and Claude' (an internal Anthropic model). Epoch AI lists it as solved by AI, reserving the right to revise if humans supplied the core ideas. The matrices are directly checkable.

Date basis

Epoch AI FrontierMath open-problems page / announcement on X (12 Aug 2026)

Tools

Claude (internal Anthropic model)

What changed

The inverse Galois problem asks whether every finite group is the Galois group of some extension of Q. By 1989 all sporadic simple groups except the Mathieu group M23 had been so realized. Huang, Jackson, Lee, Poonen, Pries and Zhang used a non-rigid triple of conjugacy classes and explicit Belyi-map computations to construct a degree-23 polynomial over Q whose splitting field is a regular M23-extension of Q unramified outside {2, 3, 23}, completing the sporadic-groups case of the problem.

Verification notes

Preprint by six named mathematicians (incl. Bjorn Poonen), consistent with independent press coverage (UConn) and Epoch AI's tracking of the problem; no dispute found. Not yet in a refereed journal. Wikipedia link left null: en.wikipedia.org was unreachable from this environment this run (network egress policy), so no page could be verified to exist yet.

AI contribution

Purely human proof; Epoch AI tracked this as a FrontierMath open problem and explicitly did not classify the solution as AI-assisted.

Date basis

arXiv v1 posting date of arXiv:2608.08538

What changed

The HRT conjecture asserted that any finite collection of distinct time-frequency shifts of a nonzero L^2 function is linearly independent. Faulhuber, Petersen, van Velthoven and Voigtlaender constructed a Schwartz function with 12 linearly dependent time-frequency shifts, disproving the conjecture even for Schwartz functions.

AI contribution

A third-party tracker attributes GPT-5.6 Pro assistance; the arXiv abstract does not mention AI. Recorded as unknown.

Date basis

arXiv v1 posting date of arXiv:2608.05044 ('Linear dependence of time-frequency shifts of a Schwartz function')

What changed

Sendov's conjecture asserts that for any polynomial of degree n >= 2 with all zeros in the closed unit disk, each zero has a critical point within distance 1. Previously known only for small degrees and (Tao, 2020) for sufficiently large n, it was proved for all n >= 2 by Lech Mazur using an AI-agent workflow (GPT-5.6 Pro via ProofAtlas), with a Lean formalization; Terence Tao published a 'digestion' confirming the proof is elementary and complete.

AI contribution

ProofAtlas states GPT-5.6 Pro 'played a substantial role in mathematical exploration, proof development, computational testing, adversarial auditing, and exposition' under human direction. Lean development of ~92,800 lines builds with no sorries; ProofAtlas notes statement-alignment review still pending. Tao's digestion (with AI assistance) treats the proof as complete; numerical verification is required for 5 <= n <= 200.

Date basis

Date on Mazur's proof PDF ('A computer-assisted proof of Sendov's conjecture', August 5, 2026) and ProofAtlas Lean formalization page; Tao's expository post followed August 12, 2026.

Tools

GPT-5.6 Pro (via ProofAtlas agent platform)

What changed

Connes conjectured that an ICC group with Kazhdan's property (T) is determined by its group von Neumann algebra (W*-superrigidity). OpenAI's Astra constructed infinitely many pairwise non-isomorphic property (T) groups with isomorphic von Neumann algebras (also answering a finite-to-one question of Popa), and independently Shuoxing Zhou (with GPT-5.6 Sol assistance) gave two explicit non-isomorphic ICC property (T) groups with isomorphic von Neumann algebras.

AI contribution

Astra result carries a Lean certificate per OpenAI; Zhou's paper acknowledges GPT-5.6 Sol assistance and was completed concurrently and independently. A non-peer-reviewed PhilPapers/PhilArchive note (J. L. Nielsen) claims the disproofs are invalid; no credible expert dispute located.

Date basis

OpenAI Astra announcement (August 1, 2026); Zhou's independent preprint arXiv:2608.02327 posted August 3, 2026.

Tools

OpenAI Astra (internal version), GPT-5.6 Sol

What changed

Ehrhart conjectured that a convex body in R^n whose barycenter is its only interior lattice point has volume at most (n+1)^n/n!, with equality only for suitable simplices; known in dimension 2 and for simplices. OpenAI's Astra proved the sharp inequality in every dimension (Lean-certified), and Jihao Liu (with GPT-5.6 Sol, Fable 5 and the Danus system) resolved the equality case the next day.

AI contribution

Astra proved the sharp inequality with a Lean certificate (1 Aug 2026); Jihao Liu, using GPT-5.6 Sol, Claude Fable 5 and other tools, settled the equality case (arXiv:2608.01040).

Date basis

OpenAI Astra announcement (August 1, 2026) for the inequality; arXiv:2608.01040 (August 2, 2026) for the equality case.

Tools

OpenAI Astra (internal version), GPT-5.6 Sol, Claude Fable 5, Danus

What changed

Erdős asked whether the k-color Ramsey number of the triangle grows only exponentially, i.e. whether lim R(3;k)^{1/k} is finite (offering a prize for a proof of finiteness). OpenAI's Astra proved a superexponential lower bound R_k(3) >= k^{k/3 - o(k)}, so R_k(3) = k^{Theta(k)} and the limit is infinite, answering the question negatively; Raphael Steiner (with ChatGPT 5.6 Pro/Sol) extended the result to all odd cycles.

AI contribution

Lean certificate released by OpenAI; OpenAI's own document labels the item 'partial progress' on the asymptotics of R_k(3) but the superexponential bound settles Erdős's finiteness question. Steiner's follow-up abstract: 'The presented proof was found autonomously by ChatGPT 5.6 Pro/Sol.'

Date basis

OpenAI Astra announcement (August 1, 2026); follow-up arXiv:2608.02537 (Steiner) posted August 3, 2026 cites the OpenAI result.

Tools

OpenAI Astra (internal version)

What changed

The compactness conjecture asked whether for every finite family F of graphs some single G in F has ex(n;G) = O(ex(n;F)); the degeneracy conjecture asserted ex(n;H) = O(n^{2-1/r}) for every r-degenerate bipartite H ($500 Erdős prize). OpenAI's Astra gave bipartite constructions disproving both.

AI contribution

Lean certificate (CompactnessAndDegeneracy.lean) published by OpenAI; community review of statement fidelity was still described as pending in early August 2026. The precise form of the 'degeneracy conjecture' disproved should be checked against Erdős problem #146 before relying on it.

Date basis

OpenAI Astra announcement 'Ten advances in mathematics and theoretical computer science' (August 1, 2026)

Tools

OpenAI Astra (internal version)

What changed

Whether every countable group is sofic (approximable by finite symmetric groups) was a central open question in geometric group theory since Gromov's 1999 work and Weiss's 2000 paper. OpenAI's Astra model constructed an explicit non-sofic group, combining Kun–Thom centralizer rigidity with an expander-matching argument realized in the binary Leavitt algebra and Thompson's group V, with a Lean certificate.

AI contribution

Astra produced the construction with a Lean 4 certificate. Andreas Thom (guest post on Tao's blog, 11 Sep 2026) confirms it resolves the question but notes it depends crucially on Kun–Thom (2019) and objected to OpenAI's original framing; OpenAI revised the announcement. An independent torsion-free construction followed (arXiv:2608.02025).

Date basis

OpenAI announcement 'Ten advances in mathematics and theoretical computer science' (August 1, 2026; PDF updated August 6, 2026)

Tools

OpenAI Astra (internal version)

What changed

Whether the winning probability of every finite two-player entangled nonlocal game decays exponentially under parallel repetition was a long-standing open problem, previously known only for special classes (free, projection, anchored games). OpenAI's Astra proved exponential parallel repetition for every finite two-player entangled game.

AI contribution

Lean certificate released by OpenAI; no independent expert writeup located as of 2026-09-11.

Date basis

OpenAI Astra announcement (August 1, 2026)

Tools

OpenAI Astra (internal version)

What changed

It was conjectured that the Cohn–Elkies linear programming bound for sphere packing has exponential growth rate sqrt(e/(2 pi)) per dimension. OpenAI's Astra proved LP_d^{1/d} -> sqrt(e/(2 pi)), determining the exact rate and giving the first improvement since Kabatiansky–Levenshtein (1978) to the general high-dimensional sphere-packing exponent.

AI contribution

Lean certificate released by OpenAI; no independent expert writeup located as of 2026-09-11.

Date basis

OpenAI Astra announcement (August 1, 2026)

Tools

OpenAI Astra (internal version)

What changed

Maxwell conjectured that the electrostatic field of n point charges in R^3 has at most (n-1)^2 non-degenerate equilibrium (critical) points. Arathoon, Ball and Kvalheim exhibited five charges whose potential has at least 24 non-degenerate critical points (versus the conjectured maximum of 16), disproving the conjecture.

AI contribution

Authors state the idea behind the construction (perturbing a symmetric three-charge base with small off-axis charges) was suggested by GPT-5.6 Sol; all verification (Taylor expansions, Hessian classification) done by the authors with Mathematica/Maple. No formal-proof-assistant verification.

Date basis

arXiv v1 posting date of arXiv:2607.27197 ('The Maxwell Conjecture is False')

Tools

GPT-5.6 Sol

What changed

Crouzeix's conjecture states that the numerical range W(A) of a square matrix (or Hilbert-space operator) A is a 2-spectral set: for every polynomial (or holomorphic function) f, ‖f(A)‖ ≤ 2·max_{z∈W(A)} |f(z)|. It was resolved in 2026 by two independent routes within about a week of each other: Shanmu Jin, a neurosurgery resident with no formal advanced-math training, produced a proof during an autonomous ~16-hour run of GPT-5.6 Sol; separately, Emiel Lorist and Felix Schwenninger gave a conventional human proof combining known weaker-estimate tools with a perturbation lemma for 2-dilations (arXiv:2608.03841).

Verification notes

Not yet formally peer-reviewed/published, but the result is endorsed by expert exposition and direct checking: Michel Crouzeix (who posed the conjecture in 2004) reviewed Jin's manuscript and believes it correct, as did numerical analysts Alex Townsend and Anne Greenbaum (Townsend wrote a SIAM News essay on it, 15 Aug 2026). The independent Lorist–Schwenninger proof reaching the same conclusion by a different method is strong corroboration. en.wikipedia.org and arxiv.org were unreachable from this environment this run (network egress policy), so the Wikipedia article seen in search results (and MathWorld's "Crouzeix's Conjecture" page) could not be freshly verified with WebFetch; the Wikipedia link is left null pending confirmation, and the arXiv/GitHub links used above come directly from search results, not guessed.

AI contribution

Jin's proof emerged from a roughly 16-hour autonomous run of GPT-5.6 Sol; he then checked and wrote up the resulting argument, and it was independently checked by Michel Crouzeix himself plus numerical analysts Alex Townsend and Anne Greenbaum. Jin's GitHub repo (jinshanmu/CrouzeixConjecture) includes a partial Lean 4 formalization alongside the LaTeX manuscript. The separately published Lorist–Schwenninger proof reports no AI involvement and corroborates the result by an independent method.

Date basis

Shanmu Jin posted his manuscript/preprint claim on 27 Jul 2026 per press accounts (first public announcement); the independent Lorist–Schwenninger arXiv preprint (2608.03841) followed on 4 Aug 2026.

Tools

GPT-5.6 Sol (ChatGPT Work mode)

What changed

Feige conjectured that for independent nonnegative random variables X_1,...,X_n with E[X_i] <= 1, P(sum X_i < E[sum X_i] + 1) >= 1/e (Feige proved 1/13; later work reached ~0.14). Fu, Han, Wang, Yan, Zhang and Zhou proved the sharp bound b_{n,delta} >= e^{-1} for delta >= 1, establishing the conjecture, with the proof found by ChatGPT 5.6 Pro and then checked and formalized in Lean by the authors.

AI contribution

Paper states 'The proof is found by ChatGPT 5.6 Pro'; Zhengqing Zhou obtained the initial proof by prompting the model to search the literature broadly; the humans checked, rewrote and formalized it in Lean (github.com/pengzhang91/Feige).

Date basis

arXiv v1 submission date of arXiv:2607.23980 as shown on the abstract page (the authors' blog gives July 30, 2026 as the posting date)

Tools

ChatGPT 5.6 Pro

What changed

The conjecture asserted that any fractional single-source flow can be rounded to an unsplittable flow that simultaneously keeps congestion within an additive d_max and does not increase cost. Dmitry Rybin, using GPT-5.6 Pro, found a 7-node, 9-arc counterexample (fractional cost 58, every congestion-legal unsplittable routing costs >= 60), later shown to be one point of an infinite family; the counterexample was formalized in Isabelle/HOL (Archive of Formal Proofs).

AI contribution

Rybin published the ChatGPT conversation (a 58-word prompt) in which the counterexample was found; verification by exhaustive enumeration and an Isabelle/AFP formalization by Arthur Freitas Ramos, David Barros Hulak and Ruy J. G. B. de Queiroz. No journal paper as of 2026-09-11.

Date basis

Rybin's public announcement on X and the same-day Archive of Formal Proofs entry (July 22, 2026); some outlets date the news July 23.

Tools

GPT-5.6 Pro

What changed

The Jacobian conjecture asserted that every polynomial map C^n -> C^n with nonzero constant Jacobian determinant is invertible. Levent Alpöge, using Anthropic's Claude Fable 5, exhibited an explicit three-variable polynomial map with Jacobian determinant -2 that is generically three-to-one, disproving the conjecture for all n >= 3 (the n = 2 case remains open).

AI contribution

Counterexample credited to Claude Fable 5 (Anthropic); problem suggested to Alpöge by Akhil Mathew. Correctness is checkable with any computer algebra system; Kevin Buzzard reports it was checked in Lean and submitted to DeepMind's Formal Conjectures repository. Follow-ups: Andy Jiang's geometric reformulation (credited to GPT), William Thompson's 24-variable cubic-homogeneous reduction (Zenodo, GPT-5.6 Sol), Christopher D. Long's counterexamples to the equivalent Gaussian Moments Conjecture (arXiv:2607.18186), Meng-Yang's counterexample to the Hessian conjecture HC_5 (arXiv:2607.22198), and Romy Mondello's 2D counterexample in characteristic 2 (arXiv:2608.02634).

Date basis

Counterexample presented 19 July 2026 (Wikipedia); announced on X 20 July; Terence Tao's exposition 21 July 2026. No arXiv preprint as of the last scan.

Tools

Claude Fable 5

What changed

Grothendieck asked whether every finite locally free (flat) group scheme of order n over an arbitrary base is annihilated by n; Deligne proved it for commutative group schemes and Grothendieck for reduced bases. Levent Alpöge and Akhil Mathew, using Claude Fable and OpenAI Sol, found a non-commutative group scheme of order 4 over an Artinian ring of residue characteristic 2 that is not killed by 4; the counterexample was autoformalized in Lean (~1,076 lines) and submitted to mathlib.

AI contribution

Question raised by Mathew at the 'Formalizing Fermat' workshop (July 6–10, 2026); the counterexample was found with AI models and autoformalized by Claude Fable; Buzzard compiled the Lean proof and Mathew opened mathlib PR #41748. A public GitHub repository (GrothendieckRankP2) states all constructions, proofs and Lean code were generated by Codex and Claude. No arXiv preprint located.

Date basis

Date of Alpöge's announcement of the counterexample, as reported in Kevin Buzzard's Xena blog post (July 20, 2026); repository manuscripts dated July 11–12, 2026.

Tools

Claude Fable, OpenAI Sol, Codex

What changed

The cycle double cover conjecture states that every bridgeless graph has a collection of cycles covering each edge exactly twice. OpenAI's GPT-5.6 Sol Ultra produced a three-page proof (reducing to cubic 3-edge-connected graphs, building nowhere-zero flows and converting them to cycle double covers via linear algebra over finite fields); Jim Geelen and Sang-il Oum posted expositions of the proof on arXiv within a week.

Verification notes

Confirmed as of 24 Sep 2026. Jim Geelen and Sang-il Oum each independently wrote and posted their own complete expositions of the argument (arXiv:2607.15399, arXiv:2607.16356). The matroid-theory community blog The Matroid Union retitled its coverage "The cycle double cover theorem" (21 Jul 2026) and states plainly "the proof is correct," noting the proof has since been formalized independently in Lean 4 multiple times (by Krystal Guo, Vaibhav Bajpai, Utku Okur, and OpenAI). An independent community audit (rjwalters/lean-genius, GitHub issue #37504) rebuilt the formalization from source (Lean v4.31.0, Mathlib pin 9a9483a9) and confirmed zero sorries/axioms beyond Lean's own foundational ones (propext, Classical.choice, Quot.sound), and that the formal statement correctly captures the unconditional conjecture. No refereed journal publication yet, but the combination of independent expert expositions, multiple independent complete Lean formalizations, and explicit community endorsement clears this dataset's confirmed bar.

AI contribution

OpenAI's PDF states 'The proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex'; reportedly produced with 64 sub-agents in under an hour from a public prompt. No Lean formalization reported; two senior graph theorists (Geelen, Oum) wrote arXiv expositions, but as of mid-July 2026 some outlets still described it as 'under active review'.

Date basis

Public announcement (X post by Ethan Knight / OpenAI PDF), July 10, 2026 (Oum's exposition gives July 11, 2026); expositions arXiv:2607.15399 (Geelen, July 16) and arXiv:2607.16356 (Oum, July 17).

Tools

GPT-5.6 Sol Ultra, Codex (GPT-5.6 Sol) for the writeup

What changed

Whether the Burau representation of the braid group B_n is faithful was known for n <= 3 (yes) and n >= 5 (no, Moody/Long–Paton/Bigelow), leaving n = 4 as a famous open case linked to whether the Jones polynomial detects the unknot. Bharathram, Birman and Brendle proved that the Burau (and hence Jones) representation of B_4 is faithful.

AI contribution

The authors report six months of unsuccessful attempts to get AI chatbots to solve it; the proof is human (Scientific American).

Date basis

arXiv v1 posting date of arXiv:2607.05283 ('The Burau representation of the braid group is faithful for n = 4')

What changed

What is the largest number of points in an n×n grid with no k+1 on a line? The trivial bound is kn. Ghosal, Goenka, Grebennikov, Keevash, Kwan and Pham proved the answer is exactly kn for every k ≥ 3 and all sufficiently large n (following a 2025 result for k ≫ √(n log n)). The original k = 2 (no-three-in-line) case remains open.

Date basis

arXiv v1 posting date (arXiv:2607.05255)

What changed

The Elekes–Rónyai conjecture predicted that for any real bivariate polynomial h that is neither additively nor multiplicatively special, |h(A,B)| >= n^{2-o(1)} for all n-sets A,B. Cosmin Pohoata showed this is false: for h(x,y) = x+y+(x-y)^2 there are arbitrarily large sets A with |h(A,A)| <= |A|^{2-c} for a fixed c>0, building on the Bloom–Sawin–Schildkraut–Zhelezov construction.

AI contribution

Human construction; no AI use indicated.

Date basis

Date of Pohoata's public blog announcement ('Another one bites the dust: the Elekes-Ronyai problem'); no arXiv preprint located as of 2026-09-11.

What changed

The sum-product conjecture predicted that for any finite set A of reals, max(|A+A|, |AA|) >= |A|^{2-o(1)}. Bloom, Sawin, Schildkraut and Zhelezov constructed sets of real (algebraic) numbers with max(|A+A|,|AA|) <= |A|^{2-c} for a fixed c>0, disproving the conjecture over R and C (and the 'many sums and products' conjecture), with extensions to p-adics, finite fields and function fields; the integer version remains open.

AI contribution

The authors used GPT-5.5 Pro during the work, building on the number-field ideas from the AI-found unit-distance counterexample; the construction and proof are human-written.

Date basis

arXiv v1 posting date of arXiv:2605.28781

Tools

GPT-5.5 Pro

What changed

Erdős conjectured that n points in the plane determine at most n^{1+O(1/log log n)} unit distances (the lattice construction being essentially optimal). An internal OpenAI reasoning model produced an infinite family of point sets with more than n^{1+c} unit distances, built from algebraic number fields via the Golod-Shafarevich class-field-tower method, disproving the conjecture (and the related Erdős-Fishburn conjecture); Will Sawin made the exponent explicit (n^{1.014}).

AI contribution

The counterexample was generated by an OpenAI model after a single prompt; the nine listed mathematicians wrote 'Remarks on the disproof of the unit distance conjecture' (a short human-verified digest). Anthropic reported that Claude Mythos independently found a shorter disproof on May 26, 2026 (air-gapped). Lean formalizations reported by Logical Intelligence (May 26, 2026) and Boris Alexeev with OpenAI Sol (June 26, 2026). Gowers called it 'the first time that AI solved a major mathematics problem'.

Date basis

OpenAI announcement and arXiv v1 posting of the human-verified writeup arXiv:2605.20695 (May 20, 2026); Sawin's explicit-exponent paper arXiv:2605.20579 posted the same day.

Tools

OpenAI internal general-purpose reasoning model (unnamed), Claude Mythos (independent later disproof, May 26, 2026)

What changed

Talagrand conjectured that for any set A of Gaussian measure at least 2/3 in R^n, a bounded number (independent of n) of Minkowski self-sums of A contains a large convex set; equivalently, any centered 1-subgaussian random vector is a sum of a universal number of standard Gaussian vectors. Hua, Song and Tudose proved this in all dimensions.

AI contribution

Song and Hua consulted ChatGPT to understand an unfamiliar object and fill a gap; the team ultimately adopted Tudose's alternative argument, so the final proof is essentially human (Scientific American).

Date basis

arXiv v1 posting date of arXiv:2605.10908 ('On Talagrand's Convexity Conjecture')

Tools

ChatGPT (GPT-5.5 Pro)

What changed

Erdős, Sárközy and Szemerédi conjectured that for any primitive set A contained in [x, infinity), sum_{a in A} 1/(a log a) < 1 + o(1) as x -> infinity (the best known bound was ~1.399, Lichtman 2023). GPT-5.4 Pro, prompted by amateur Liam Price, found a proof via Markov chains with von Mangoldt weights, yielding sum_{a>x} 1/(a log a) <= 1 + O(1/log x); Tao, Lichtman and others verified, shortened and extended it (also giving a short proof of the Erdős primitive set conjecture).

AI contribution

The method was 'suggested from output of GPT-5.4 Pro' and had been overlooked since Erdős's 1935 paper; proof verified in Lean per erdosproblems.com. Related problems #164 and #1217 were resolved in the same writeup.

Date basis

Date of the GPT-5.4 Pro solution recorded on Tao's Erdős-problems wiki (April 13, 2026); writeup arXiv:2605.00301 posted May 1, 2026.

Tools

GPT-5.4 Pro

What changed

Benjamini and Schramm conjectured that Bernoulli percolation on every infinite transitive graph is 'sharp' on both sides of the critical point; the subcritical half was settled in 2007, but supercritical sharpness (exponential decay of finite clusters in the isoperimetric profile for all p > p_c) remained open. Diskin, Easo, Radhakrishnan, Sudakov and Tassion proved it for all infinite transitive graphs.

Date basis

arXiv v1 posting date of arXiv:2603.03257 ('Supercritical sharpness of percolation')

What changed

Erdős–Graham–Ruzsa–Straus asked whether there are infinitely many a, b, n with a, b >= eps*n, a! b! | n! (a+b-n)! and a+b > n + C log n. Kevin Barreto and Liam Price, using GPT-5.2 Pro to find the argument and Harmonic's Aristotle to produce a Lean proof, established the intended statement (with b = n/2, a = n/2 + O(log n)); it was regarded as the first Erdős problem fully resolved autonomously by an AI system.

AI contribution

GPT-5.2 Pro produced the proof idea and Aristotle produced a Lean-verified proof; the problem as literally stated had trivial solutions, so the proof addresses the intended (C_1 log n < a+b-n < C_2 log n) version, marked 'proved (Lean)' on erdosproblems.com.

Date basis

Date of the AI solution as reported by Quanta and Tao's Erdős-problems wiki (January 4, 2026); human-readable writeup arXiv:2601.07421 posted January 12, 2026.

Tools

GPT-5.2 Pro, Aristotle (Harmonic)

What changed

Whether the iterates of Nesterov's 1983 accelerated gradient method converge to a minimizer (not just in function value) was open for ~40 years. Uijeong Jang and Ernest Ryu proved point convergence, with the discovery of the proof 'heavily assisted by ChatGPT' (GPT-5), which proposed the key structural reorganization.

AI contribution

Ryu reports ~12 hours over three days with GPT-5; the model proposed approaches and a key reorganization but could not assemble a complete proof; Ryu vetted and wrote the final proof. OpenAI published a case study (24 Nov 2025).

Date basis

arXiv:2510.23513 v1 posting date

Tools

ChatGPT (GPT-5)

What changed

Kim and Vu conjectured that for d = ω(log n), a random d-regular graph on n vertices can be coupled with high probability to lie between two binomial random graphs G(n,p) with edge probabilities asymptotically d/n, so that properties of the well-understood binomial model transfer to random regular graphs. Natalie Behague, Daniel Il'kovič and Richard Montgomery proved the conjecture in full, extending an earlier partial proof (d ≫ log^4 n) by Gao, Isaev and McKay.

Verification notes

No dispute or error reported; covered as a completed, settled proof by Quanta Magazine (18 Sep 2026), which does not treat it as tentative.

AI contribution

No AI involvement reported in any source found.

Date basis

arXiv v1 posted October 2025 (arXiv:2510.20765); exact day not verified because arxiv.org was unreachable via WebFetch/curl this run (network egress policy)

What changed

Jeffery–Witteveen (2025) showed QMA completeness can be amplified to doubly-exponentially close to 1 and asked whether black-box procedures can do better. Aaronson, Harris and Witteveen proved this is optimal: relative to a quantum oracle no polynomial-resource black-box amplification achieves completeness closer than doubly exponential or super-exponentially small soundness.

AI contribution

Aaronson: GPT-5-Thinking suggested studying the rational function Tr[(I-E(theta))^{-1}], the key technical step in the completeness case ('this worked, as we could easily check ourselves'). A commenter (Phillip Harris, later coauthor) then found a simpler determinant-based argument that replaced it. Aaronson noted the suggestion 'should have' been obvious.

Date basis

arXiv:2509.21131 v1 posting date (blog post 27 Sept 2025)

Tools

GPT-5 Thinking

What changed

It was conjectured that every convex polyhedron is 'Rupert', i.e. a copy of it can be passed through a straight hole cut in the original. Steininger and Yurkevich constructed an explicit convex polyhedron with 90 vertices, 240 edges and 152 faces (the 'Noperthedron') and proved, with heavy computer assistance, that it does not have the Rupert property, disproving the conjecture.

AI contribution

Computer-assisted proof (exhaustive numerical/interval search over ~18 million orientation blocks), but no AI/ML component reported.

Date basis

arXiv v1 posting date (arXiv:2508.18475)

What changed

Whether a (very) general smooth cubic hypersurface in P^5 is rational was a famous open problem in birational geometry. Katzarkov, Kontsevich, Pantev and Yu introduced new birational invariants ('Hodge atoms', combining Gromov–Witten invariants with Hodge theory via F-bundles) and used them to prove that a very general cubic fourfold is not rational.

Date basis

arXiv v1 posted August 2025 (arXiv:2508.05105; exact day not verified)

What changed

It was a long-standing open question (widely conjectured true) whether the unknotting number is additive under connected sum, u(K1 # K2) = u(K1) + u(K2). Brittenham and Hermiller found the first counterexamples: the connected sum of the (2,7)-torus knot 7_1 with its mirror image has unknotting number at most 5, less than 3 + 3.

AI contribution

Found via a large-scale computer search using SnapPy and related software; no AI/ML component reported.

Date basis

arXiv v1 posting date (arXiv:2506.24088)

What changed

Random d-regular graphs are 'lossless' vertex expanders (small sets S have (1−ε)d|S| neighbors), but no explicit constant-degree construction was known. Hsieh, Lubotzky, Mohanty, Reiner and Zhang gave the first explicit construction of constant-degree lossless vertex expanders (and biregular bipartite versions), with applications to quantum LDPC codes.

Date basis

arXiv v1 posting date (arXiv:2504.15087)

What changed

The Kakeya set conjecture asserts that every compact subset of R^n containing a unit line segment in every direction has Hausdorff (and Minkowski) dimension n. Wang and Zahl proved the n = 3 case, the first resolution beyond the plane, via new volume estimates for unions of convex sets/tubes.

Date basis

arXiv v1 posting date (arXiv:2502.17655)

What changed

It was expected (by analogy with Friedman's theorem for random regular graphs) that a Weil–Petersson random hyperbolic surface of genus g has first Laplace eigenvalue λ1 ≥ 1/4 − ε with probability tending to 1 as g → ∞; previous results reached 2/9 − ε. Anantharaman and Monk proved the optimal 1/4 − ε bound using their theory of 'Friedman–Ramanujan functions'.

Date basis

arXiv v1 posting date (arXiv:2502.12268)

What changed

Erdős showed every set of n nonzero integers has a sum-free subset of size at least n/3 and asked whether the n/3 can be improved by a term tending to infinity. Bedert proved that every set of n integers contains a sum-free subset of size at least n/3 + c log log n, answering Erdős's question affirmatively.

Date basis

arXiv v1 posting date (arXiv:2502.08624)

What changed

The conjecture proposed a weighted L^2 inequality for the Fourier extension operator of a smooth hypersurface, controlled by the supremum of the weight over tubes (via its X-ray transform). Hannah Cairo, then 17, constructed an explicit counterexample (using fractal-like weights), disproving the conjecture.

Date basis

arXiv v1 posting date (arXiv:2502.06137), as recorded on Wikipedia

What changed

For N×N Hermitian random band matrices with bandwidth W, physicists conjectured that eigenvectors are delocalized with GUE statistics when W ≫ sqrt(N). Yau and Yin proved delocalization of all bulk eigenvectors, quantum unique ergodicity and GUE eigenvalue universality for W ≥ N^{1/2+c}, settling the delocalized side of the conjecture (the localized regime W ≪ sqrt(N) remains open). Follow-up work with Dubova, K. Yang and F. Yang extended this to dimensions 2 and 3.

Date basis

arXiv v1 posting date (arXiv:2501.01718)

What changed

Whether a random d-regular graph is Ramanujan (all non-trivial eigenvalues at most 2·sqrt(d−1)) with probability bounded away from 0 and 1 was a decades-old question, the subject of a famous bet between Noga Alon and Peter Sarnak. Huang, McKenzie and Yau proved edge universality for random regular graphs, showing the probability tends to about 69%, so both were 'wrong' in the sense of the bet.

Date basis

arXiv v1 posting date (arXiv:2412.20263)

What changed

Bourgain's slicing problem asks whether every convex body of volume one in R^n has a hyperplane section of (n−1)-volume at least a universal constant c > 0 (equivalently, the isotropic constant is bounded). Klartag and Lehec proved this affirmatively, combining Guan's Dec 2024 bound L_n ≤ C log log n with stochastic localization and stability of the Shannon–Stam inequality.

Date basis

arXiv v1 posting date (arXiv:2412.15044, 19 Dec 2024); Qingyang Guan's key intermediate bound is arXiv:2412.09075 (12 Dec 2024)

What changed

Dudeney's 1902 hinged dissection turns an equilateral triangle into a square using four pieces; whether three pieces could suffice was open for 120 years. Demaine, Kamata and Uehara proved that no three-piece dissection exists, so four pieces is optimal.

Date basis

arXiv v1 posting date (arXiv:2412.03865)

What changed

After Matiyasevich (1970) showed Hilbert's tenth problem is undecidable over Z, it remained open whether the same holds for the ring of integers of every number field (Denef–Lipshitz conjecture). Koymans and Pagano proved that Hilbert's tenth problem has a negative answer for every infinite finitely generated Z-algebra, in particular for all rings of integers of number fields, by constructing elliptic curves with no rank growth in suitable quadratic extensions using additive combinatorics.

Date basis

arXiv v1 posting date (arXiv:2412.01768, submitted 2 Dec 2024). An independent proof by Levent Alpöge, Manjul Bhargava, Wei Ho and Ari Shnidman appeared in January 2025 (out of 2024 range).

What changed

The moving sofa problem asks for the largest-area planar shape that can be moved around a right-angled corner in a hallway of unit width. Jineon Baek proved that Gerver's 1992 sofa (18 curve sections, area 2.2195…) is optimal, resolving the problem.

Date basis

arXiv v1 posting date (arXiv:2411.19826, 29 Nov 2024)

What changed

The conjecture states that for a prime p ≡ 1 (mod 4) with fundamental unit ε = x + y(1+√p)/2 of Z[(1+√p)/2], p does not divide y. Reinhart found the first counterexample, p = 331914313984493, by computational search, disproving the conjecture.

AI contribution

Computational search (algorithms of Stephens–Williams; primality verified with Mathematica/PARI-GP), no AI.

Date basis

arXiv v1 (arXiv:2410.21864); the v1 manuscript is dated 29 Oct 2024 (alphaXiv lists 31 Oct 2024), so the exact day may be off by one or two days.

What changed

Yao conjectured that uniform probing is the optimal greedy open-addressing hash-table strategy, with expected worst-case probe cost growing linearly in 1/(1−load). Krapivin, Farach-Colton and Kuszmaul disproved it with a non-greedy scheme achieving (log(1/(1−load)))² worst-case expected probes, and proved this is optimal.

Date basis

Presented at FOCS 2024 (Oct 2024); arXiv:2501.02305 posted 4 Jan 2025

What changed

The Stanley–Stembridge conjecture states that the chromatic symmetric function of the incomparability graph of any (3+1)-free poset is e-positive (a nonnegative combination of elementary symmetric functions). Hikita proved it by giving a probabilistic interpretation of the e-expansion coefficients of the chromatic quasisymmetric function of unit interval graphs.

Date basis

arXiv v1 posting date (arXiv:2410.12758, 16 Oct 2024)

What changed

Friedlander and Iwaniec conjectured that there are infinitely many primes of the form p^2 + 4q^2 with both p and q prime (Gaussian primes with prime coordinates), with an asymptotic count. Green and Sawhney proved this (and more generally for p^2 + nq^2 with n ≡ 0 or 4 mod 6) using Gowers norms and the quasipolynomial inverse theorem.

Date basis

arXiv v1 posting date (arXiv:2410.04189, 5 Oct 2024 per Semantic Scholar record)

What changed

The bunkbed conjecture states that in the 'bunkbed' product of a graph with an edge, under Bernoulli bond percolation, two vertices on the same level are at least as likely to be connected as the corresponding vertices on different levels. Gladkov, Pak and Zimin gave an explicit counterexample (a planar graph on 7,222 vertices), building on Hollom's 2024 hypergraph counterexample, showing the conjecture is false.

AI contribution

The authors initially explored computer/ML-guided search but abandoned it; the final counterexample is a rigorous, non-computer-assisted construction adapted from Lawrence Hollom's hypergraph counterexample.

Date basis

First public announcement on Igor Pak's blog (1 Oct 2024); arXiv v1 (arXiv:2410.02545) posted 3 Oct 2024.

What changed

Whether the Dirichlet L-value L(2, χ_{-3}) is irrational was a well-known open problem, out of reach of Apéry-style methods. Calegari, Dimitrov and Tang proved that 1, ζ(2) and L(2, χ_{-3}) are linearly independent over Q (in particular L(2, χ_{-3}) is irrational) using a new arithmetic holonomy bound applied to Zagier's construction.

Date basis

arXiv v1 posting date (arXiv:2408.15403, 27 Aug 2024)

What changed

The Aldous–Lyons conjecture asserts that every unimodular random rooted network is a Benjamini–Schramm limit of finite graphs (equivalently, every invariant random subgroup of a free group is co-sofic). Bowen, Chapman, Lubotzky and Vidick disproved it: Part I introduces subgroup tests and reduces the conjecture to a decidability question; Part II (Bowen, Chapman, Vidick) proves the relevant approximation problem undecidable via an MIP*=RE-style compression argument, yielding non-sofic unimodular networks.

Date basis

arXiv v1 of Part I (arXiv:2408.00110, submitted 31 Jul 2024), which announces the negative resolution; Part II completing the argument (arXiv:2501.00173) was submitted 30 Dec 2024 (announced 3 Jan 2025).

What changed

The busy beaver function BB(n) is the maximum number of steps a halting n-state 2-symbol Turing machine can make. The bbchallenge collaboration proved BB(5) = 47,176,870 by deciding the halting behaviour of all ~181 million 5-state machines, with the entire proof formalized and checked in Coq (Rocq).

AI contribution

Proof relies on custom deciders and a machine-checked Coq/Rocq proof; no machine-learning/AI tools reported.

Date basis

Public announcement on the bbchallenge forum (2 July 2024); the Coq proof by contributor 'mxdys' was completed on 10 May 2024; the write-up 'Determination of the fifth Busy Beaver value' appeared on arXiv on 15 Sep 2025 (arXiv:2509.12337).

What changed

The Kervaire invariant problem asks in which dimensions there exist smooth framed manifolds of Kervaire invariant one. After Hill–Hopkins–Ravenel ruled out all dimensions ≥ 254, dimension 126 was the last open case. Lin, Wang and Xu proved that h_6^2 is a permanent cycle in the Adams spectral sequence, so such manifolds exist in dimension 126; hence they exist exactly in dimensions 2, 6, 14, 30, 62 and 126.

AI contribution

Heavily computer-assisted (a program by Lin ruled out 101 of 105 cases in the Adams spectral sequence), but no AI/ML tools reported.

Date basis

First public announcement: Zhouli Xu's talk at the Princeton Algebraic Topology Seminar on 30 May 2024 (announced by John Baez on Mathstodon 29 May 2024); arXiv preprint 'On the Last Kervaire Invariant Problem' (arXiv:2412.10879) posted 14 Dec 2024.

What changed

Schramm asked whether there exist bodies of constant width in R^n whose volume is exponentially smaller than that of the ball of the same width (i.e., whether r_n ≤ 1 − ε for all n). Arman, Bondarenko, Nazarov, Prymak and Radchenko answered yes with an explicit construction of a constant-width body of volume at most 0.9^n times that of the unit ball, for all large n.

Date basis

arXiv v1 posting date (arXiv:2405.18501, 28 May 2024)

What changed

Viterbo's conjecture asserts that among convex bodies in R^{2n} of a given volume, the Euclidean ball maximizes every symplectic capacity (equivalently, capacity^n ≤ n!·volume). Haim-Kislev and Ostrover constructed an explicit counterexample: a Lagrangian product of two pentagons whose Ekeland–Hofer–Zehnder capacity exceeds the conjectured bound.

Date basis

arXiv v1 posting date (arXiv:2405.16513, 26 May 2024)

What changed

Numerical work by Deconinck and Oliveras predicted that periodic Stokes water waves have infinitely many isolated islands ('isolas') of modulational instability in the complex spectral plane. Berti, Corsi, Maspero and Ventura proved the existence of infinitely many such isolas, confirming the conjecture.

Date basis

arXiv v1 posting date (arXiv:2405.05854)

What changed

The geometric Langlands conjecture asserts an equivalence between the category of D-modules on the moduli stack of G-bundles on a curve and a category of quasi-coherent sheaves on the stack of local systems for the Langlands dual group. A team of nine mathematicians proved the unramified categorical conjecture (characteristic 0) in a series of five papers totalling over 800 pages.

Date basis

arXiv v1 of 'Proof of the geometric Langlands conjecture I' (arXiv:2405.03599), submitted 6 May 2024 (Wikipedia gives 6 May 2024 as the announcement date; Quanta reports the write-up was first posted on the authors' website in February 2024). Papers II–V followed on arXiv through September 2024.

What changed

It was conjectured that a Brownian particle advected by a critically correlated, divergence-free random velocity field moves superdiffusively, spreading like sqrt(t·log t)^{1/2} rather than sqrt(t). Armstrong, Bou-Rabee and Kuusi proved the superdiffusive central limit theorem, settling the conjecture.

Date basis

arXiv v1 posting date (arXiv:2404.01115)

What changed

Erdős asked for the least h(k) such that every set of h(k) points in general position in the plane contains an empty convex k-gon. For k = 6 only 30 ≤ h(6) ≤ 1717 was known. Heule and Scheucher proved with a SAT solver (later formally verified in Lean) that every 30-point set in general position contains an empty hexagon, so h(6) = 30.

AI contribution

SAT-solver computation (not machine learning); the proof was formally verified in Lean (Subercaseaux, Nawrocki, Gallicchio, Codel, Carneiro, Heule, ITP 2024).

Date basis

arXiv v1 posting date (arXiv:2403.00737, 1 Mar 2024)

What changed

It was unknown whether every game of the card game Beggar-My-Neighbour (played with a standard 52-card deck) terminates. Brayden Casella found (10 Feb 2024) a starting deal that leads to a periodic, never-ending game; the write-up identifies a 62-trick cycle reached from 30 distinct starting hands, settling the question.

AI contribution

Found by computer search; no AI/ML tools reported.

Date basis

Date of discovery reported on Wikipedia (10 Feb 2024); arXiv write-up 'A Non-Terminating Game of Beggar-My-Neighbor' (arXiv:2403.13855) posted 19 Mar 2024

What changed

Kronheimer asked whether a smoothly embedded surface in a simply connected 4-manifold must (under natural hypotheses on its self-intersection number) have simply connected complement. Hughes and Ruberman answered the question negatively: for every integer n they construct a simply connected 4-manifold with a smoothly embedded surface of self-intersection n whose complement has non-trivial fundamental group, using homological properties of Thompson's group V and sporadic simple groups.

Date basis

arXiv v1 (arXiv:2402.01921) submitted 3 Feb 2024 per alphaXiv; manuscript header dated 6 Feb 2024