# Cross-Reference Dossier: Ten Famous Unsolved Problems — One-Week AI Team Choice (October 2026)

## Summary

**Read this first — the list of "ten unsolved problems" contains two traps and one earthquake.**

1. **Two of the ten are not open at all.** The Banach–Tarski "paradox" is a *proven theorem* (1924). The Continuum Hypothesis is *provably undecidable in ZFC* (Gödel 1940 + Cohen 1963). Any team that spends its week "attacking" them as open problems has wasted it — but precisely because their proofs exist and have even been machine-formalized, they offer the *highest* guaranteed verifiable output of the ten.
2. **The other eight are genuinely open**, including all six remaining Millennium problems on the list (Riemann, BSD, P vs NP, Navier–Stokes, Yang–Mills — five of the six; the sixth, Hodge, is not on the list). Of the seven Millennium problems, only Poincaré has been *officially* declared solved by Clay. Source: Millennium Prize Problems overview, read 2026-10-21, https://en.wikipedia.org/wiki/Millennium_Prize_Problems
3. **The earthquake (Sept–Oct 2026, all unreviewed):** On 8 Sept 2026 OpenAI announced a Lean-formalized finite-time blowup proof for *forced* 3D Navier–Stokes, claiming Clay alternatives C and D; on 11 Sept Clay said the problem has "apparently been settled" while stressing its evaluation is "deliberately unhurried" and awarding no prize. On 6 Oct 2026 OpenAI released 722 AI-generated manuscripts (372 families), headlined by a claimed "quasi-Riemann hypothesis" (no zeros with Re s > 7/8 for all Dirichlet L-functions); three manuscripts were withdrawn on 7 Oct after a sign error. In Aug–Sept 2026 the 12-year-old bounded-prime-gap record of 246 was challenged by a cascade of unreviewed claims (240, 240, 236, 212, 186). **None of these 2026 claims has completed peer review or independent verification as of 21 Oct 2026.** This dossier reports the peer-reviewed record as the baseline and the 2026 claims separately, labelled as claims, throughout.
4. **Bottom line for the choice:** ranked by realistic one-week *verifiable* output for 20 AI text-and-mathematics agents with web access and no serious compute cluster, the order is: **1 Banach–Tarski, 2 Continuum Hypothesis, 3 Collatz, 4 Goldbach, 5 Twin Primes/Bounded Gaps, 6 BSD, 7 Riemann, 8 P vs NP, 9 Navier–Stokes, 10 Yang–Mills** (full table with one-line justifications at the end). The top four are the only ones where a named theorem can plausibly be *formalized or computationally certified from scratch* inside seven days.

**Confidence key:** *Established* = peer-reviewed / institutionally accepted. *Claimed 2026* = public manuscript/Lean artifact, no peer review yet. Several 2026 items rest on trade-press and secondary reporting (IEEE Spectrum, Scientific American, Science) rather than refereed papers; that is flagged where it matters.

---

## Findings

### 1. Riemann Hypothesis

#### (1) True current status
**OPEN — established.** All nontrivial zeros of ζ(s) conjectured on Re s = 1/2; no proof or counterexample is accepted. The Sept–Oct 2026 AI claims do *not* include a proof of RH itself: OpenAI's own catalogue and independent exposition state explicitly "It does not prove the Riemann hypothesis" — the claim is the weaker quasi-RH zero-free half-plane below. Sources: exposition status chapter, read 2026-10-21, https://judegomila.com/posts/quasi-riemann-hypothesis ; catalogue summary, read 2026-10-21, https://cellcog.ai/blog/openai-math-results/

#### (2) Strongest known partial results / records
- **De Bruijn–Newman constant Λ** (RH ⟺ Λ ≤ 0): Rodgers–Tao (2018) proved Λ ≥ 0, so RH, if true, is "barely true." Polymath 15 (2019) proved Λ ≤ 0.22. Platt–Trudgian (2020/21) improved this to **Λ ≤ 0.2 — the peer-reviewed record**. Sources: Polymath 15, arXiv, read 2026-10-21, https://arxiv.org/abs/1904.12438v1 ; bound history, read 2026-10-21, https://en.wikipedia.org/wiki/De_Bruijn%E2%80%93Newman_constant
- **Zero verification height:** Platt–Trudgian rigorously verified RH for all zeros with |Im s| ≤ **3×10¹²** (over 12.3×10¹² zeros). Source: "The Riemann hypothesis is true up to 3·10¹²", arXiv, read 2026-10-21, https://arxiv.org/pdf/2004.09765
- **Zero-density breakthrough (established):** Guth–Maynard (2024; *Annals of Mathematics* 203 (2026), 623–675) gave the first substantial improvement since 1940 near σ = 3/4: N(σ,T) ≤ T^{30(1−σ)/13+o(1)}, plus primes in short intervals of length x^{17/30+o(1)}. Sources: read 2026-10-21, https://annals.math.princeton.edu/2026/203-2/p06 ; https://arxiv.org/pdf/2405.20552
- **Claimed 2026 (unreviewed):** (i) Λ ≤ 0.1787854, a computer-assisted preprint by Gomila instantiating Polymath 15's criterion at the existing 3×10¹² height — a preprint claim, *not* the peer-reviewed record (its own text calls Λ ≤ 0.2 "the relevant peer-reviewed benchmark"). Source: read 2026-10-21, https://raw.githubusercontent.com/judegomila/dbn-lambda-01787854-candidate-audit/a74738deb6d5e0f76887cb36901da08b68dca705/gomila_dbn_lambda_01787854_release.pdf (ii) **Quasi-RH (OpenAI, paper dated 30 Sept 2026, released 6 Oct):** no zeros with Re s > 7/8 for ζ and *every* Dirichlet L-function (uniform in modulus and height), which would also exclude Landau–Siegel zeros; a shorter human-edited companion proves 11/12 instead. A Lean formalization of the 7/8 statement for ζ (against Mathlib's own `riemannZeta`) is in the release as a comparator challenge. Status per the exposition itself: "As of October 2026 neither paper has been peer reviewed"; experts (Lichtman, Radziwiłł) have reconstructed the shorter argument and call it potentially the most significant AI-for-math result so far, while Sarnak "will not call it a theorem until humans check every detail." Sources: read 2026-10-21, https://judegomila.com/posts/quasi-riemann-hypothesis ; https://www.aieon.ee/eng/2026/10/openai-quasi-riemann-hypothesis-proof-unpacked-by-lichtman-and-radziwill/

