A curated, source-linked index of open mathematical problems reportedly solved, refuted, or settled with the help of AI — with a bias toward claims that come with checkable certificates.
This list began by tracking the July 2026 "floodgates" wave: a burst of activity on math X/Twitter in which frontier models and agents produced explicit counterexamples and short proofs to long-open conjectures, often verified in Lean 4 or by DRAT/SAT certificates. It started with a claimed counterexample to the Jacobian Conjecture on 2026-07-20 and cascaded from there.
Each lemma / conjecture is listed on its own line below and links to the relevant write-up. New claims are appearing daily; this index itemizes the ones with a traceable primary source and some form of verification.
This index records claims and their public scrutiny. It does not adjudicate the mathematics. Read the legend and how to read this list before trusting a row.
Each line reads: name — result · field · how long open — what happened (model, person). Verify: what checking exists. date · links.
Result: refuted (counterexample found) · proved (statement proved true) ·
nonexistence (a searched-for object provably doesn't exist).
Verify — whose checking exists, not a judgment by this index: Lean 4 / DRAT
(machine-checked proof) · independent (second verifier, adversarial agent, third-party
artifact, or classical-object check) · author-only (posted witness, transcript, or
hand-checkable arithmetic) · scooped / disputed (priority contested or a rediscovery) ·
under review (extraordinary claim, expert discussion ongoing) · arXiv (a preprint exists).
One line per lemma, newest first. Batches are broken out — every conjecture is its own line.
- WOW-II conjecture 305 — refuted · spectral graph theory · open (unspecified) — one-shotted with Sol 5.6 Ultra (Pedro Lirón de Robles), counterexample images posted with a "can someone check" request. Verify: under review. 2026-07-24 · announce
- Graph conjecture 22 (dmg / zdmg) — refuted · graph theory · open ~6 days — GPT-5.6 Pro found a 9-vertex counterexample (zdmg 9 > 4·dmg 8) with code and an exact verifier (bax). Verify: author-only. 2026-07-24 · announce
- Adenwalla conjecture 4.12 — proved · combinatorics · open ~1 yr — GPT-5.6 Pro (Holter batch of 10): g_m(ab) ≤ (a+1)(b+1) < 2ab for composite n, primes finish it. Verify: author-only. 2026-07-23 · post · chat
- Tang–Zhang conjecture 3.1 — refuted · analysis · open ~9 mo — GPT-5.6 Pro (Holter): at p=3/2, two rational rank-one 2×2 matrices give 1.0363 > the conjectured optimum 1.0347. Verify: author-only. 2026-07-23 · chat
- 14-vertex DDMOG sparsity conjecture — refuted · graph theory · open ~5 wk — GPT-5.6 Pro (Holter): a strongly-connected 22-edge DDMOG (the paper's candidate was 24; 21 impossible by parity). Verify: author-only. 2026-07-23 · chat
- Hashemi conjecture 4.1 — proved · random matrices · open ~3 mo — GPT-5.6 Pro (Holter): explicit finite-free Hermite eigenbasis with mean-zero singular values {2^(−k/2)}. Verify: author-only. 2026-07-23 · chat
- Hypercube edge-multiset problem 7 — refuted · combinatorics · open ~12 days — GPT-5.6 Pro (Holter): 22 landmarks separate all 448 edges of Q7, so edim_m(Q7) ≤ 22, not ∞ (exact value still unknown). Verify: author-only. 2026-07-23 · chat
- Bubboloni–Fumagalli–Praeger conjecture 1 — proved · group theory / graphs · open ~9 mo — GPT-5.6 Pro (Holter): any induced P4 in the enhanced power graph forces one in the ordinary power graph. Verify: author-only. 2026-07-23 · chat
- DeLeo–Henderschedt–Wells conjecture 1.4 — proved · combinatorics · open ~8 wk — GPT-5.6 Pro (Holter): disc(n) ≥ 2^(1−1/⌈n/2⌉), with equality via a lex-merge construction. Verify: author-only. 2026-07-23 · chat
- Friedman conjecture 3.2 — refuted · algebraic geometry · open ~2 days — GPT-5.6 Pro (Holter): on Gr(2,4), the datum (1,5,1,1,5,1) has three positive critical points (two strict local maxima + a saddle). Verify: author-only. 2026-07-23 · chat
- Bóna–Maga–Richey conjecture 3.1 — refuted · combinatorics · open ~7 wk — GPT-5.6 Pro (Holter): the inequality reverses for k ≥ 4 — ρ_{0^k} < ρ_{0^(k−2)10}. Verify: author-only. 2026-07-23 · chat
- Suvagiya conjecture 3 — refuted · spectral graph theory · open ~4 days — GPT-5.6 Pro (Holter): n=32 with step-2 signs (−,+,−,−,+,−,+,+) gives spectral radius 2.7936 < 2.7945. Verify: author-only. 2026-07-23 · chat
- Gray–Payne–Swisher–Watson conjecture 1.2 — proved (claimed) · combinatorics (fixed-perimeter partitions) · very recent (2026 paper) — GPT-5.6 Pro autonomously picked and claimed a proof (FO/FD ratio → 0) after self-critique + 7.3M checks; Holter says "no clue if correct." Verify: author-only, under review. 2026-07-23 · announce
- Graffiti conjecture 284 — refuted · spectral graph theory · open ~30 yr — Capy (Grok 4.5) refuted it in 8 min with the Hoffman–Singleton graph as witness, adversarially reviewed (Justin Sun). Verify: independent. 2026-07-23 · announce · traces
- Brandt regular-supergraph (West's list) — refuted · graph theory · open ~20 yr — Devin found a 9-vertex counterexample with a Farkas infeasibility certificate, reproven in Lean 4 (Jared Zoneraich). Verify: Lean 4, independent. 2026-07-23 · announce · solution
- Graffiti conjecture 39 — proved · spectral graph theory · open ~40 yr — Devin proved
dev(D) ≤ n⁺(G)via Popoviciu + Cauchy interlacing, fully formalized in Lean 4. Verify: Lean 4, independent. 2026-07-23 · announce · proof - Graffiti conjecture 40 — proved · spectral graph theory · open ~40 yr — same four-step argument gives
dev(D) ≤ n⁻(G); Lean 4, axioms audited (Devin). Verify: Lean 4, independent. 2026-07-23 · announce · proof - Written-on-the-Wall conjecture 698 — proved · spectral graph theory · open decades — Devin proved
s⁻(G) ≤ R(G)(Rayleigh + Cauchy–Schwarz + AM–GM), crediting 1993 ingredient lemmas; Lean 4. Verify: Lean 4, independent. 2026-07-23 · announce · proof - Graffiti conjecture 154 — refuted · spectral graph theory · open ~40 yr — Devin refuted it with a lollipop(50,70) graph (n=120), Lean 4 — but scooped: demonstrandum-research published the same witness 6 weeks earlier. Verify: Lean 4, scooped. 2026-07-23 · announce · priority
- Graffiti conjecture 143 — refuted · spectral graph theory · open ~40 yr — refuted with a dumbbell graph (exact-arithmetic verifier; Lean left partial for irrational eigenvalues); also scooped by demonstrandum-research (Devin). Verify: independent, scooped. 2026-07-23 · priority
- Černý conjecture — positive-level one-cluster automata — proved · automata / combinatorics · open (special case) — reset-length bound proved via a linear-algebra argument from OpenAI Codex (GPT-5.6 Sol), author-verified (Yinfeng Zhu). Verify: arXiv, author-verified. 2026-07-23 · arXiv:2607.19675
- (9,6,1)-perfect Mendelsohn design — nonexistence · design theory · smallest open case — Devin proved it doesn't exist three independent ways (kissat/DRAT, CP-SAT, exhaustive DFS); LRAT checked inside Lean. Verify: DRAT, Lean 4, independent. 2026-07-22 · announce · solution
- BTD(14,18; 7,1,9; 7,4) — nonexistence · design theory · survived CPro1 — Devin proved nonexistence, DRAT proof
s VERIFIED+ independent CP-SAT. Verify: DRAT, independent. 2026-07-22 · solution - BTD(12,15; 6,2,10; 8,6) — nonexistence · design theory · survived CPro1 — Devin proved nonexistence, DRAT-certified + independent CP-SAT. Verify: DRAT, independent. 2026-07-22 · solution
- BTD(12,20; 4,3,10; 6,4) — nonexistence · design theory · survived CPro1 — Devin proved nonexistence with two independent CP-SAT models + DRAT proof. Verify: DRAT, independent. 2026-07-22 · solution
- Erdős problem #390 — proved (claimed) · number theory · decades open — GPT-5.6 Sol (Shouqiao Wang): asymptotic f(n)−2n ∼ c·n log n for factoring n! into consecutive integers. Verify: author + AI, under review. 2026-07-22 · thread · paper
- Erdős problem #486 — proved (claimed) · number theory / combinatorics · long-open — GPT-5.6 Sol (Wang), with a Lean 4 formalization. Verify: Lean (author), under review. 2026-07-22 · folder
- Erdős problem #536 — proved (claimed) · number theory / combinatorics · long-open — GPT-5.6 Sol (Wang). Verify: author + AI, under review. 2026-07-22 · folder
- Erdős problem #788 — proved (claimed) · number theory · decades open — GPT-5.6 Sol (Wang): f(n) = n^(1/2+o(1)) for sumset-avoiding subsets, with a complete Lean formalization. Verify: Lean (author, machine-checked per repo), under review. 2026-07-22 · paper
- Erdős problem #1002 — proved (claimed) · number theory / combinatorics · long-open — GPT-5.6 Sol (Wang). Verify: author + AI, under review. 2026-07-22 · folder
- Erdős problem #1038 — proved (claimed) · number theory / combinatorics · long-open — GPT-5.6 Sol (Wang), with a large (3,000+ file) Lean project. Verify: Lean (author), under review. 2026-07-22 · folder
- Dinitz–Garg–Goemans conjecture — refuted · combinatorial optimization / flows · open ~30 yr — GPT-5.6 Pro found a graph where fractional flow costs 58 but any bounded-violation unsplittable flow costs ≥60 (Dmitry Rybin). Verify: author-only. 2026-07-22 · announce · chat
- Balabdaoui–Wellner conjecture — proved · probability / statistics · open since 2014 — strong log-concavity of the Chernoff density, with the entire proof reportedly generated by GPT-5.6 Sol (Xianyang Zhang, Quan Zhou). Verify: arXiv. 2026-07-22 · arXiv:2607.18619
- mod-4 Kawauchi conjecture — proved · knot theory · open (mod-4 case) — Conway polynomials of amphicheiral knots; Claude Fable 5 proposed the strategy and drafted the proof, author-verified (Jim Conant). Verify: arXiv, author-verified. 2026-07-22 · arXiv:2607.18655
- Spectral edge of the quartic SYK model — proved · mathematical physics · open aspects — theorem established with substantial help from GPT-5.6 (Yukun He). Verify: arXiv. 2026-07-22 · arXiv:2607.18998
- Gaussian Moments conjecture — refuted · algebra (Jacobian-adjacent) · open — explicit low-degree counterexamples for all n ≥ 3, prompted by the Jacobian result, via ChatGPT + Claude (Christopher D. Long). Verify: arXiv. 2026-07-21 · post · arXiv:2607.18186
- Jacobian Conjecture (n = 3) — claimed refutation, not yet confirmed · algebraic geometry · open since 1939 — Fable (Anthropic) posted an explicit cubic map of ℂ³ with constant Jacobian det −2 that sends three distinct points to one (Levent Alpöge). The spark of the wave; being scrutinized (not endorsed) by Tao and the Secret Blogging Seminar — an extraordinary claim for a conjecture this old. Verify: author-only, under review. 2026-07-20 · announce
Related but not counted as resolved: WoW 129 (still open, exhaustive only to n = 11 — see 698 page); BTD(14,28; 8,3,14; 7,6) (undecided after ~19 h — see BTD page); Aaronson–Arkhipov anticoncentration (AI-assisted human proof, Simon Coste, arXiv:2607.20329); improved stochastic multi-gradient descent convergence (thin sourcing).
Have one to add? See CONTRIBUTING.
- 2026-06-12 — demonstrandum-research publishes verified Graffiti refutations (incl. 154/143) on GitHub/Zenodo. Barely noticed.
- 2026-07-20 — Alpöge posts the Jacobian Conjecture counterexample ("close friend fable"). It goes viral; Tao and the Secret Blogging Seminar dig in.
- 2026-07-22 — Rybin posts the Dinitz–Garg–Goemans counterexample (GPT-5.6 Pro).
- 2026-07-23 — the Devin/jzone3 pipeline announces a batch (Brandt, Graffiti 39/40/154, WoW 698, design nonexistence); Capy refutes Graffiti 284 in 8 minutes; Musk amplifies. The 154 priority correction lands the same day.
The July 2026 wave is exciting and noisy. A few things to keep in mind:
- Checkable ≠ peer-reviewed. A
verify.pyor a Lean proof certifies a specific formal statement. Whether that statement faithfully captures the conjecture (vs. a paraphrase) is a separate, human question. The best efforts here check it explicitly. - Refuting is easier than proving. Most wave results are counterexamples or nonexistence — a single small witness or an UNSAT certificate. That's real, and also why the pace looks fast.
- Priority is hard on the open web. Graffiti 154 had already been refuted six weeks earlier in a Zenodo artifact invisible to journal search. Assume some "firsts" will be relabeled as rediscoveries.
- Credit the ingredients. Several "proofs" chain known lemmas in a new way; the honest entries credit those lemmas rather than claiming them.
- Extraordinary claims (hi, Jacobian) stay in the "under review" column until the expert discussion settles, no matter how clean the arithmetic.
Verification badges describe what checking exists, sourced from the authors and third parties — they are not a certification by this repository.
New entries welcome — especially with a link to a checkable certificate. See CONTRIBUTING.md for the entry template and the sourcing bar.
This is a curated index of public claims by third parties, compiled from X/Twitter posts, public repositories, and preprints. Links point to live third-party content that may change or be corrected. Attributions and affiliations are as reported at the time of writing. Nothing here is a mathematical endorsement. Corrections are welcome via issue or PR.
CC0-1.0 — public domain. The linked works belong to their respective authors.