#### (3) Formalization state
**Best-in-class infrastructure, no proof of RH.** Mathlib now contains: the definition `riemannZeta`, ζ(2) = π²/6, the Euler product, the functional equation, ζ(s) ≠ 0 for Re s ≥ 1, a formal *statement* `RiemannHypothesis`, and Dirichlet's theorem on primes in arithmetic progressions (Loeffler–Stoll, *Annals of Formalized Mathematics*). The PrimeNumberTheoremAnd (PNT+) project (Kontorovich–Tao) has formalized the Prime Number Theorem in Lean (Wiener–Ikehara route, with stronger-error-term work continuing). Sources: read 2026-10-21, https://arxiv.org/html/2503.00959v3 ; https://AlexKontorovich.github.io/PrimeNumberTheoremAnd/blueprint.pdf

#### (4) Week-tractability verdict
- **Plausible artifact:** a source-cited audit dossier on the quasi-RH claim (statement-matching the Lean comparator theorem against the paper, dependency map of the 11/12 argument), *or* a Lean formalization of a classical named partial result not yet in Mathlib (e.g., a zero-free region with explicit constants, building on PNT+). Both are checkable.
- **Flatly impossible:** proving RH; improving Λ below 0.2 (requires Platt-scale interval-arithmetic computation — a cluster job); independently re-verifying zeros to 3×10¹².

---

### 2. Collatz Conjecture

#### (1) True current status
**OPEN — established.** Every orbit is conjectured to reach 1; no proof, no counterexample, no prize-grade progress in 2025–26. Tao's own framing: upgrading "almost all" to "all" is "likely to be almost as hard as the full Collatz conjecture."

#### (2) Strongest known partial results
- **Computational verification (record):** Barina (2025, *The Journal of Supercomputing* 81:810, doi 10.1007/s11227-025-07337-0) verified convergence for all n < **2⁷¹ ≈ 2.36×10²¹**, using GPU algorithms (1,335× speedup) distributed over European supercomputers, finding four new path records. Source: journal PDF via Brno UT, read 2026-10-21, https://www.vut.cz/www_base/vav_priloha.php?vavID=197809&prilohaID=298514
- **Strongest theoretical result:** Tao (2019; *Forum of Mathematics, Pi* 10:e12, 2022): for *any* f(N) → ∞, Col_min(N) ≤ f(N) for **almost all** N in the sense of logarithmic density — i.e., almost every orbit attains almost bounded values. Source: read 2026-10-21, https://www.cambridge.org/core/services/aop-cambridge-core/content/view/1008CC2DF91AF87F66D190C5E01C907F/S2050508622000087a.pdf/div-class-title-almost-all-orbits-of-the-collatz-map-attain-almost-bounded-values-div.pdf
- Supporting structure: Terras (almost all n have finite stopping time), Krasikov–Lagarias (≥ x^0.84 of integers ≤ x reach 1), Eliahou-type lower bounds excluding nontrivial cycles below enormous periods (best cycle-length bound ≈ 2.18×10¹¹ in shortcut form, as of 2025). Source: read 2026-10-21, https://en.wikipedia.org/wiki/Collatz_conjecture

#### (3) Formalization state
**Statement-level only in the large libraries.** Google DeepMind's FormalConjectures repository contains a Lean statement (`CollatzConjecture.lean`); Mathlib has no Collatz theory of substance. Small verified fragments exist outside Mathlib (e.g., an Oct 2026 Lean formalization, via AxiomProver, of Mazur's positive-density result — at least a positive proportion of n reach 1 in ≤ 10.46 log n steps — showing the *kind* of fragment that is formalizable). Sources: read 2026-10-21, https://deepwiki.com/google-deepmind/formal-conjectures/3.1-wikipedia-conjectures ; https://hexagonmath.org/2610.00249v1

#### (4) Week-tractability verdict
- **Plausible artifact (one of the best on this list):** (a) an original, reproducible verification codebase (optimized sieve/stopping-time algorithm in e.g. Rust/Python with BigInt fallbacks) certifying a *named finite range* (e.g., all n < 2⁴⁰ in roughly minutes-to-hours of ordinary CPU time, with published checksums and path records) — honestly framed as re-verification, not a record attempt; plus (b) a Lean formalization of a named elementary partial result (e.g., no cycles of a specified small type, or convergence for a complete residue-class family mod 2^k).
- **Flatly impossible:** beating 2⁷¹ (supercomputer-scale); formalizing Tao 2019 (56 pages of 3-adic/renewal-process analysis); proving the conjecture.

---

### 3. Goldbach Conjectures (Strong & Weak)

#### (1) True current status
**Strong Goldbach: OPEN. Weak (ternary) Goldbach: PROVEN** (Helfgott 2013, with a publication caveat below). Every even n > 2 = p + q remains conjectural; every odd n > 5 = p + q + r is a theorem. Sources: read 2026-10-21, https://en.wikipedia.org/wiki/Goldbach's_conjecture

#### (2) Strongest known partial results
- **Verification bound (record):** Oliveira e Silva, Herzog & Pardi (*Mathematics of Computation* 83, 2014) verified strong Goldbach for all n ≤ **4×10¹⁸** (double-checked to 4×10¹⁷) by distributed computation. Source: as cited in https://en.wikipedia.org/wiki/Goldbach's_conjecture (read 2026-10-21).
- **Helfgott's proof of weak Goldbach (2013):** circle method for large odds (beyond ≈10³⁰) + computer verification below; accepted for the *Annals of Mathematics Studies* series in 2015 and **widely accepted by the community, but as of the sources consulted it has still not appeared in final journal/book form**, Helfgott having undertaken major referee-suggested revisions — report it as "accepted as true; publication still pending," not as a settled bibliographic fact. Immediate corollary: every even n ≥ 4 is a sum of at most 4 primes. Sources: read 2026-10-21, https://en.wikipedia.org/wiki/Goldbach_conjecture ; https://old.maa.org/press/maa-reviews/goldbachs-problem
- **Chen's theorem (1973), the closest sieve result to strong Goldbach:** every sufficiently large even number is p + (prime or semiprime) — the famous "1+2." Source: read 2026-10-21, https://en.wikipedia.org/wiki/Chen%27s_theorem
- Also: Montgomery–Vaughan — Goldbach exceptions below N number O(N^{1−c}) (density zero).

#### (3) Formalization state
**Thin.** A Lean *statement* of Goldbach exists in statement collections/FormalQualBench-style stubs (including a stub for Helfgott's ternary theorem as a target, not a proof). Finite-range checks have been done in Lean as exercises (sorry-free Goldbach to 2×10⁵ was demonstrated in Lean 3 by Mehta, per the Lean Zulip archive). No formalization of Chen, Helfgott, or the 4×10¹⁸ verification exists. A widely circulated 2023 "Lean proof of Goldbach" note (Vega) was publicly refuted on Zulip (its key inequality is false for n > 7000) — a cautionary example for the team. Sources: read 2026-10-21, https://deepwiki.com/math-inc/FormalQualBench/3.3-number-theory-and-additive-combinatorics ; https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Checking.20the.20Goldbach.20conjecture.html

#### (4) Week-tractability verdict
- **Plausible artifact:** a reproducible segmented-sieve verifier with independently checkable certificates pushing a *clean-room* verification to ~10¹¹–10¹² on commodity hardware (well short of 4×10¹⁸, but fully reproducible — unlike the record), paired with a Lean proof of Goldbach up to a modest bound via verified computation, and a rigorous synthesis of Helfgott's proof architecture.
- **Flatly impossible:** any new theoretical progress on strong Goldbach; formalizing Chen or Helfgott (hundreds of pages of sieve/circle method); re-running 4×10¹⁸.

---

### 4. Twin Prime Conjecture / Bounded Gaps

#### (1) True current status
**Twin prime conjecture: OPEN** (infinitely many p with p+2 prime). The *bounded gaps* theorem (some finite gap recurs infinitely often) is proven. Note the mission's requested values (246; 6 under generalized Elliott–Halberstam) are the **established** record — but see the unreviewed Aug–Sept 2026 cascade below, which the team must not present as established.

#### (2) Strongest known partial results
- **Established chain:** Zhang (2013) H₁ ≤ 70,000,000 → Polymath 8a ≤ 4,680 → Maynard (2013, independently Tao) ≤ 600 → **Polymath 8b (2014): H₁ ≤ 246 unconditionally**. Sources: Polymath retrospective, read 2026-10-21, https://arxiv.org/pdf/1409.8361 ; https://sugaku.net/oa/W1576273050/
- **Conditional:** assuming Elliott–Halberstam, H₁ ≤ 12; assuming the *generalized* Elliott–Halberstam conjecture, **H₁ ≤ 6** — and 6 is provably the limit of pure sieve methods (parity barrier). Sources: same as above; summary read 2026-10-21, https://en.wikipedia.org/wiki/Prime_gap
- **Claimed Aug–Sept 2026 (NONE peer-reviewed; established bound remains 246):** an AI-found argument presented by Hanxin Zhang claiming 240 (28 Aug); Julia Stadlmann's human preprint (arXiv:2608.31126) proving H₁ ≤ 240 by combining Bombieri–Vinogradov with newer smooth-moduli equidistribution — the most conventionally credible of the claims; Kintali 236 (1 Sept); Axiom Math 212 (3 Sept); OpenAI GPT-6 Astra 186 (2 Sept; paper + Lean formalization *with explicit assumptions* + a Python-FLINT numerical certificate). Sources: read 2026-10-21, https://arxiv.org/html/2608.31126v1 ; https://en.wikipedia.org/wiki/Prime_gap ("As of September 2026, none of those claims has been peer-reviewed, leaving the established bound at 246"); https://traictory.com/news/2026-10-03-prime-gaps-186-explained

#### (3) Formalization state
**Transformed in Aug 2026.** Axiom Math's AxiomProver published **PrimeGapsLib (17 Aug 2026): a machine-checked Lean 4 formalization of Maynard 2013 + the Polymath 8b tightening to 246** (and of Maynard's 600), built on Mathlib + PrimeNumberTheoremAnd, assuming only the Bombieri–Vinogradov theorem, with a public comparator challenge for independent checking (full check takes hours). Reported first by IEEE Spectrum. Before this, bounded gaps had no Lean formalization at all. Sources: read 2026-10-21, https://spectrum.ieee.org/axiom-math-246-theorem-formalization ; https://primegaps.axiommath.ai/blueprint.pdf ; https://www.unite.ai/axiom-maths-ai-verifies-the-246-prime-gaps-theorem-in-lean/

#### (4) Week-tractability verdict
- **Plausible artifact:** an independent audit of PrimeGapsLib's comparator statement (does the formalized theorem match Polymath 8b's?), a reproducible verification of the admissible-tuple + sieve-weight numerical certificates behind the claimed 240/212/186 bounds (finite, checkable computations), and a source-cited adjudication of the Aug–Sept cascade. This is genuinely useful, week-sized, and verifiable.
- **Flatly impossible:** formalizing Maynard–Tao from scratch (Axiom's effort was a 41-contributor project); proving gap 2, 4, or 6 unconditionally (no conditional route exists even under EH for 2 or 4); any new sieve bound by hand in a week.

---

### 5. Birch and Swinnerton-Dyer Conjecture

#### (1) True current status
**OPEN in general — established.** BSD (rank E(Q) = ord_{s=1} L(E,s), plus the leading-coefficient formula with Sha, regulator, Tamagawa numbers) is proven only for analytic rank ≤ 1. The full formula (finiteness and exact order of Sha) is open even in many rank-0/1 cases beyond the p-parts proven by recent work.

#### (2) Strongest known partial results
- **Rank 0:** Coates–Wiles (1977, CM curves: L(E,1) ≠ 0 ⇒ E(Q) finite); extended via modularity + Kolyvagin to all E/Q.
- **Rank 0 and 1 (the headline theorem):** Gross–Zagier (1986, Heegner-point height = L′(E,1)) + Kolyvagin (1990, Euler systems) + Rubin (CM cases) ⇒ if ord_{s=1} L(E,s) ≤ 1 then rank E(Q) equals that order and **Sha is finite**. With the modularity theorem this now covers *every* E over Q. Sources: read 2026-10-21, https://arxiv.org/html/2506.03465v2 ; https://ncatlab.org/nlab/revision/Birch+and+Swinnerton-Dyer+conjecture/7
- **Rank ≥ 2:** no general theorem; progress is via p-converse theorems (Burungale–Skinner–Tian–Wan and successors) and Iwasawa theory. A 2026 ANTS XVII paper algorithmically identified **36,687 curves** in LMFDB that admit infinite families of quadratic twists satisfying full BSD unconditionally. Source: read 2026-10-21, https://arxiv.org/pdf/2601.16044
- **Computational data (LMFDB):** complete tables for all **3,064,705 elliptic curves over Q of conductor < 500,000**, with ranks/generators computed by Cremona's eclib/mwrank and Heegner-point methods; analytic ranks computed with rigorous interval arithmetic in related datasets (analytic rank is rigorously an *upper* bound issue for rank ≥ 2 — vanishing of derivatives cannot be certified numerically). Sources: read 2026-10-21, https://lmfdb.org/EllipticCurve/Q/Source ; https://antsmath.org/ANTSXVII/papers/antsxvii-banwait_huang-paper.pdf
- Record algebraic rank: Elkies' rank-28 curve (2006, expected rank; at least 28 independent points) remains the famous benchmark — no rank ≥ 29 example is established.

#### (3) Formalization state
**Foundations yes, BSD no.** Mathlib has a complete Weierstrass-curve development: nonsingular points with a proven abelian group law in affine, projective and Jacobian coordinates. It has **no** L-function of an elliptic curve, no analytic rank, no Sha, and no BSD statement/theorem; the Dirichlet-L-function machinery (Loeffler–Stoll) is the nearest infrastructure. Sources: read 2026-10-21, https://Leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.html

#### (4) Week-tractability verdict
- **Plausible artifact:** a reproducible data audit: using LMFDB/PARI-style computation, verify rank = analytic rank and the BSD leading-coefficient identity (to stated precision, with error bounds) for *every* curve below a chosen conductor bound (e.g., N ≤ 10,000) and publish the code + discrepancy log (expected: zero discrepancies, with Sha values as predicted squares). Also feasible: Lean computation of explicit group-law/rank-0 torsion examples on named curves using Mathlib's group law.
- **Flatly impossible:** any rank ≥ 2 theorem; formalizing Gross–Zagier or Kolyvagin (each is a monograph); defining L(E,s) in Lean from scratch in a week.

---

### 6. P vs NP

#### (1) True current status
**OPEN — established.** No accepted proof either way; Clay problem. There is no "record bound" culture comparable to the other problems — the strongest knowledge is *negative metaknowledge*: the barrier theorems below, plus circuit lower bounds that remain exponentially far from what P ≠ NP needs (best known explicit circuit lower bounds are only slightly superlinear, ~3n-ish, for general circuits).

#### (2) Barriers any proof must clear
- **Relativization (Baker–Gill–Solovay, 1975):** there are oracles A, B with P^A = NP^A and P^B ≠ NP^B; hence no oracle-insensitive technique (classical diagonalization) can settle it. A proof must be *non-relativizing*.
- **Natural proofs (Razborov–Rudich, 1997):** if strong pseudorandom generators / one-way functions exist, no "natural" circuit lower-bound proof (constructive + large property) can separate P from NP — and all classic circuit lower bounds are natural. A proof must be *non-naturalizing* (or refute standard cryptography).
- **Algebrization (Aaronson–Wigderson, 2008):** relativization's strengthening — techniques that work relative to low-degree algebraic extensions of oracles (which includes the arithmetization behind IP = PSPACE and the PCP theorem) also cannot settle it. A proof must be simultaneously non-relativizing, non-naturalizing, and non-algebrizing.
Sources: Aaronson–Wigderson paper, read 2026-10-21, https://www.zanotowane.pl/1131/4086/ ; barrier survey summary, read 2026-10-21, https://en.wikipedia.org/wiki/P_and_NP
- Note: the barriers are *not* independence results — P vs NP is not known to be independent of ZFC, and the barriers leave open e.g. Williams-style algorithms-to-lower-bounds and geometric complexity theory routes.

#### (3) Formalization state
**The problem's surroundings are formalized — in Isabelle, not Lean.** The Isabelle Archive of Formal Proofs contains a complete formalization of the **Cook–Levin theorem** (SAT is NP-complete), including multi-tape Turing machines and definitions of P and NP. Lean/Mathlib has Turing-machine basics but no comparable complexity-classes library and no Cook–Levin; FormalConjectures-style statement stubs for P vs NP exist. Source: read 2026-10-21, https://isa-afp.org/entries/Cook_Levin.html

#### (4) Week-tractability verdict
- **Plausible artifact:** a rigorous, source-cited barrier synthesis *plus* one small formalized fragment — e.g., in Lean or Isabelle, the easy direction of Baker–Gill–Solovay (an oracle relative to which P = NP, via an EXP-complete oracle) at the level of definitions and the core diagonalization/counting lemma, with an explicit statement of what remains unformalized. An axiom-analysis ("what would a proof have to violate?") is also deliverable.
- **Flatly impossible:** any separation or collapse; formalizing Razborov–Rudich in full; beating the ~3n circuit lower-bound frontier.

---

### 7. Navier–Stokes Existence and Smoothness

#### (1) True current status
**CONTESTED — read carefully.** *Established position until Sept 2026:* open; neither global regularity nor blowup known for 3D. *Claimed 8 Sept 2026:* OpenAI announced a proof of finite-time blowup for solutions **driven by a smooth external force**, i.e., breakdown alternatives **C** (on R³) and **D** (periodic) in Fefferman's official Clay formulation — any *one* of A–D resolves the Clay problem as posed. Clay's 11 Sept 2026 statement said the problem has "apparently been settled" and that evaluation/credit assignment "is deliberately unhurried"; **no prize has been awarded, no independent verification has been completed, and Clay's prize rules require qualifying publication + at least two years + general acceptance.** Crucially, even if the claim is fully correct, the *unforced* alternatives A/B — the question most researchers mean by "the Navier–Stokes problem" — remain **undecided**: C is not the negation of A, because C permits a chosen smooth force. A priority dispute (Buckmaster–Alpöge, who released Lean-formalized Euler/Boussinesq blowup work in Aug 2026 and accuse OpenAI of front-running; OpenAI denies using their data) and a method dispute (experts say the claimed resemblance to the Córdoba–Martínez-Zoroa program is superficial) are both unresolved. Sources: status synthesis with primary-source links, read 2026-10-21, https://navier-stokes.org/navier-stokes-problem-solved/ ; https://www.scientificamerican.com/article/openais-blockbuster-navier-stokes-proof-isnt-what-we-thought-it-was/?utm_campaign=sprinklr&utm_medium=social&utm_source=x ; Science (AAAS) controversy report, read 2026-10-21, https://bpb-us-w2.wpmucdn.com/wp.wpi.edu/dist/a/409/files/2026/09/Science_2026_How-an-AI-math-breakthrough-ignited-a-controversy.pdf ; Clay status note, read 2026-10-21, https://en.wikipedia.org/wiki/Millennium_Prize_Problems

#### (2) Key partial results and 2024–2026 developments
- **Leray (1934):** global-in-time weak solutions exist for all finite-energy data, satisfying the energy inequality; uniqueness and smoothness in this class open (for f = 0).
- **2D is settled:** global smooth existence/uniqueness (Ladyzhenskaya).
- **Caffarelli–Kohn–Nirenberg (1982):** partial regularity for suitable weak solutions — the singular set has **zero 1-dimensional parabolic Hausdorff measure**, P¹(S) = 0; still the strongest general regularity statement.
- **Regularity criteria:** Beale–Kato–Majda-type and Prodi–Serrin–Ladyzhenskaya criteria — blowup at T* forces blowup of specific scale-critical norms (e.g., ∫‖ω‖∞ dt); Tao (2016) proved blowup for an *averaged* NS with the same energy/scaling structure, a barrier showing energy+scaling arguments alone cannot prove regularity. Buckmaster–Vicol (2019): non-uniqueness of wild weak solutions outside the Leray–Hopf class; Albritton–Brué–Colombo (2022): non-uniqueness of *forced* Leray–Hopf solutions.
Source for the classical list: read 2026-10-21, https://navier-stokes.org/progress/
- **AI-assisted work (established, 2025):** DeepMind + collaborators (Wang et al., 18 Sept 2025) used physics-informed neural networks at near-machine precision to discover **new families of unstable singularities for three simpler fluid equations (IPM, Boussinesq, and Euler-type models)** — explicitly *not* a Navier–Stokes blowup; the same blog notes finding any NS singularity is a still-unsolved Millennium problem. Scientific American further reports (i) the related Gómez-Serrano team's axisymmetric Euler-with-boundary blowup *candidate* would take years to prove, and (ii) a Feb 2026 preprint showing axisymmetric Euler blowups of that type **do not carry over** to Navier–Stokes (viscosity kills them). Sources: read 2026-10-21, https://deepmind.google/blog/discovering-new-solutions-to-century-old-problems-in-fluid-dynamics/ ; https://www.scientificamerican.com/article/humans-and-ai-race-to-blow-up-maths-toughest-equations/
- **The Sept 2026 claim's artifacts:** a 166-page manuscript ("Finite Time Blowup for Navier–Stokes": for every ν > 0, smooth compactly-supported-in-time force, u₀ = 0, solution on [0,1) with bounded L² energy but lim sup ‖u(t)‖∞ = ∞) and a Lean repository reporting **zero `sorry`, only the standard axioms, review status "self-assessed,"** with its C/D reference statements taken from the FormalConjectures project; produced, per OpenAI, by ~10,000 agents in ~88 h (+17 h formalization). Independent tasks still outstanding per the status site: building the Lean project, axiom audit, and statement-matching against Fefferman's text. Source: read 2026-10-21, https://navier-stokes.org/navier-stokes-problem-solved/

#### (3) Formalization state
Mathlib has essentially **no** Navier–Stokes theory (no Leray, no CKN; PDE infrastructure is far from sufficient). The only substantial NS formalizations in existence as of Oct 2026 are the contested Sept 2026 artifacts: OpenAI's claimed C/D formalization and Buckmaster–Alpöge's Euler/Boussinesq formalizations — both self-assessed, neither independently audited in the sources consulted. FormalConjectures supplies the reference *statements* of A–D that OpenAI's repo used.

#### (4) Week-tractability verdict
- **Plausible artifact:** a statement-matching audit — a clause-by-clause concordance between Fefferman's C/D (decay conditions on f, energy class, periodicity) and (i) the 166-page manuscript's Theorem 1.1/Corollary 10.6 and (ii) the Lean declarations, with every gap flagged; plus a source-cited state-of-the-art synthesis separating forced from unforced. This is high-value and exactly text-agent-shaped. (Actually *building* the large Lean project may exceed a no-cluster week's compute.)
- **Flatly impossible:** proving A/B or unforced blowup; formalizing Leray or CKN in Lean; reproducing DeepMind-grade PINN singularity searches (serious compute); certifying or refuting the 166-page proof in seven days.

---

### 8. Yang–Mills Existence and Mass Gap

#### (1) True current status
**OPEN — established.** No construction of 4D quantum Yang–Mills meeting Clay's standard exists; the many 2025–26 self-published "complete proofs" (Zenodo, PhilArchive, Academia.edu) have no institutional recognition, and Clay continues to list the problem as unsolved. Source: status discussion, read 2026-10-21, https://mail.smonad.com/problems/yang-mills.html

#### (2) What a Clay-standard solution requires; lattice evidence
- **The requirement (Jaffe–Witten official description):** for *every* compact simple gauge group G, construct a **nontrivial** quantum Yang–Mills theory on R⁴ satisfying axioms "at least as strong as" the **Wightman / Osterwalder–Schrader axioms** (Euclidean invariance, reflection positivity, regularity/clustering), and prove the Hamiltonian has a **mass gap Δ > 0**: spectrum(H) ⊆ {0} ∪ [Δ, ∞), with 0 a simple eigenvalue (unique vacuum). Reflection positivity + OS reconstruction is what turns a Euclidean measure into a Hilbert space, unitary dynamics and a self-adjoint H; exponential clustering of correlators is equivalent to the gap. Source: official-statement summary, read 2026-10-21, https://seoulinside.substack.com/p/yang-mills-theory-archive
- **Why it's hard:** constructive QFT succeeded in 2D and 3D (Glimm–Jaffe program) but the 4D continuum limit — controlling the lattice theory uniformly as spacing a → 0 at *weak* coupling (asymptotic freedom regime), proving nontriviality (non-Gaussian limit) and a uniform gap — has resisted the renormalization-group program (Balaban's work remains incomplete/unaccepted as a full solution).
- **Lattice evidence (strong, numerical, non-rigorous):** decades of lattice gauge theory give exponential decay of correlators, an area law for Wilson loops (confinement), and a glueball spectrum whose lightest state (0⁺⁺) sits at ≈ **1.5–1.7 GeV** for pure SU(3) — i.e., physicists regard the gap as experimentally/numerically certain; what is missing is the continuum-limit *proof*. Source: lattice review summary, read 2026-10-21, https://www.academia.edu/165430749/Mass_Gap_Color_Screening_and_Strong_Coupling_from_Lattice_Geometry

#### (3) Formalization state
**Effectively zero.** Mathlib contains Lie groups, connections and differential geometry, but no quantum field theory, no OS axioms, no lattice Yang–Mills, and no formal statement of the Clay problem with mathematical content. There is no comparable-library milestone analogous to Flypitch (CH) or AFP Cook–Levin (P vs NP).

#### (4) Week-tractability verdict
- **Plausible artifact:** only a synthesis: a rigorous, source-cited "what would count" dossier (OS axioms checklist scored against the strongest partial constructions — 3D YM, lattice strong-coupling regime where a gap *is* rigorously known) and a curated, reproducible summary of published lattice glueball data. A genuinely formal artifact could be a Lean formalization of a *toy* gap theorem (e.g., spectral gap for a finite-dimensional/lattice Hamiltonian at strong coupling) — honest, small, and clearly labelled as a toy.
- **Flatly impossible:** anything touching the continuum 4D construction; any lattice computation competitive with published values (cluster-scale Monte Carlo); formalizing OS reconstruction.

---

### 9. Banach–Tarski Paradox

#### (1) True current status — FLAG: NOT AN UNSOLVED PROBLEM
**It is a proven theorem (1924), not an open problem and not a logical paradox.** Banach & Tarski, "Sur la décomposition des ensembles de points en parties respectivement congruentes," *Fundamenta Mathematicae* 6 (1924), 244–277: a solid ball in R³ can be partitioned into *finitely many* pieces that reassemble by rigid motions into two balls each congruent to the original. "Paradox" = counterintuitive only. The proof essentially uses the axiom of choice (to select orbit representatives) and a paradoxical decomposition of the free group F₂ embedded in SO(3); the pieces are necessarily non-Lebesgue-measurable (which is exactly why volume is not contradicted). It **fails in dimensions 1 and 2** (the isometry groups are amenable/solvable), and the minimum number of pieces for the ball is 5. Any source listing Banach–Tarski among "unsolved problems" is simply wrong. Sources: theorem statement and 1924 provenance, read 2026-10-21, https://sugaku.net/oa/W4236932388/ ; https://encyclopediaofmath.org/wiki/Banach%E2%80%93Tarski_paradox

#### (2) Strongest results / context
The theorem itself is the result; its modern content is the theory it launched: amenability (von Neumann), paradoxical decompositions, and the fact that in Solovay-type models of ZF + DC where all sets are measurable, Banach–Tarski *fails* — so it is a theorem *of ZFC*, equivalent in flavor to a choice principle, not an absolute geometric fact. Dougherty–Foreman (1992) even produced a version with pieces having the Baire property. Source: read 2026-10-21, https://www.researchgate.net/publication/11743897_Banach-Tarski_Paradox_Using_Pieces_with_the_Property_of_Baire

#### (3) Formalization state
**Fully formalized — in Coq.** Daniel de Rauglaudre, "Formal Proof of the Banach-Tarski Paradox," *Journal of Formalized Reasoning* 10(1), 2017: a complete Coq proof; its `Print Assumptions` output transparently lists the axioms used (classical logic and a choice principle, TTCA) — an ideal audit target. No comparably complete Lean/Mathlib version was found in the sources consulted (Mathlib has the free-group and group-action ingredients). Source: read 2026-10-21, https://jfr.unibo.it/article/download/6927/7043

#### (4) Week-tractability verdict
- **Plausible artifact (best on this list):** a Lean 4 formalization of the *core* of the theorem with no `sorry` — realistically scoped as: paradoxical decomposition of F₂, its action by rotations on S² minus a countable set, and equidecomposability of the sphere — *or* a complete, axiom-audited port/verification report of the Coq proof with a modern exposition. The proof is finite, classical, and fully understood: success is a matter of labour, not insight.
- **Flatly impossible:** nothing of substance — which is precisely the point. The only impossible framing is "solving" it as an open problem. (A full ball-in-R³ Lean port in 7 days is ambitious; the sphere-level core is the safe scope.)

---

### 10. Continuum Hypothesis

#### (1) True current status — FLAG: SETTLED, BY INDEPENDENCE
CH asserts 2^{ℵ₀} = ℵ₁ (no cardinal strictly between the integers and the reals). Its status in ZFC is **completely settled**:
- **Gödel (1940):** CH **cannot be disproved** in ZFC (assuming ZF is consistent). He built the constructible universe L, an inner model of ZF in which AC and (generalized) CH hold — so ZFC + CH is relatively consistent.
- **Cohen (1963):** CH **cannot be proved** in ZFC either. He invented forcing, adjoining many new reals to a model to obtain a model of ZFC + ¬CH (indeed 2^{ℵ₀} can consistently be ℵ₂, ℵ_ω₊₁, … subject to König-type constraints) — so ZFC + ¬CH is relatively consistent. Fields Medal 1966.
- **Conclusion:** CH is **independent of ZFC** (assuming Con(ZFC)). It is neither an open problem in ZFC nor "unknown whether true": any resolution requires *new axioms*, and the live research questions are about which extensions (large cardinals do *not* settle CH; forcing axioms like PFA imply 2^{ℵ₀} = ℵ₂; Woodin's program argues both sides) should be adopted. Sources: read 2026-10-21, https://en.wikipedia.org/wiki/Generalized_continuum_hypothesis (independence section); exposition, read 2026-10-21, https://www.academia.edu/43949246/Forcing_and_the_Independence_of_the_Continuum_Hypothesis

#### (2) Strongest results / context
The independence theorem *is* the strongest result, and it is unconditional mathematics (relative consistency). Modern refinements: Easton's theorem (the continuum function on regular cardinals is constrained only by monotonicity + König), and the fact that large-cardinal axioms are themselves independent of CH questions (they are preserved by small forcing that changes 2^{ℵ₀}).

#### (3) Formalization state
**Fully formalized in Lean — a landmark.** The Flypitch project (Han, van Doorn, et al., ITP 2019 / CPP 2020) formalized *forcing and the independence of CH* in Lean 3 using Boolean-valued models: both `CH_unprovable` and `¬CH_unprovable`, hence `independence_of_CH`. (Their formalization proves the CH direction by collapse forcing rather than by constructing L — same independence conclusion.) Much of Flypitch did not migrate into Mathlib proper, but the standalone artifact builds and is auditable. Source: read 2026-10-21, https://flypitch.github.io/assets/flypitch-itp-2019.pdf ; http://florisvandoorn.com/papers/flypitch-cpp-2020.pdf

#### (4) Week-tractability verdict
- **Plausible artifact:** a definitive axiom-analysis dossier (what Gödel and Cohen each proved, with the relative-consistency statements stated exactly) *plus* a verified formal component: reproduce/build the Flypitch independence proof in a pinned environment, produce an axiom-and-`sorry` audit of it, and formalize one self-contained fragment from scratch in current Lean/Mathlib (e.g., the Cohen-poset combinatorics for a finite fragment, or L satisfying CH for a bounded level). Guaranteed-verifiable output.
- **Flatly impossible:** "proving or disproving CH" in ZFC — provably impossible, not merely hard. Any claimed ZFC proof of CH or ¬CH the team might hallucinate is *certainly* wrong; that certainty is itself a useful guardrail.

---

## Comparative Ranking by Realistic One-Week Verifiable Output

Assumptions: 20 AI text-and-mathematics agents, web access, ordinary laptops/cloud notebooks, **no serious compute cluster**; "verifiable output" = an artifact a third party can check (Lean proof with no `sorry`, reproducible computation with code + checksums, or a statement-matching audit against primary sources).

| Rank | Problem | One-line justification |
|---|---|---|
| 1 | Banach–Tarski | Already a theorem with a finite classical proof and a complete Coq formalization to port/audit — a no-`sorry` Lean core proof is achievable by labour alone. |
| 2 | Continuum Hypothesis | Independence is already fully formalized in Lean (Flypitch), so the week can deliver a reproduced build, an axiom audit, and a definitive axiom-analysis with zero discovery risk. |
| 3 | Collatz | Trivial to state and cheap to compute: a reproducible verification to ~2⁴⁰ with certificates plus a Lean proof of an elementary partial result (residue-class families / small cycle exclusions) fits easily in a week. |
| 4 | Goldbach | A clean-room segmented-sieve verification to ~10¹¹–10¹² with checkable certificates and a Lean finite-range proof is realistic; the theorems around it (Helfgott, Chen) give a rich, settled synthesis target. |
| 5 | Twin Primes / Bounded Gaps | PrimeGapsLib (Aug 2026) and the unreviewed 240/212/186 cascade create concrete audit work — comparator statement-matching and numerical-certificate re-verification — but no new sieve mathematics is possible in a week. |
| 6 | BSD | LMFDB data makes a fully reproducible rank/BSD-constant audit for all curves below a conductor bound a solid artifact, but Mathlib's missing L(E,s) caps any formalization at explicit group-law examples. |
| 7 | Riemann | Superb infrastructure (Mathlib ζ/L-functions, formalized PNT, quasi-RH comparator) supports an audit/synthesis and small formal lemmas, but every *new* bound needs cluster-scale interval arithmetic. |
| 8 | P vs NP | The barriers make an excellent rigorous synthesis and a small relativization fragment is formalizable, yet most of the week yields exposition rather than checkable mathematics. |
| 9 | Navier–Stokes | The Sept 2026 C/D claim makes a Fefferman-vs-manuscript-vs-Lean concordance genuinely valuable, but auditing a 166-page proof and its large Lean project — let alone Leray/CKN — exceeds a no-cluster week. |
| 10 | Yang–Mills | No formalization infrastructure, lattice evidence needs Monte-Carlo clusters, and the Clay bar is a full constructive continuum QFT — only a synthesis (plus an honestly-labelled toy gap formalization) is possible. |

**Recommendation in one sentence:** if the team must *ship a verified artifact*, choose Banach–Tarski (formalization) or CH (audit + analysis); if it must work on a genuinely open problem, choose Collatz or Goldbach (reproducible computation + a named formalized fragment); treat the 2026 Navier–Stokes / quasi-RH / prime-gap claims as *audit subjects*, not as problems to re-solve.

---

## Could not verify / Open questions

- **All Sept–Oct 2026 breakthrough claims are unadjudicated.** Navier–Stokes C/D (OpenAI), quasi-RH 7/8 (OpenAI), prime gaps 240/236/212/186, and Λ ≤ 0.1787854 are supported by public manuscripts/Lean artifacts and reputable trade-press reporting (Scientific American, Science, IEEE Spectrum) but by **no completed peer review and no independent verification** in the sources consulted (checked to 21 Oct 2026). Clay's "apparently been settled" (11 Sept 2026) is an acknowledgment, not a certification; its prize rules impose qualifying publication, ≥ 2 years, and general acceptance.
- **Helfgott publication status:** sources agree the ternary-Goldbach proof is community-accepted and was accepted (2015) for *Annals of Mathematics Studies* with major revisions underway; I could not confirm a final published edition as of Oct 2026. Do not cite it as "published in journal X, year Y."
- **BSD record rank:** Elkies' 2006 rank-28 curve is universally cited as the record; I did not find an institutional source certifying the *exact* current record (28 vs. higher conditional examples) as of 2026 — treat "28" as the standard cited benchmark, not a freshly verified record.
- **Prime-gap cascade details:** the 236 (Kintali) and 212 (Axiom) claims rest on fewer/weaker sources than Stadlmann's arXiv preprint (240) and Axiom's *formalization* of 246 (IEEE Spectrum). The Wikipedia prime-gap summary — "none peer-reviewed, established bound at 246" — is the safest single adjudication.
- **Formalization absences** (no Mathlib L(E,s)/BSD, no Mathlib Navier–Stokes, no Mathlib QFT, no Lean Cook–Levin) are negative claims based on library documentation and targeted searches on 2026-10-21; small private repositories may exist that search did not surface. The numerous 2026 Zenodo/PhilArchive "complete proofs" of Yang–Mills, P = NP, etc. were disregarded as unrecognized by any institution — their existence is noted here so the team is not surprised by them.
- The mission did not specify the team's Lean/compute environment beyond "no serious compute cluster"; verdicts assume standard cloud notebooks. With a real cluster, Collatz/Goldbach/Riemann verification scopes (not their rankings) would expand.

## Sources

All read 2026-10-21 via the web index / page fetch; status flags as in the text.

**Cross-cutting / Clay status**
- Millennium Prize Problems (status incl. Sept 2026 NS claim, 2-year rule) — https://en.wikipedia.org/wiki/Millennium_Prize_Problems
- OpenAI 722-manuscript release, withdrawals and Lean coverage — https://cellcog.ai/blog/openai-math-results/

**Riemann**
- Polymath 15, Λ ≤ 0.22 — https://arxiv.org/abs/1904.12438v1
- De Bruijn–Newman constant, bound history (0.22 → 0.2 Platt–Trudgian) — https://en.wikipedia.org/wiki/De_Bruijn%E2%80%93Newman_constant
- Platt–Trudgian, RH true up to 3×10¹² — https://arxiv.org/pdf/2004.09765
- Guth–Maynard, Annals 2026 — https://annals.math.princeton.edu/2026/203-2/p06 ; preprint https://arxiv.org/pdf/2405.20552
- Gomila, claimed Λ ≤ 0.1787854 (preprint) — https://raw.githubusercontent.com/judegomila/dbn-lambda-01787854-candidate-audit/a74738deb6d5e0f76887cb36901da08b68dca705/gomila_dbn_lambda_01787854_release.pdf
- Quasi-RH exposition incl. status/formalization chapters — https://judegomila.com/posts/quasi-riemann-hypothesis
- Quasi-RH expert reactions — https://www.aieon.ee/eng/2026/10/openai-quasi-riemann-hypothesis-proof-unpacked-by-lichtman-and-radziwill/
- Loeffler–Stoll, zeta & L-functions in Lean / PNT+ — https://arxiv.org/html/2503.00959v3 ; https://AlexKontorovich.github.io/PrimeNumberTheoremAnd/blueprint.pdf

**Collatz**
- Barina 2025, verification to 2⁷¹ (J. Supercomputing) — https://www.vut.cz/www_base/vav_priloha.php?vavID=197809&prilohaID=298514
- Tao 2022, almost-all orbits (Forum Math Pi) — https://www.cambridge.org/core/services/aop-cambridge-core/content/view/1008CC2DF91AF87F66D190C5E01C907F/S2050508622000087a.pdf/div-class-title-almost-all-orbits-of-the-collatz-map-attain-almost-bounded-values-div.pdf
- Collatz survey facts (Terras, Krasikov–Lagarias, cycles) — https://en.wikipedia.org/wiki/Collatz_conjecture
- FormalConjectures contents — https://deepwiki.com/google-deepmind/formal-conjectures/3.1-wikipedia-conjectures
- Mazur-density Lean formalization example (2026) — https://hexagonmath.org/2610.00249v1

**Goldbach**
- Goldbach's conjecture (Oliveira e Silva 4×10¹⁸; Helfgott status; ≤4 primes corollary) — https://en.wikipedia.org/wiki/Goldbach's_conjecture
- MAA review (Helfgott proof status) — https://old.maa.org/press/maa-reviews/goldbachs-problem
- Chen's theorem — https://en.wikipedia.org/wiki/Chen%27s_theorem
- FormalQualBench stubs (ternary Goldbach target) — https://deepwiki.com/math-inc/FormalQualBench/3.3-number-theory-and-additive-combinatorics
- Lean finite Goldbach checks; Vega claim refuted — https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Checking.20the.20Goldbach.20conjecture.html

**Twin primes / bounded gaps**
- Polymath 8 retrospective (246; EH 12; generalized EH 6) — https://arxiv.org/pdf/1409.8361 ; https://sugaku.net/oa/W1576273050/
- Prime gap (2026 cascade adjudication: none peer-reviewed, established 246) — https://en.wikipedia.org/wiki/Prime_gap
- Stadlmann, H₁ ≤ 240 (arXiv:2608.31126) — https://arxiv.org/html/2608.31126v1
- Axiom PrimeGapsLib formalization of 246 — https://spectrum.ieee.org/axiom-math-246-theorem-formalization ; https://primegaps.axiommath.ai/blueprint.pdf ; https://www.unite.ai/axiom-maths-ai-verifies-the-246-prime-gaps-theorem-in-lean/
- 2026 cascade explainer — https://traictory.com/news/2026-10-03-prime-gaps-186-explained

**BSD**
- Rank ≤1 theorem (Coates–Wiles, Gross–Zagier, Kolyvagin, Rubin) — https://arxiv.org/html/2506.03465v2 ; https://ncatlab.org/nlab/revision/Birch+and+Swinnerton-Dyer+conjecture/7
- Twist families (36,687 curves) — https://arxiv.org/pdf/2601.16044 ; https://antsmath.org/ANTSXVII/papers/antsxvii-banwait_huang-paper.pdf
- LMFDB elliptic-curve data sources (complete to conductor 500,000) — https://lmfdb.org/EllipticCurve/Q/Source
- Mathlib elliptic-curve group law — https://Leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.html

**P vs NP**
- Aaronson–Wigderson, algebrization (incl. relativization & natural proofs history) — https://www.zanotowane.pl/1131/4086/
- Barriers summary — https://en.wikipedia.org/wiki/P_and_NP
- Isabelle AFP Cook–Levin formalization — https://isa-afp.org/entries/Cook_Levin.html

**Navier–Stokes**
- Classical partial results (Leray, CKN, BKM, Tao barrier) — https://navier-stokes.org/progress/
- Sept 2026 claim status, Clay response, Lean self-assessment, A–D analysis — https://navier-stokes.org/navier-stokes-problem-solved/
- Scientific American on the claim and method dispute — https://www.scientificamerican.com/article/openais-blockbuster-navier-stokes-proof-isnt-what-we-thought-it-was/?utm_campaign=sprinklr&utm_medium=social&utm_source=x
- Science (AAAS) on the priority controversy — https://bpb-us-w2.wpmucdn.com/wp.wpi.edu/dist/a/409/files/2026/09/Science_2026_How-an-AI-math-breakthrough-ignited-a-controversy.pdf
- DeepMind (Sept 2025), unstable singularities in fluid equations — https://deepmind.google/blog/discovering-new-solutions-to-century-old-problems-in-fluid-dynamics/
- Scientific American, AI/Euler blowup race and Feb 2026 non-transfer result — https://www.scientificamerican.com/article/humans-and-ai-race-to-blow-up-maths-toughest-equations/

**Yang–Mills**
- Clay/Jaffe–Witten requirements (OS axioms, Δ > 0) — https://seoulinside.substack.com/p/yang-mills-theory-archive
- Status: Clay still lists unsolved — https://mail.smonad.com/problems/yang-mills.html
- Lattice evidence (glueball ≈1.5–1.7 GeV, confinement) — https://www.academia.edu/165430749/Mass_Gap_Color_Screening_and_Strong_Coupling_from_Lattice_Geometry

**Banach–Tarski**
- Theorem (1924) and Coq formal proof — https://sugaku.net/oa/W4236932388/ ; https://jfr.unibo.it/article/download/6927/7043
- Background/equidecomposability — https://encyclopediaofmath.org/wiki/Banach%E2%80%93Tarski_paradox
- Baire-property version (Dougherty–Foreman) — https://www.researchgate.net/publication/11743897_Banach-Tarski_Paradox_Using_Pieces_with_the_Property_of_Baire

**Continuum Hypothesis**
- Independence (Gödel L; Cohen forcing) — https://en.wikipedia.org/wiki/Generalized_continuum_hypothesis ; https://www.academia.edu/43949246/Forcing_and_the_Independence_of_the_Continuum_Hypothesis
- Flypitch Lean formalization of independence — https://flypitch.github.io/assets/flypitch-itp-2019.pdf ; http://florisvandoorn.com/papers/flypitch-cpp-2020.pdf