Post-Cutoff

OpenAI’s maths release, family by family

OpenAI released 721 AI-written mathematics manuscripts on 6 October 2026, grouped into 373 "result families", and added more on 7 and 26 October. Almost none has been peer reviewed. This page lists every family: how well known the problem is, whether a machine-checked Lean proof exists, what happened to it since, and where we cover it.

373 result families, 245 with a Lean formalization in the repository (often of part of the claim: each scope note says what is covered). Papers OpenAI withdrew (such as the abelian-eightfold Weil-class paper and its two dependants) are no longer listed in the release; its history.md explains each withdrawal. 100 have at least one entry here. 88 concern famous problems, 19 of them still without their own entry. Plain text for AI models

Source: github.com/openai/math (CONTENTS.md, lean/formalization.yaml, history.md), read 29 October 2026; community checks: oai-math-revised. A Lean proof shows the formal statement is proved; whether that statement says what the paper claims still needs a human reader.

Famous problems 88

Named problems that mathematicians outside the field would recognise. Each should have its own entry.

  1. 002 The full BSD formula from low Selmer corank

    Awaiting review; here: OpenAI claims BSD in Selmer corank ≤ 1 and Goldfeld’s conjecture

    Full BSD formula when some p-power Selmer corank is 0 or 1. Calegari, Colmez: technical, no progress on general BSD; Burungale: correctness still being analysed.

  2. 003 The quasi-Riemann hypothesis

    Lean Awaiting review; here: OpenAI model claims the quasi-Riemann hypothesis, William Banks writes out OpenAI’s Landau–Siegel proof with explicit constants, Cureton and Thorner, with AxiomProver, extend the quasi-Riemann zero-free half-plane to every Dedekind zeta function (Re s > 31/32, Lean-formalized), All 16,453,493 imaginary quadratic fields with class number ≤ 2000 determined unconditionally, using OpenAI’s Siegel-zero proof made explicit in Lean with Claude Opus 5.5

    Zero-free half-plane Re s > 7/8 for ζ and Dirichlet L-functions, Lean (two kernels). Siegel-zero companion reproved by Kerr and Green; Tao sketch; Quanta feature.

  3. 004 Hilbert’s tenth problem over ℚ

    Awaiting review; here: OpenAI claims Hilbert’s tenth problem over ℚ is undecidable

    Rational solvability of integer polynomials is undecidable. Unformalized; uses families 006 and 010. Calegari: ‘threw me for a loop’; Pasten: ‘original’; Sun: 86 unknowns.

  4. 005 Irrationality of Catalan’s constant

    Lean Awaiting review; here: OpenAI: Catalan’s constant is irrational (Lean)

    Catalan’s constant is irrational; one-line Lean statement over Mathlib, comparator accepted. Calegari sees new ideas or optimizations; follow-ups derive μ(G) ≤ 740.

  5. 006 Goldfeld’s conjecture: densities and mean analytic rank

    Awaiting review; here: OpenAI claims BSD in Selmer corank ≤ 1 and Goldfeld’s conjecture

    Goldfeld’s conjecture: quadratic twists split 50/50 between analytic ranks 0 and 1, mean 1/2. A GitHub check found a weak proof step, not a disproof.

  6. 007 Ordinary two-point correlations and the corrected Elliott conjecture

    Lean Awaiting review; no entry yet

    Ordinary (non-logarithmic) two-point Chowla and binary corrected Elliott conjectures; Lean main theorem accepted. Wang–Yi build on it; no expert check yet. Lead filed.

  7. 008 The Deligne–Drinfeld conjecture

    Lean Confirmed by an independent expert; here: Deligne–Drinfeld conjecture proved; experts simplify and reprove OpenAI’s proof

    Deligne–Drinfeld proved; Willwacher: ‘remaining part … solved by OpenAI’, simplified proof; Hirose independent proof; Lean main statement accepted; HMI workshop. Own entry (confirmed).

  8. 016 Zilber–Pink in abelian varieties and the Siegel threefold

    Awaiting review; here: OpenAI claims abelian Zilber–Pink

    Abelian Zilber–Pink over Q̄ (hence over any char-0 field via Barroero–Dill) and curves in A2. Unformalized; Barroero–Dill–Kühne, Dogra–Saha cite it as announced.

  9. 017 The irrationality exponent of π is 2

    Lean Awaiting review; here: OpenAI model claims the irrationality exponent of π is exactly 2 (Lean-formalized), which implies the Flint–Hills series converges, Gregory Chudnovsky, with ChatGPT, claims the lemniscate period has irrationality exponent 2, with a Lean 4 proof built on OpenAI’s π-exponent library

    Irrationality exponent of π is 2 (Lean), implying Flint–Hills convergence. Calegari: ‘amazing result’; Zudilin notes closeness to Roth’s argument (via Persiflage).

  10. 019 The local p-adic section conjecture and global consequences

    Awaiting review; no entry yet

    Local p-adic section conjecture; Grothendieck’s section conjecture over ℚ for X0(N), X1(N). Unformalized. Carlson–Kim–Srinivasan–Stix online seminar since 20 Oct. Lead filed.

  11. 028 Uniformly bounded components of Gaussian-prime graphs

    Lean Awaiting review; no entry yet

    Gaussian moat conjecture: no bounded-step walk to infinity through Gaussian primes; components uniformly bounded. Lean main accepted; nonexplicit bound. Lead filed.

  12. 029 Primitive roots for every admissible integer base

    Awaiting review; here: OpenAI claims Artin’s primitive root conjecture (infinitude)

    Infinitude in Artin’s primitive root conjecture for every admissible base, ≫ x/(log x)² primes. Calegari: ‘not at all surprising’ given QRH; Bhargava adds positive density.

  13. 030 Modularity of elliptic curves over imaginary quadratic fields

    Awaiting review; here: OpenAI: elliptic curves over imaginary quadratic fields are modular

    Every elliptic curve over every imaginary quadratic field is modular. Calegari: ‘a really nice trick’; Bao Le Hung extends it to all totally real fields.

  14. 032 The rational Hodge conjecture for CM abelian varieties

    Lean Confirmed by an independent expert; here: OpenAI release proves the rational Hodge conjecture for all CM abelian varieties, giving the Tate conjecture for abelian varieties over finite fields; Lean proof added 26 Oct, human-written proof by van Hoften and Sempliner, and Milne calls it proved

    Rational Hodge for CM abelian varieties; three K3 companions withdrawn 7 Oct, Lean added 26 Oct. Van Hoften–Sempliner reprove it; Milne: ‘in fact been proved’.

  15. 033 Iitaka subadditivity, variation, and logarithmic additivity

    Lean Awaiting review; here: OpenAI claims the abundance conjecture; Jihao Liu raises priority

    Campana’s orbifold Iitaka subadditivity and Popa’s inequality; companion claims ordinary Iitaka C_{n,m}. Lean covers one branch only. Covered in the abundance entry.

  16. 034 Log abundance for compact Kähler spaces under logarithmic Iitaka subadditivity

    Updated by OpenAI; here: OpenAI claims the abundance conjecture; Jihao Liu raises priority

    Log abundance in characteristic zero and for compact Kähler spaces, effective Iitaka fibration; Kähler papers revised 7 Oct. Jihao Liu raises priority; no expert assessment.

  17. 038 Fujita’s freeness conjecture

    Awaiting review; no entry yet

    Fujita’s freeness conjecture at the sharp bound m ≥ n+1 in every dimension. 23 Sep manuscript, unformalized; no expert assessment found. Lead filed.

  18. 039 Nagata’s conjecture and maximal Seshadri constants

    Lean Confirmed by an independent expert; here: Nagata’s 1959 conjecture

    Nagata’s conjecture for r ≥ 10 very general points and maximal Seshadri constants. Lean main. Tevelev’s exposition calls the proof remarkably simple.

  19. 040 Bloch’s conjecture for complex surfaces

    Awaiting review; here: OpenAI claims Bloch’s conjecture for surfaces

    Bloch’s conjecture for every surface with p_g = 0, via Quot-scheme virtual localization. Unformalized; Litt flags a miscitation he thinks harmless.

  20. 047 Zariski cancellation and affine fibrations over the complex numbers

    Lean Awaiting review; no entry yet

    Zariski cancellation fails over ℂ in dimension 4 (explicit fourfold); Dolgachev–Weisfeiler disproved. Lean accepted; Huang’s entry cites it only. Lead filed.

  21. 054 Irrational cubic fourfolds with Hodge-theoretic and categorical K3 associations

    Awaiting review; no entry yet

    Very general cubic fourfolds of large admissible discriminant are irrational despite K3 associations, disproving Kuznetsov’s conjecture. No expert comment found. Lead filed.

  22. 072 Brennan’s conjecture and the integral-means spectrum

    Lean Confirmed by an independent expert; here: Brennan’s conjecture: experts confirm and shorten OpenAI’s proof

    Brennan’s conjecture and the integral-means spectrum, Lean main. Binder, Ivrii, Prause and Smirnov checked it and gave a shorter proof.

  23. 073 The Falconer distance conjecture

    Lean Awaiting review; here: OpenAI proves the Falconer distance conjecture (Lean)

    Falconer’s distance conjecture in every dimension; Lean statement uses Mathlib’s dimH and Lebesgue measure, accepted. Cheng et al. build a quantitative planar version.

  24. 074 Kakeya in three and four dimensions

    Awaiting review; here: OpenAI claims 3D restriction and Bochner–Riesz conjectures, OpenAI claims local smoothing and Kakeya in all dimensions

    Kakeya maximal conjecture in ℝ³ and full dimension of 4D Kakeya sets (manuscripts only); superseded by family 079’s all-dimension Lean claim.

  25. 077 Fourier restriction for positively curved surfaces

    Awaiting review; here: OpenAI claims 3D restriction and Bochner–Riesz conjectures, OpenAI claims local smoothing and Kakeya in all dimensions

    Stein’s Fourier restriction conjecture in ℝ³ (sphere, positively curved surfaces). Manuscripts only; Korobenko–Sawyer cite the diagonal theorem.

  26. 078 The three-dimensional Bochner–Riesz conjecture

    Awaiting review; here: OpenAI claims 3D restriction and Bochner–Riesz conjectures, OpenAI claims local smoothing and Kakeya in all dimensions

    Three-dimensional Bochner–Riesz conjecture in its strict range. Manuscript only; also a corollary of family 079’s all-dimension claim.

  27. 079 Local smoothing for the Euclidean wave equation

    Lean Updated by OpenAI; here: OpenAI claims 3D restriction and Bochner–Riesz conjectures, OpenAI claims local smoothing and Kakeya in all dimensions

    Sogge’s local smoothing conjecture, 3D (Sep) and every dimension (manuscript and Lean added 26 Oct), with Kakeya and Bochner–Riesz corollaries. Leng: ‘absolutely shocking’.

  28. 087 The Mahler conjectures, functional inequalities and polar-product symplectic width

    Lean Awaiting review; here: OpenAI proves the Mahler conjectures (Lean)

    Symmetric and general Mahler conjectures in every dimension with equality cases; Lean for both, accepted. Kalai highlights it; Winter: Mahler implies Kalai’s flag conjecture.

  29. 090 Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy

    Lean Awaiting review; no entry yet

    Universal optimality of the triangular lattice, Sandier–Serfaty, Brauchart–Hardin–Saff and planar Cohn–Elkies sharpness. Lean for main parts. No expert comment found. Lead filed.

  30. 102 The Unique Games Conjecture and optimal approximation thresholds

    Lean Awaiting review; here: OpenAI model claims a proof of Khot’s Unique Games Conjecture, with Lean formalization

    Khot’s Unique Games Conjecture plus direct Max-Cut and Vertex Cover hardness, Lean. Moshkovitz (via Aaronson): ‘The Unique Games Conjecture is true’; writeup ‘poorly written’.

  31. 103 Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$

    Lean Updated by OpenAI; here: OpenAI claims L = RL = BPL with a Lean proof

    L = RL = BPL, Lean added 7 Oct; configuration fixed 26 Oct; a community re-check found statement definitions identical to the proof’s.

  32. 106 Hardness of coloring three-colorable graphs

    Lean Awaiting review; here: OpenAI model claims a proof of Khot’s Unique Games Conjecture, with Lean formalization

    NP-hard to colour 3-colourable graphs with any constant number of colours, Lean. Fei–Minzer–Wang derive the same from 4-to-1 games (UGC entry).

  33. 107 Matrix multiplication with exponent at most 9/4

    Lean Confirmed by an independent expert; here: OpenAI proves ω ≤ 9/4 for matrix multiplication

    ω ≤ 9/4 for matrix multiplication, Lean. Re-proved over every field by Amanov–van den Berg–Zuiddam and constructively by Pass; algorithms galactic.

  34. 109 Integer multiplication below $`n\log n`$

    Awaiting review; here: Outside researchers using AI crowdsource a tighter exponent in OpenAI’s integer-multiplication result #109, from 2^-182 to about 2^-8.4 (conditional)

    Integer multiplication in O(n (log n)^{1−κ}), κ = 2^−182. David Harvey: ‘the claimed o(n log n) bound is plausible’, details unchecked; community raised κ.

  35. 113 Approximate counting and entropy of perfect matchings

    Lean Confirmed by an independent expert; here: Counting perfect matchings in general graphs: OpenAI FPRAS, simplified proof

    FPRAS for counting perfect matchings in general graphs; AOV entropy conjecture. Lean. Liu–Meng give a simplified self-contained proof. Own entry (30 Oct).

  36. 124 Polynomial-time scheduling on three identical machines

    Lean Awaiting review; no entry yet

    Polynomial-time minimum-makespan scheduling of unit jobs with precedences on three machines, a Garey–Johnson open problem since 1979. Lean main accepted. Lead filed.

  37. 130 Exact Fourier transforms below $`n\log n`$

    Lean Awaiting review; no entry yet

    Claims exact DFT in O(n(log n)^(1−10⁻¹³)) operations, below n log n; Lean; Recht calls it galactic; Aaronson: barrier ‘since the 1960s’; community raised the saving.

  38. 142 Deterministic polynomial factorization over prime fields

    Awaiting review; no entry yet

    Claims deterministic polynomial-time factoring over F_p without GRH, a classic derandomization problem; no Lean; relies on a companion Hecke zero-free claim; Voloch posted a reformulation.

  39. 143 Hilbert’s sixteenth problem: uniform bounds for limit cycles

    Lean Awaiting review; here: Hilbert’s 16th problem: uniform limit-cycle bound claimed (OpenAI)

    Claims a uniform bound on limit cycles of planar polynomial fields (Hilbert’s 16th, second part); Lean covers only quintic Liénard; no expert check.

  40. 145 Rokhlin’s multiple-mixing problem

    Lean Awaiting review; no entry yet

    Claims mixing implies mixing of all orders (Rokhlin, 1949); Lean accepted; Bryna Kra singled it out but said the writing blocked her understanding.

  41. 155 A counterexample to periodic tiling in dimension three

    Lean Awaiting review; here: Periodic tiling conjecture fails in dimension 3 (OpenAI claim, Lean-checked)

    Finite ℤ³ tile with no fully periodic tiling (lowest possible dim), ℝ³ thickening too; Lean incl. minimality accepted. Demaine–Langerman build on it (undecidability). No expert check yet. Own entry.

  42. 156 Borsuk’s conjecture fails in dimension nine

    Lean Awaiting review; here: Borsuk’s conjecture fails in dimension 9 (OpenAI claim, Lean-checked)

    Compact (infinite) projector set of ℝP³ in ℝ⁹ needs >10 parts; record was 63 (finite). Lean accepted; Kalai: ‘major progress’, ‘very beautiful’. Finite subsets 8-colourable (Damásdi). Own entry.

  43. 157 Graph coloring, clique minors, and Colin de Verdière invariants

    Lean Awaiting review; here: Hadwiger’s conjecture disproved? (OpenAI, Lean)

    Claims counterexamples to Hadwiger’s conjecture, even fractional, with independence number 2; Lean proves the ordinary form (added 7 Oct); no expert check.

  44. 158 The Euclidean plane cannot be colored with five colors

    Lean Awaiting review; here: Chromatic number of the plane is 6 or 7, OpenAI claims (Lean)

    Claims the plane is not 5-colourable, so χ(R²) is 6 or 7; Lean (definition caveat closed 26 Oct); Koshelev–Kupavskii–Voronov build on it.

  45. 159 Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi bounds

    Lean Awaiting review; here: Erdős’s arithmetic-progression conjecture claimed (OpenAI, Lean)

    Claims Erdős’s $5000 arithmetic-progression conjecture via quasipolynomial Szemerédi bounds; Lean covers the qualitative statement; Bloom: synthesis of existing techniques.

  46. 161 Counterexamples to Sidorenko’s conjecture and the forcing conjecture

    Lean Awaiting review; here: Sidorenko’s conjecture disproved? (OpenAI, Lean)

    Disproves Sidorenko’s conjecture with a 35-vertex, 66-edge bipartite graph, and the forcing conjecture; Lean proves a host exists, none published.

  47. 165 The Harary–Hill and Zarankiewicz crossing-number formulas

    Lean Awaiting review; here: Harary–Hill and Zarankiewicz crossing-number conjectures (OpenAI, Lean)

    Claims exact crossing numbers of K_n and K_m,n (Harary–Hill, Zarankiewicz); Lean; Balko published a simplified human proof; own entry.

  48. 167 Planar distinct distances and unit-distance bounds

    Lean Awaiting review; here: Unit-distance bound below n^(4/3) claimed (OpenAI, Lean)

    Claims u(n) = O(n^(4/3−δ)), first gain over Spencer–Szemerédi–Trotter since 1984, plus weak pinned distances; Lean; WillSawin sketched an effective version.

  49. 168 Combinatorial invariance of Kazhdan–Lusztig polynomials

    Lean Awaiting review; no entry yet

    Claims the combinatorial invariance conjecture for Kazhdan–Lusztig polynomials in all Coxeter systems (studied by DeepMind in 2021); Lean; cited as claimed by Caselli–Marietti.

  50. 180 Barnette’s Hamiltonian-cycle conjecture

    Lean Confirmed by an independent expert; here: Barnette’s 1969 Hamiltonicity conjecture

    Claims Barnette’s Hamiltonicity conjecture; Lean; Zhentao Li’s hand-written, partly re-proved version (arXiv 2610.30490); own entry.

  51. 193 Serre’s intersection-multiplicity conjecture

    Awaiting review; no entry yet

    Claims Serre’s positivity of intersection multiplicities for all regular local rings, incl. ramified mixed characteristic; no Lean; formal-conjectures keeps it open.

  52. 196 A counterexample to Kaplansky’s zero-divisor conjecture

    Lean Awaiting review; here: Kaplansky’s zero-divisor and direct-finiteness conjectures refuted? (OpenAI, Lean)

    Claims a finitely presented torsion-free group with zero divisors in F₂[G], refuting Kaplansky’s zero-divisor conjecture; Lean-formalized; no explicit elements published.

  53. 197 A torsion-free group algebra that is not directly finite

    Lean Awaiting review; here: Kaplansky’s zero-divisor and direct-finiteness conjectures refuted? (OpenAI, Lean)

    Claims Kaplansky direct-finiteness counterexamples, refuting Gottschalk’s surjunctivity and the Determinant Conjecture; Lean only for torsion examples; torsion-free case unformalized.

  54. 202 The blockwise Alperin weight conjecture

    Awaiting review; no entry yet

    Claims the blockwise Alperin weight conjecture for every finite group and prime; no Lean; no expert reaction found.

  55. 213 Critical percolation on every quasi-transitive graph

    Lean Awaiting review; here: Claude-written Lean proof claims the dying percolation conjecture θ(p_c)=0 in every dimension

    Claims θ(p_c) = 0 on Z³ and on all quasi-transitive graphs (Benjamini–Schramm); Z³ covered in our Anthropic entry; quasi-transitive part not.

  56. 215 Canonical $`O(3)`$ continuum limit and exact $`O(4)`$ mass asymptotics

    Lean Awaiting review; here: 2D O(n) mass gap (Polyakov) and O(3) continuum limit claimed (OpenAI)

    Claims Polyakov’s 2D O(n) mass gap (n ≥ 3), an O(3) continuum theory with a gap, and O(4) asymptotics; Lean for decay only.

  57. 223 Random-cluster interfaces: critical, disordered, thermal, and natural-time scaling

    Awaiting review; no entry yet

    Claims SLE limits of critical square-lattice FK interfaces for 0<q≤4, including bond percolation (q=1); no Lean; an independent audit alleges a gap.

  58. 235 Limiting random SAT thresholds, sharp variance and computability

    Lean Awaiting review; here: Random k-SAT threshold exists for every k ≥ 3: a human proof and an OpenAI Lean-checked proof

    Threshold for random k-SAT, every k ≥ 3, plus Θ(n) variance and computability of α₃; all 4 Lean challenges accepted (26 Oct). OpenAI credits Carenini’s human ECCC proof (5 Oct) with priority. Own entry.

  59. 237 The three-quarter exponent for honeycomb self-avoiding walk

    Lean Awaiting review; no entry yet

    Claims honeycomb self-avoiding walks have diameter n^(3/4+o(1)), Nienhuis’s prediction, via 13 manuscripts; Lean covers only supporting finiteness lemmas.

  60. 244 The Partition Principle does not imply Choice

    Lean Awaiting review; here: Set theorist Asaf Karagila refuses to review OpenAI’s claimed solution of the Partition Principle problem (does PP imply AC?): ‘It sucked’; calls the 722-paper release a ‘Denial of Service’, OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems

    Claims Con(ZF) gives a model of the Partition Principle without Choice; Lean; Karagila criticised the paper and declined to review; own entry.

  61. 246 Cannon’s conjecture

    Lean Awaiting review; here: Cannon’s conjecture claimed (OpenAI, Lean); Bonk’s seminar talk

    Claims Cannon’s conjecture: 2-sphere-boundary hyperbolic groups act geometrically on H³; Lean; Mario Bonk presented ‘the AI proof’ at Quasiworld (22 Oct).

  62. 247 An infinite finitely presented residually finite 2-group and a finitely presented nil algebra

    Lean Awaiting review; here: Finitely presented Burnside problem answered negatively? (OpenAI, Lean)

    Claims an infinite finitely presented periodic group (Steinberg group with property (T)) and a residually finite 2-group; Lean for the first.

  63. 248 Thompson’s group F is nonamenable

    Lean Confirmed by an independent expert; here: Thompson’s group F is nonamenable

    Claims Thompson’s group F is nonamenable; Lean; Kim–Lodha’s human exposition and follow-ups; own entry.

  64. 252 A torsion-free hyperbolic group that is neither residually finite nor linear over any field

    Lean Awaiting review; here: A non-sofic word-hyperbolic group

    Torsion-free hyperbolic group that is not residually finite, a long-standing question; Lean accepted. Basis of Sandhu–Thom’s non-sofic group. Kourovka: unverified AI solution.

  65. 254 Classifying spaces and geometric obstructions for Artin groups

    Lean Awaiting review; no entry yet

    Artin K(π,1) conjecture (finite rank), parabolic intersection conjecture, Artin group without geometric CAT(0) action; all Lean-accepted. Tiozzo: Astra shrank 116 generators to 12.

  66. 260 Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions

    Lean Awaiting review; here: Bray, Dolmen, Khuri & Schmidt prove the spacetime Penrose inequality for ‘maximally parameterized’ data with Claude’s help, and say OpenAI’s Oct 6 Penrose paper appears to finish their program

    Spacetime Penrose inequality in all dimensions plus charged, rotating and AdS versions. Lean covers supporting results only. Bray–Dolmen–Khuri–Schmidt prove a maximally parameterized case.

  67. 261 Localization and delocalization in the Anderson model

    Lean Awaiting review; here: OpenAI claims Anderson localization in 2D and extended states in 3D

    2D Anderson localization at every disorder and 3D absolutely continuous spectrum at weak disorder (Simon’s Problems 1–2). OpenAI Lean: spectrum only; third-party Lean of 3D.

  68. 264 Strong cosmic censorship near two-ended Kerr data

    Awaiting review; here: OpenAI claims strong cosmic censorship near Kerr

    Local strong cosmic censorship near Kerr in Christodoulou’s C⁰∩W^{1,2}_loc formulation, with C¹ and C² versions. No Lean. Sung-Jin Oh organised a reading group.

  69. 265 Area laws and tensor networks for two-dimensional gapped systems

    Awaiting review; here: OpenAI’s 2D area law proof Lean-verified by Axiom

    2D area law and polynomial PEPS for gapped ground states. Formalized independently (Axiom’s AreaLaw2D, TNLean). Aaronson: ‘One of the main open problems in Hamiltonian complexity.’

  70. 266 Exactly three mutually unbiased bases in dimension six

    Lean Awaiting review; no entry yet

    Zauner’s conjecture: exactly three MUBs in ℂ⁶, computer-assisted. Code restored 26 Oct; Lean proves only ≤5. Jaswal reports an independent certified computation (Zenodo, 13 Oct).

  71. 267 Positive-temperature Bose–Einstein condensation and exact quantum depletion

    Lean Awaiting review; here: OpenAI claims quantum ferromagnet order and interacting Bose condensation

    Bose–Einstein condensation in every ground state of the dilute hard-sphere gas (Lean accepted) and at fixed positive temperature; Bogoliubov depletion law. SciAm highlight.

  72. 268 The spin-one Haldane gap

    Awaiting review; here: OpenAI proves the spin-one Haldane gap (periodic chains)

    Spin-one Haldane gap for even periodic chains (computer-assisted). Hal Tasaki studied the analytic part favourably; computer part not independently checked. Own entry.

  73. 271 Bloch’s law, its lattice correction, and the spherical magnetization law

    Lean Awaiting review; here: OpenAI claims quantum ferromagnet order and interacting Bose condensation

    Spontaneous magnetization of the quantum Heisenberg ferromagnet in d≥3 (Lean accepted) and Bloch’s T^{3/2} law. OpenAI published a reasoning summary; SciAm highlight.

  74. 285 Counterexamples to Baum–Connes and Kadison–Kaplansky

    Awaiting review; here: OpenAI claims Baum–Connes and Kadison–Kaplansky counterexamples

    Coefficient-free Baum–Connes fails (torsion-free injectivity; irrational-trace surjectivity); Kadison–Kaplansky fails. Guoliang Yu builds on the irrational-trace paper (arXiv 2610.35674). No Lean.

  75. 287 Isomorphism of the free group factors

    Lean Confirmed by an independent expert; here: OpenAI model claims the free group factor problem

    Free group factors are all isomorphic, L(F₂)≅L(F₃). Lean accepted; Shlyakhtenko proved a C*-algebraic version (our entry marks it confirmed).

  76. 288 Kadison’s similarity conjecture

    Lean Awaiting review; here: OpenAI claims Kadison’s similarity problem (Lean)

    Kadison’s 1955 similarity problem answered positively, plus one hyperreflexivity constant; Lean full statement accepted (oai-math-revised, MathVet). AIM marks solved; no expert reaction. Own entry.

  77. 304 The Hilbert–Smith conjecture in every dimension

    Awaiting review; here: Hilbert–Smith conjecture claimed by OpenAI, Lean-checked by a separate AI proof

    Hilbert–Smith conjecture in every dimension; no Lean. A separate AI-agent proof is Lean-checked on Palomar (adbrw). Formal Conjectures issue #6914 still open.

  78. 305 Four-dimensional disk embedding and Wall’s conjecture

    Awaiting review; here: OpenAI claims 4D Borel counterexample and that F₂ is not good

    Disk embedding conjecture fails, so F₂ is not good (Freedman–Quinn); a PD4 group without aspherical manifold model (Wall). No Lean; no expert check found.

  79. 320 Nonhomeomorphic closed aspherical four-manifolds

    Awaiting review; here: OpenAI claims 4D Borel counterexample and that F₂ is not good

    Homotopy-equivalent, non-homeomorphic closed aspherical 4-manifolds with hyperbolic fundamental group: topological Borel conjecture fails in dimension 4. No Lean.

  80. 335 Gromov’s integral scalar-curvature bound for simplicial volume

    Awaiting review; here: OpenAI claims the aspherical positive-scalar-curvature conjecture

    Gromov–Lawson aspherical conjecture in all dimensions (positive scalar curvature forces rational inessentiality) and Gromov’s integral simplicial-volume bound. No Lean. Sauer: ‘I am stunned.’

  81. 338 Yau’s uniformization conjecture

    Awaiting review; no entry yet

    Yau’s uniformization conjecture: complete noncompact Kähler manifolds with positive bisectional curvature are biholomorphic to ℂⁿ. No Lean; no expert reaction found.

  82. 340 A counterexample to the nearby Lagrangian conjecture

    Awaiting review; here: OpenAI claims a counterexample to the nearby Lagrangian conjecture

    Counterexample to Arnold’s nearby Lagrangian conjecture in T*(S⁹×S^{N−1}). No Lean. Wenyuan Li’s seminar talk presents it ‘assuming the counterexample is correct’.

  83. 345 Infinitely many closed geodesics on Riemannian spheres and closed three-manifolds

    Awaiting review; here: Infinitely many closed geodesics on every sphere, claimed and re-proved

    Infinitely many closed geodesics for every metric on every sphere and every closed 3-manifold. Chen–Deng–Zhang give an independent, Codex-assisted proof, extended to projective spaces.

  84. 350 Yau’s nodal bounds: surfaces and higher dimensions

    Lean Awaiting review; here: OpenAI: Yau’s nodal bound holds on surfaces, fails in higher dimensions

    Yau’s nodal upper bound proved on smooth surfaces, disproved for smooth metrics in dimensions 3–5. Lean for all three Comparator-accepted.

  85. 362 Global smoothness for relativistic Vlasov–Maxwell

    Lean Awaiting review; here: OpenAI claims global smoothness for 3D relativistic Vlasov–Maxwell (Lean)

    Large-data global smooth solutions of 3D relativistic Vlasov–Maxwell; Lean full statement accepted in 2 runs. Reasoning summary; Xie: small exponent margin. No expert reaction. Own entry.

  86. 369 The hot spots conjecture for simply connected planar domains

    Lean Awaiting review; here: OpenAI claims the planar hot spots conjecture (Lean)

    Strict hot spots for smooth simply connected planar domains; Lean accepted. Burdzy and Bañuelos (ChatGPT) extend it to rough domains, unchecked; Atar–Burdzy 3D counterexample. Own entry.

  87. 375 De Giorgi’s conjecture in dimension eight

    Awaiting review; here: OpenAI claims De Giorgi’s conjecture in dimension eight, AI-assisted results in the 26 Oct 2026 sweep

    De Giorgi’s conjecture in dimension eight and stable Allen–Cahn solutions in ℝ⁷. No Lean; Long–Zou build on it. Own entry.

  88. 378 Disproof of the Exponential Time Hypothesis

    Lean Awaiting review; here: OpenAI claims ETH is false, Anthropic’s Claude also refutes ETH

    ETH refuted: subexponential exact #k-SAT, added 26 Oct. Lean for a weaker bound; Impagliazzo–Paturi–Williams working group. Own entries.

Known in their field 245

Named open problems that specialists know.

  1. 001 Milne’s rationality conjecture and algebraic specialization

    Awaiting review; here: OpenAI release proves the rational Hodge conjecture for all CM abelian varieties, giving the Tate conjecture for abelian varieties over finite fields; Lean proof added 26 Oct, human-written proof by van Hoften and Sempliner, and Milne calls it proved

    Milne’s rationality conjecture for abelian varieties with good reduction. Milne: ‘it seems, the statements in the article are now proven’; Madapusi wrote an improved exposition.

  2. 009 Function-field reconstruction from Milnor K-theory and Galois data

    Lean Awaiting review

    Function fields recovered from mod-ℓ Milnor K-theory; Bogomolov–Pop reconstruction. Lean covers uniqueness only. AHGT seminar talks announced on these manuscripts.

  3. 010 Unrestricted pro-modularity at the prime two

    Awaiting review

    Fontaine–Mazur for odd 2-dimensional 2-adic representations without residual hypotheses. Calegari: main difficulties ‘technical’; it is an input to the Hilbert-tenth proof.

  4. 011 Prime-factor statistics of $`p-1`$

    Awaiting review; here: Lü, Wang & Wu claim µ(p+2) = o(π(x)), a model case of the parity problem open since at least 1989, building on an OpenAI preprint with ChatGPT’s help, Mid-October 2026: arXiv results with disclosed AI help

    Poisson–Dirichlet law for prime factors of p−1 (Ford–Konyagin–Luca) and totients with n^(1−ε) preimages (Erdős #821, per Bloom). Lü–Wang–Wu build on it.

  5. 012 Independent largest prime factors of consecutive integers

    Lean Awaiting review

    Erdős–Pomerance: largest prime factors of n and n+1 asymptotically independent; P⁺(n) < P⁺(n+1) has density 1/2 (Erdős #371). Lean main accepted.

  6. 013 Ostmann’s inverse Goldbach conjecture

    Lean Awaiting review

    Ostmann’s inverse Goldbach: no finite modification of the primes is a sumset A+B (Erdős #431). Lean main. Leonetti and Elsholtz–Stadlmann follow up.

  7. 014 Restricted geometric Langlands, global Arthur enhancements, and generic Ramanujan

    Awaiting review

    Restricted geometric Langlands in characteristic p and Ramanujan for generic cuspidal exceptional-group representations over function fields. Eight manuscripts; no expert comment found.

  8. 015 Torus-packet equidistribution in prime, quartic, and sextic degrees

    Lean Awaiting review

    Haar equidistribution of torus packets in prime degree ≥ 5 and primitive quartic and sextic fields. Lean covers the prime-degree theorem.

  9. 018 The Margulis–Platonov conjecture over global fields

    Awaiting review

    Margulis–Platonov conjecture on noncentral normal subgroups of G(k) over every global field, including characteristic 2. No expert comment found.

  10. 020 Squarefree quartics and power-free polynomial values

    Lean Awaiting review

    Squarefree values of irreducible quartics with predicted density; (d−2)-free values in degrees 4–8, covering all d ≥ 4 with Browning. Lean main accepted.

  11. 021 A quadratic bound for Jacobsthal’s function

    Lean Awaiting review

    Jacobsthal’s function: every Ck² consecutive integers contain one coprime to any number with k prime factors. Lean, with a log-log refinement.

  12. 022 The weak inhomogeneous Duffin–Schaeffer conjecture

    Awaiting review

    Weak inhomogeneous Duffin–Schaeffer conjecture for every real shift. Manuscript only; no expert comment found.

  13. 023 Patterson’s first moment for cubic Gauss sums

    Lean Awaiting review; here: AI-assisted results in the 19 Oct 2026 arXiv listing

    Unconditional Patterson first moment for cubic Gauss sums over primary Eisenstein primes. Lean main; a 19 Oct arXiv paper uses its character moments.

  14. 024 An asymptotic formula for the number of totients

    Lean Awaiting review

    Asymptotic formula for the number of totients up to x; V(cx)/V(x) → c answers Erdős–Hall (Erdős #416, per Bloom). Lean main.

  15. 025 Short Egyptian fractions

    Lean Confirmed by an independent expert

    Erdős: every a/b is a sum of O(log log b) distinct unit fractions (#304). Lean. Bloom–van Doorn human exposition and simplification; erdosproblems credits it.

  16. 026 Positive lower density of large prime gaps

    Lean Awaiting review

    A positive proportion of prime gaps exceed C·log p for each C; answers Erdős–Prachar (#968). Lean covers only the p_n/n corollary.

  17. 031 Uchida’s conjecture for open homomorphisms of Galois groups

    Awaiting review

    Uchida’s conjecture: open homomorphisms between solvably closed Galois groups of number fields come from field embeddings. No expert comment found.

  18. 036 Numerical semiampleness and generalized minimal models

    Updated by OpenAI; here: OpenAI claims the abundance conjecture; Jihao Liu raises priority

    Numerical semiampleness of nef generalized adjoints; minimal models for generalized lc pairs. Kähler paper revised 7 Oct; listed in the abundance entry.

  19. 037 The ordinary-double-point volume gap

    Awaiting review

    Ordinary-double-point volume gap: singular klt germs have normalized volume ≤ 2(n−1)ⁿ, equality only for ordinary double points. No expert comment found.

  20. 041 Hyperkähler SYZ and projective-space bases

    Awaiting review; here: Engel & Mauri post a 7-page proof of the hyperkähler SYZ conjecture, two days after OpenAI’s catalogue claimed it; AI used only to proofread

    Strong hyperkähler SYZ (nef isotropic classes semiample) and projective-space bases of Lagrangian fibrations. Engel–Mauri posted an independent human proof.

  21. 042 Oka classification for minimal compact complex surfaces: Kodaira dimension zero and class VII

    Awaiting review

    Every complex K3 surface is Oka; Oka classification of minimal class VII surfaces. An et al. (arXiv 2610.10475) credit its local-to-global argument.

  22. 043 P = W for fixed-determinant SL<sub>n</sub> moduli spaces

    Awaiting review

    Fixed-determinant P = W in composite rank, completing all coprime ranks with the known prime-rank cases. No comment found.

  23. 044 The equivariant cohomological Hikita conjecture

    Awaiting review

    Equivariant cohomological Hikita conjecture for all quivers. Ben Webster’s GitHub repo Hikita-AI hosts a reader’s guide and rewrite, with text contributed by Hiraku Nakajima.

  24. 046 Shafarevich counterexamples in dimension two and with large fundamental group

    Awaiting review

    Counterexamples to Shafarevich’s holomorphic convexity conjecture: a projective surface and a fourfold with large fundamental group. No expert comment found.

  25. 048 A characteristic-zero counterexample to Lipman–Zariski

    Awaiting review

    Characteristic-zero counterexample to the Zariski–Lipman conjecture: a singular normal surface with free tangent sheaf. Manuscript only.

  26. 049 A stable-coordinate counterexample in four variables

    Lean Awaiting review

    A stable coordinate that is not a coordinate in four variables; Abhyankar–Sathaye counterexample. Lean main accepted.

  27. 050 A counterexample to Griffiths’ positivity conjecture

    Lean Awaiting review

    Ample rank-two bundles on P¹×P¹ without Griffiths-positive metrics, disproving Griffiths’ positivity conjecture. Lean main.

  28. 051 Kobayashi’s canonical-ampleness conjecture

    Awaiting review

    Kobayashi: compact Kähler manifolds without entire curves have ample canonical bundle. Qin–Tian cite it in arXiv 2609.25762 v5.

  29. 052 Tangent splittings and product decompositions

    Lean Awaiting review

    Beauville splitting for two integrable summands and Höring’s integrability conjecture on rationally connected manifolds. Lean main.

  30. 053 A counterexample to Pixton completeness in Chow

    Awaiting review

    A tautological relation vanishing in Chow but outside Pixton’s span disproves Pixton’s completeness conjecture. Johannes Schmitt signed up to digest it.

  31. 055 Gepner symmetry and large-volume stability on threefolds

    Awaiting review

    Toda’s Gepner stability condition on every quintic threefold; large-volume Bridgeland stability on all Calabi–Yau threefolds. No expert comment found.

  32. 056 Termination of projective and Kähler fourfold minimal model programs

    Updated by OpenAI; here: OpenAI claims the abundance conjecture; Jihao Liu raises priority

    Termination of MMPs for projective lc fourfolds and Kähler fourfolds; three manuscripts revised 7 Oct. Listed in the abundance entry.

  33. 057 Fundamental groups of special complex varieties and root orbifolds

    Awaiting review

    Campana’s abelianity conjecture: special compact Kähler manifolds have virtually abelian fundamental groups. No expert comment found.

  34. 058 Semialgebraic universal covers and bounded domains

    Lean Awaiting review

    Kollár–Pardon conjecture on semialgebraic universal covers. Lean covers the bounded-symmetric-domain companion only.

  35. 059 Counterexamples to Zariski’s multiplicity conjecture

    Awaiting review

    Counterexamples to Zariski’s 1971 multiplicity conjecture: ambiently homeomorphic hypersurface germs with different multiplicities. Manuscript only.

  36. 060 The Global Spherical Shell conjecture

    Awaiting review

    Global spherical shell conjecture for class VII surfaces with b₂ > 0, completing their classification modulo known cases. No expert comment found.

  37. 062 Projective contact classification and the LeBrun–Salamon conjecture

    Awaiting review; here: Two claimed proofs of the LeBrun–Salamon conjecture

    LeBrun–Salamon conjecture and projective contact classification. Hu–Liu–Wan posted an independent proof; covered by our two-proofs entry.

  38. 063 The generalized Mukai conjecture

    Awaiting review

    Generalized Mukai conjecture ρ(ι−1) ≤ n for Fano manifolds. Pearson’s arXiv v2 (2604.25023) notes the claim.

  39. 064 Topological triviality of μ-constant surface singularities

    Awaiting review

    Surface case of the μ-constant (Lê–Ramanujam) problem: μ-constant families in ℂ³ are topologically trivial. Manuscript only.

  40. 065 Virasoro constraints for complete intersections and projective-bundle towers

    Awaiting review

    Virasoro constraints for smooth complete intersections and projective-bundle towers in all genera. No expert comment found.

  41. 066 Bounded klt complements for Fano contractions

    Lean Awaiting review

    Shokurov’s bounded klt complements for ε-lc Fano contractions. Lean covers a local compactness lemma only.

  42. 067 The Campana–Peternell conjecture in dimension six

    Awaiting review

    Campana–Peternell conjecture in dimension six: Fano sixfolds with nef tangent bundle are rational homogeneous. Manuscript only.

  43. 069 Global quantum geometric Langlands at irrational level

    Awaiting review

    Quantum geometric Langlands equivalence at irrational level for simple groups. An automated referee report (OSVerify) flags issues.

  44. 071 Koebe’s circle-domain conjecture

    Lean Awaiting review

    Koebe’s 1908 circle-domain conjecture (existence) and the removability-to-rigidity half of He–Schramm. Lean covers both. No expert comment found.

  45. 075 The $`L\log L`$ Fourier-convergence conjecture

    Lean Awaiting review

    Fourier partial sums of every L log L function converge almost everywhere, the classical endpoint question beyond Carleson–Hunt. Lean main. No expert comment found.

  46. 076 Real ultraflat Littlewood polynomials and unbounded binary merit factors

    Lean Awaiting review

    Ultraflat ±1 polynomials at every large length; disproves Turyn’s bounded merit factor conjecture (Erdős #1150). Lean; el Abdalaoui disputes one scope.

  47. 080 The exact Sobolev endpoint for Schrödinger convergence

    Awaiting review; here: OpenAI claims 3D restriction and Bochner–Riesz conjectures

    Sharp Sobolev endpoint H^{n/(2(n+1))} of Carleson’s Schrödinger convergence problem in every dimension. Manuscripts only.

  48. 081 Riesz transforms and rectifiability in higher codimension

    Lean Awaiting review

    Bounded Riesz transforms imply uniform rectifiability in the remaining higher codimensions (David–Semmes problem). Lean main. Hoffman–Jaye cite it.

  49. 082 Annular variation and dyadic absolute bounds for the triangular Hilbert transform

    Lean Awaiting review

    Maximal and variational L³×L³→L^{3/2} bounds for the triangular Hilbert transform at the symmetric point. Lean main.

  50. 083 Hilbert transforms along Lipschitz directions

    Lean Awaiting review

    Short-scale L² bound for Hilbert transforms along Lipschitz vector fields, a form of Stein’s conjecture. Lean main.

  51. 084 The geometric case of the Erdős similarity conjecture

    Lean Awaiting review

    Erdős similarity conjecture for geometric sequences of every ratio (#120). Lean covers the dyadic case; Jiang–Xi extend the construction.

  52. 085 Endpoint Sobolev regularity of centered disk averages

    Lean Awaiting review

    Hajłasz–Onninen problem for the planar centered disk maximal function: ‖∇Mf‖₁ ≤ C‖∇f‖₁. Lean main.

  53. 086 An L<sup>3</sup> bound for the trilinear Hilbert transform

    Awaiting review

    L³×L³×L³ → L¹ bound for the trilinear Hilbert transform with slopes 1, 2, 3. OSVerify’s automated report lists issues.

  54. 088 Sharp projection-body inequalities and a counterexample to simplex maximization

    Lean Awaiting review

    Petty’s projection-volume conjecture for n ≥ 4, Lutwak–Petty inequalities, and a counterexample to Brannen’s simplex conjecture. Lean main.

  55. 089 Bounded-distortion L<sub>1</sub> embeddings of planar and bounded-treewidth graphs

    Lean Awaiting review

    Planar and bounded-treewidth cases of the Gupta–Newman–Rabinovich–Sinclair L1-embedding conjecture. Lean main. Hung Le is reading the planar proof.

  56. 091 Logarithmic and L<sub>p</sub> Brunn–Minkowski inequalities and the B-conjecture

    Lean Awaiting review

    Logarithmic Brunn–Minkowski conjecture for symmetric bodies and the B-conjecture for even log-concave measures. Lean main; Livshyts explores it.

  57. 092 The optimal order of convex-body covering density

    Lean Awaiting review

    Worst-case covering density of convex bodies is Θ(n log n), lattice and translative. Lean main; Kalai lists it.

  58. 094 Subpolynomial dimension reduction in L<sub>p</sub>

    Lean Awaiting review

    Subpolynomial dimension reduction in L_p for p ≠ 2 at any distortion D > 1, answering Naor’s question. Lean main.

  59. 095 Hyperbolicity cones without semidefinite lifts

    Lean Awaiting review

    A hyperbolicity cone that is not a spectrahedral shadow disproves the generalized and projected Lax conjectures. Lean main; Kevin Shu’s exposition.

  60. 096 The Gaussian propeller conjecture in every dimension

    Lean Confirmed by an independent expert; here: Heilman simplifies OpenAI’s propeller conjecture proof

    Khot–Naor Gaussian propeller conjecture in every dimension, Lean. Heilman simplified the proof and treats it as proved.

  61. 097 The Euclidean Steinitz–Bergström bound

    Lean Awaiting review

    Euclidean Steinitz–Bergström constant is Θ(√d). Lean main; Russo–Wei cite it.

  62. 098 Compact counterexamples to bi-Lipschitz dimension reduction

    Lean Awaiting review

    Compact doubling subsets of every infinite-dimensional Banach space with no bi-Lipschitz embedding into finite dimensions (Lang–Plaut). Lean main.

  63. 099 The sharp exponential scale of edit-distance distortion

    Lean Awaiting review

    ℓ1 distortion of edit distance is exp(Θ(√(log d log log d))). Lean main.

  64. 100 Cylinder coverings below the half-area bound

    Lean Awaiting review

    Finite cylinder covers of the regular tetrahedron below the half-area bound disprove Bang’s conjecture. Lean; Pinho gives an explicit 4,096-cylinder cover.

  65. 101 The sharp simplex conjecture for isotropic constants

    Awaiting review

    Simplices uniquely maximize the isotropic constant (strong slicing conjecture); sharp entropy bound for log-concave laws. Manuscript only.

  66. 104 Quasipolynomial algorithms for mean-payoff, stochastic and parity games

    Lean Awaiting review

    Deterministic quasipolynomial algorithms for mean-payoff, stochastic mean-payoff and mean-payoff parity games. Lean covers the randomized version only.

  67. 105 Perfect completeness for 2-to-1 games

    Lean Awaiting review; here: OpenAI model claims a proof of Khot’s Unique Games Conjecture, with Lean formalization

    Khot’s 2-to-1 Games Conjecture with perfect completeness, Lean. Fei–Minzer–Wang posted a 4-to-1 version on 14 Sep (in the UGC entry).

  68. 108 A cubic permanent–determinant lower bound

    Lean Awaiting review

    Ω(n³) lower bound for the border determinantal complexity of the permanent (best was quadratic). Lean main; Guo reuses its Lean declarations.

  69. 110 Optimal-order randomized k-server on arbitrary metrics

    Lean Awaiting review

    Randomized k-server O(log²k) on every metric, matching the known lower-bound order. Lean main; configuration changed 26 Oct.

  70. 111 One-sample matroid prophet inequalities against an almighty adversary

    Lean Awaiting review

    One-sample matroid prophet inequality with constant ratio against an almighty adversary. Lean (2^−310); bottlebrushes PR improves to 2^−38.

  71. 112 Beyond the square-root exponent for depth-three circuits

    Lean Awaiting review

    Explicit language requiring 2^{ω(√n)} depth-3 circuits, past the square-root barrier. Lean main. Chukhin (ECCC) and Li–Zhong extend it; Goldreich comments.

  72. 114 Approximate counting of common integer polymatroid bases

    Lean Awaiting review

    FPRAS for common bases of two matroids and integer polymatroids, Lean. Chen–Liu (arXiv 2610.06724, 5 Oct) independently claim the matroid case.

  73. 115 Sampling and counting contingency tables with arbitrary margins

    Lean Awaiting review

    Exact uniform sampling and FPRAS counting of contingency tables with arbitrary margins and cell bounds. Lean main.

  74. 116 Uniform black-box noncommutative identity testing across characteristics

    Lean Awaiting review

    Deterministic black-box identity testing for noncommutative formulas in every characteristic. Lean main.

  75. 117 Uniform sparsest cut: hardness and semidefinite gaps

    Lean Awaiting review

    Constant-factor NP-hardness of uniform sparsest cut and near √log n SDP gaps. Lean covers the integrality gaps only.

  76. 118 Bin packing and unbounded configuration-LP gaps

    Lean Awaiting review

    Bin packing: configuration-LP additive gap unbounded (MIRUP false); fixed additive approximation NP-hard. Lean main.

  77. 119 The Courtade–Kumar and Hellinger conjectures

    Lean Awaiting review; here: Courtade–Kumar ‘most informative Boolean function’ conjecture (2013) proved three times in two days, all with AI: Ky & Tran (ChatGPT), Google + CUHK (Gemini, Lean-verified end-to-end), Mahdavifar & Beirami

    Courtade–Kumar and Hellinger conjectures, Lean. Courtade–Kumar had been proved three times in September; Ky proves the antipodal Hellinger case.

  78. 120 Almost-linear-time exact matching and prescribed-degree factors in general graphs

    Awaiting review

    Randomized almost-linear-time maximum matching and prescribed-degree factors in general graphs. Manuscript only.

  79. 121 Almost-linear approximation of edit distance

    Lean Awaiting review

    (1+ε)-approximation of edit distance in N^{1+o(1)} time. Lean main; Hu–Kociumaka–Nogler–Saha footnote it as claimed.

  80. 122 Quantitative trace-reconstruction bounds with a uniform decoder

    Lean Awaiting review

    Worst-case trace reconstruction needs n^{Ω(log log n)} traces; quasipolynomial uniform decoder. Lean covers the lower bound.

  81. 125 The metric k-median approximation threshold and recovery

    Lean Awaiting review; here: OpenAI model claims tight 1 + 2/e approximation for k-median, k-median breaks the factor-2 barrier

    Tight (1+2/e+ε) approximation for metric k-median, Lean. Svensson: ‘completely solved a problem’ his students worked on; EPFL group posts other algorithms.

  82. 126 Exponential semidefinite complexity of perfect matching

    Lean Awaiting review

    Claims every exact semidefinite lift of the perfect-matching polytope has exponential size (Rothvoss’s question); Lean proves only superpolynomial bounds.

  83. 127 Average sensitivity of polynomial threshold functions

    Lean Awaiting review

    Claims average sensitivity of degree-d polynomial threshold functions is at most 8d√n, the asymptotic Gotsman–Linial conjecture; Lean-formalized.

  84. 128 A factor-two approximation for shortest common superstring

    Lean Awaiting review

    Claims a polynomial-time factor-2 approximation for shortest common superstring; Lean-formalized; several community implementations benchmark it against greedy.

  85. 129 Exponential state costs for two-way automata

    Lean Awaiting review

    Claims exponential lower bounds for 2NFA complementation and for simulating 1NFAs by 2DFAs over growing alphabets (Sakoda–Sipser); both Lean-formalized.

  86. 131 Rapid mixing of graph switches for every degree sequence

    Lean Awaiting review

    Claims the switch chain mixes in O(n⁸) for every graphical degree sequence (Kannan–Tetali–Vempala conjecture); Lean-formalized mixing bound.

  87. 132 A superquadratic separation of sensitivity and block sensitivity

    Lean Awaiting review

    Disproves the quadratic sensitivity vs block-sensitivity bound (bs ≥ s^α, α > 2); Lean; Kothari and others raised α past 2.13 with Lean.

  88. 134 Generalized star height at most three

    Lean Awaiting review

    Claims every regular language has generalized star height at most 3 (uniform bound in the generalized star-height problem); Lean-formalized; height 1 vs 2 untouched.

  89. 136 A quasilinear PCP theorem for PPAD

    Awaiting review

    Claims the quasilinear PCP-for-PPAD conjecture; only partial Lean; Daskalakis et al. (arXiv 2610.28141) cite the claim but do not rely on it.

  90. 138 Subset Sum in $`O(2^{0.49n})`$ time

    Awaiting review

    Claims worst-case Subset Sum in randomized O(2^0.49n) time, beating meet-in-the-middle; no Lean; Kapila claims 0.4877 building on it (Hexagon).

  91. 141 Existential–universal real sentences in the counting hierarchy

    Awaiting review

    Claims the existential theory of the reals lies in the counting hierarchy; no Lean; Bürgisser notes ‘several ChatGPT generated papers’ claiming this.

  92. 144 Banach’s simple Lebesgue-spectrum problem

    Lean Awaiting review

    Claims a smooth volume-preserving T³ diffeomorphism with simple Lebesgue spectrum, answering Banach’s problem in smooth dynamics; Lean; no expert reaction found.

  93. 146 Positive metric entropy for the standard map

    Lean Awaiting review

    Claims positive metric entropy of the Chirikov standard map for all large parameters (Sinai’s conjecture); Lean; Oliver Knill notes small parameters remain open.

  94. 147 The near-boundary Birkhoff conjecture

    Awaiting review

    Claims the near-boundary Birkhoff conjecture: a foliated grazing collar of caustics forces an ellipse; no Lean; no expert reaction found.

  95. 148 The entropy-rate dimension formula for self-similar measures

    Lean Awaiting review; here: Exact overlaps conjecture for self-similar measures on the line proved, OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems

    Claims the exact-overlaps dimension formula for self-similar measures on the line; Lean; Kittle–Kogler’s independent AI-found, human-rewritten proof has its own entry.

  96. 149 Classwise permanence for weakly reversible mass-action systems

    Lean Awaiting review; here: AI-assisted results in the 23 Oct 2026 arXiv listing

    Claims the permanence conjecture for weakly reversible mass-action systems; Lean; Mislan and Lv et al. reuse its Lean development (mention in 23 Oct listing).

  97. 150 Weak mixing of triangular billiards with an irrational angle

    Lean Awaiting review

    Claims every triangular billiard with an irrational angle is weakly mixing; ergodicity is Lean-formalized; previously known only for generic triangles.

  98. 151 A C<sup>1</sup> counterexample to the entropy conjecture

    Lean Confirmed by an independent expert; here: oai-math-revised: mathematicians launch a community hub to revise OpenAI’s AI-written math manuscripts (guest post on Tao’s blog)

    Disproves Shub’s entropy conjecture for C¹ self-maps; Lean; Andrey Gogolev wrote an elementary account extending the construction to every finite C^r.

  99. 152 Zero entropy does not guarantee a smooth positive-volume model

    Lean Awaiting review

    Claims a zero-entropy system with no smooth positive-volume model (smooth realization problem); Lean proves only a finite-entropy version.

  100. 153 Arithmetic classification and non-Pisot singularity for Bernoulli convolutions

    Awaiting review

    Claims an arithmetic classification of singular Bernoulli convolutions and singularity at quartic Salem reciprocals; no Lean; Kogler plans an exposition; follow-ups cite it.

  101. 154 Pointwise multiple ergodic averages for mixing transformations

    Awaiting review

    Claims a.e. convergence of multiple ergodic averages for mixing transformations (Furstenberg’s question, mixing case); four manuscripts; no Lean; no reaction found.

  102. 160 Superexponential van der Waerden numbers

    Lean Awaiting review

    Claims W_r(k) > k^(ck log r), so W_2(k)^(1/k) → ∞ (Erdős #138); Lean; Bloom notes Fox–Hunter had r ≥ 3 by similar methods.

  103. 162 Counterexamples to Ryser’s covering conjecture

    Lean Awaiting review

    Claims intersecting (q+1)-partite hypergraphs needing q+1 cover vertices, disproving Ryser’s conjecture and Gyárfás’s tree-cover conjecture; Lean; no explicit instance.

  104. 164 Hindman’s finite sums and products conjecture

    Awaiting review

    Claims Hindman’s finite sums-and-products conjecture over the integers; no OpenAI Lean, but Yao Xu’s AI-assisted Lean proof is linked by formal-conjectures (Erdős #172).

  105. 166 The higher-dimensional Erdős distinct-distances conjecture

    Awaiting review

    Claims ≫ n^(2/d) distinct distances in every dimension d ≥ 3 (Erdős #1083); no OpenAI Lean; Bloom notes it builds on Tidor–Yu–Zakharov.

  106. 169 Shareshian–Wachs elementary positivity

    Lean Awaiting review

    Claims Shareshian–Wachs e-positivity of chromatic quasisymmetric functions; Lean (config fixed 26 Oct); Swanson calls it opaque and independent of Hikita’s proof.

  107. 170 Sharp logarithmic exponents for off-diagonal Ramsey numbers

    Lean Awaiting review

    Claims r(s,t) = t^(s−1)/(log t)^(s−2+o(1)) for s ≥ 5, sharpening Bradač’s 2026 exponent; Lean; Lin–Zhang use it for r(4,t).

  108. 171 The hypercube Ramsey conjecture

    Awaiting review

    Claims the hypercube Ramsey number is O(2^n) (Burr–Erdős); no OpenAI Lean, but Yao Xu’s AI-assisted Lean proof is linked by formal-conjectures (Erdős #181).

  109. 172 Classification of finite Euclidean Ramsey configurations

    Lean Awaiting review

    Claims a tensor-criterion classification of finite Euclidean Ramsey configurations, disproving Leader–Russell–Walters; Lean; several Lean follow-ups build on it.

  110. 173 Seymour’s second-neighborhood conjecture

    Lean Awaiting review

    Claims Seymour’s second-neighbourhood conjecture for all oriented graphs; Lean-formalized; no expert assessment found.

  111. 174 Deterministic construction of strong thin spanning trees

    Lean Awaiting review

    Claims Goddyn’s strong thin-tree conjecture with a deterministic polynomial-time construction; Lean-formalized; no reaction found.

  112. 175 Talagrand’s expectation thresholds, discrete convexity, and graph decompositions

    Lean Awaiting review

    Claims Talagrand’s expectation-threshold equivalence and discrete-convexity conjectures; Lean; Fang–Wang’s v2 says OpenAI’s result supersedes their log-star bound.

  113. 176 The second Kahn–Kalai conjecture with an edge-count bound

    Lean Awaiting review

    Claims the second Kahn–Kalai conjecture with a 1 + log₂h factor; Lean-formalized; Kalai listed it among related results.

  114. 177 Bounded-degree coboundary expanders

    Lean Awaiting review

    Claims bounded-degree F₂ coboundary expanders in every dimension ≥ 3; Lean; Michael Chapman counts it among problems he ‘grew up on’.

  115. 178 Deterministic nonbipartite Ramanujan graphs in every fixed degree

    Awaiting review

    Claims deterministic nonbipartite Ramanujan graphs for every degree ≥ 3; no Lean; a public gist alleges a gap in Theorem 8.3.

  116. 179 The circulant Hadamard and Barker-sequence conjectures

    Lean Awaiting review

    Claims Ryser’s circulant Hadamard conjecture (orders 1 and 4 only) and the Barker-sequence classification; Lean; formal-conjectures marks it solved.

  117. 181 The Erdős–Gallai cycle-decomposition conjecture

    Lean Confirmed by an independent expert; here: Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help, OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems, October 2026: the arXiv stream of conjectures settled with disclosed AI help continues

    Claims O(n) cycle-and-edge decompositions (Erdős–Gallai); Lean; Jaehoon Kim proved it independently with AI help (arXiv 2610.07840).

  118. 182 Power savings for intersective polynomial differences and prime arguments

    Lean Awaiting review

    Claims power-saving Sárközy-type bounds for intersective polynomial differences; Lean for squares; Fan–Lott call the draft ‘largely unreadable’.

  119. 183 Power savings for planar halving lines and k-sets

    Lean Awaiting review

    Claims O(n^(4/3−ε)) halving lines for points with no three collinear, improving Dey’s bound; Lean-formalized; constants non-explicit.

  120. 184 Correspondence coloring with a fixed forbidden subgraph

    Lean Awaiting review

    Claims the Ajtai–Erdős–Komlós–Szemerédi independence conjecture and Alon–Krivelevich–Sudakov colouring; Lean for independence; Bloom notes it beats Shearer.

  121. 185 Counterexamples to infinite matroid intersection and packing/covering

    Lean Awaiting review

    Disproves unrestricted infinite matroid intersection and packing/covering conjectures in ZFC; Lean; Nash-Williams’s finitary version untouched.

  122. 186 Uniform influence and sharp thresholds for graph and hypergraph properties

    Lean Awaiting review

    Claims Friedgut–Kalai threshold-width bounds for symmetric graph and hypergraph properties; Lean for graphs; Kalai highlighted it.

  123. 187 Snaky in 21 Maker moves

    Lean Confirmed by an independent expert

    Settles Harary’s Snaky game: Maker wins within 21 moves; Lean; Nándor Sieben built proof sequences from it (20 moves); later 19.

  124. 188 The sharp terminal leave in random triangle removal

    Lean Confirmed by an independent expert

    Claims random triangle removal leaves ~n^(3/2)/(2√2) edges (Joos–Kühn constant); Lean; Keevash proved it independently with essentially the same method.

  125. 189 Cycle–clique Ramsey numbers

    Lean Awaiting review

    Claims the Erdős–Faudree–Rousseau–Schelp formula R(C_m,K_n) = (m−1)(n−1)+1 for all m ≥ n ≥ 3; Lean-formalized (Erdős #551).

  126. 191 A power improvement in the Heilbronn triangle lower bound

    Lean Awaiting review

    Claims n points with every triangle of area ≥ n^(−2+c), refuting the conjectured n^(−2+o(1)) Heilbronn upper bound; Lean-formalized.

  127. 194 Lech’s multiplicity conjecture

    Lean Awaiting review

    Claims Lech’s multiplicity conjecture in all dimensions and characteristics; Lean covers a supporting lemma; Iyengar–Ma–Walker had an AI-found equal-characteristic proof.

  128. 195 A counterexample to the small Cohen–Macaulay module conjecture

    Lean Awaiting review; here: Hochster’s 1973 small Cohen–Macaulay conjecture

    Counterexample to Hochster’s small Cohen–Macaulay module conjecture (domain form); Lean covers only the ring; Anghel’s survey; own entry.

  129. 198 A counterexample to finitistic-dimension finiteness

    Lean Awaiting review

    Claims a finite-dimensional algebra of infinite little finitistic dimension, refuting the finitistic dimension conjecture; Lean; Tang extended it to all fields.

  130. 199 Counterexamples to Auslander–Reiten, Tachikawa and related homological conjectures

    Lean Awaiting review

    Claims counterexamples to Auslander–Reiten, Tachikawa and Nakayama-type conjectures; Lean; Marczinzik urges careful checking; Tang and Kitamura extend them.

  131. 200 Eisenbud–Green–Harris and lex-plus-powers

    Awaiting review

    Claims the Eisenbud–Green–Harris and lex-plus-powers conjectures in characteristic zero; no Lean; no expert reaction found.

  132. 201 A counterexample to Kurosh’s division-ring problem

    Awaiting review

    Claims an algebraic two-generated division ring of infinite dimension, answering Kurosh’s problem negatively; no catalogued Lean; no expert reaction found.

  133. 203 Donovan’s conjecture over fields and complete mixed-characteristic DVRs

    Awaiting review

    Claims Donovan’s conjecture over algebraically closed fields and its integral form over complete DVRs; no Lean; no reaction found.

  134. 205 Saxl’s conjecture and universal tensor squares

    Lean Awaiting review

    Claims Saxl’s conjecture and universal tensor squares for S_n (n ∉ {2,4,9}); Lean-formalized; volunteers re-derived parts.

  135. 206 Finite lattice representation and undecidability

    Lean Awaiting review

    Claims some finite lattices are not congruence lattices of finite algebras, plus undecidability; Lean; DeMeo’s AI-assisted reading found the negative answer sound.

  136. 207 The ℓ¹-Bass conjecture for all discrete groups

    Lean Awaiting review; here: Kaplansky’s zero-divisor and direct-finiteness conjectures refuted? (OpenAI, Lean)

    Claims the ℓ¹-Bass conjecture and Kaplansky’s idempotent conjecture in characteristic zero; Lean; Chatterji doubts it, Sauer calls it ‘deeply creative’.

  137. 208 Finite symmetric tensor categories and the Verlinde tower

    Confirmed by an independent expert; here: Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help, October 2026: the arXiv stream of conjectures settled with disclosed AI help continues

    Claims the finite Benson–Etingof–Ostrik conjecture; Coulembier and Flake proved it first with GPT-6 Astra help (arXiv 2610.04096); no Lean.

  138. 209 Integral counterexamples to Gersten’s conjecture

    Awaiting review

    Claims integral counterexamples to Gersten’s conjecture for ramified mixed-characteristic (0,5) regular local rings; no Lean; no reaction found.

  139. 210 Foulkes’ conjecture for sixth powers and quadratic stabilization

    Lean Awaiting review

    Claims Foulkes’ conjecture for sixth powers and quadratic stabilization of the Foulkes–Howe map; Lean; a volunteer re-checked 6 ≤ b ≤ 25 by computer.

  140. 211 The geometric phase diagram, diffusion, and spectra of random planar maps

    Lean Awaiting review

    Claims FK planar maps converge to LQG (q≤4) or the Brownian tree (q>4); Lean for q>4; Holden’s independent work complements it.

  141. 212 Planar first-passage geometry and the absence of bigeodesics

    Lean Awaiting review

    Claims no bigeodesics in planar first-passage percolation and strict convexity of the exponential limit shape; Lean covers differentiability.

  142. 214 The Benjamini–Schramm nonuniqueness conjecture

    Lean Awaiting review

    Claims p_c < p_u on every nonamenable quasi-transitive graph (Benjamini–Schramm 1996); Lean; Tasmin Chu says it builds on Hutchcroft’s approach.

  143. 216 Critical and near-critical XY scaling and BKT universality

    Awaiting review

    Claims the critical XY correlation r^(−1/4)(log r)^(1/8) and the BKT essential singularity; six manuscripts; no Lean; no expert reaction found.

  144. 217 The low-temperature Sherrington–Kirkpatrick fluctuation law

    Awaiting review

    Claims n^(1/6) fluctuations and a limiting law for the low-temperature SK free energy; conditional Lean; Aronow–Lopatto reprove one step.

  145. 218 Conformal universality for weakly interacting and random-bond Ising models

    Lean Awaiting review

    Claims conformal (SLE₃) universality for weakly interacting and weak random-bond Ising models; Lean covers only a comparison lemma.

  146. 219 GOE bulk universality for regular graphs with weak Anderson disorder

    Confirmed by an independent expert

    Claims GOE bulk universality for fixed-degree random regular graphs, even cubic; He, Huang and Wang proved the clean case independently (arXiv 2610.08127).

  147. 220 Directional zero–one laws beyond iid environments and iid ballisticity

    Lean Awaiting review

    Claims directional zero–one laws (d ≥ 3) and ballisticity from directional transience for random walks in random environment; Lean-formalized.

  148. 221 The Mézard–Parisi formula for diluted spin glasses

    Lean Awaiting review; here: OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems

    Claims the Mézard–Parisi cavity formula for diluted even-arity spin glasses (Viana–Bray); Lean; OpenAI published a reasoning summary.

  149. 222 Perceptron free energies and microscopic jamming exponents

    Lean Awaiting review

    Claims perceptron free energies (Ising and spherical) and jamming exponents; Lean only for finiteness; Fu–Sohn’s independent draft overlaps.

  150. 224 Critical and quenched near-critical universality for Poisson–Voronoi percolation

    Awaiting review

    Claims Cardy’s formula for critical Poisson–Voronoi percolation and quenched near-critical universality; no Lean; no expert reaction found.

  151. 225 Gaussian free field limits throughout the balanced six-vertex regime

    Awaiting review

    Claims Gaussian free field limits for the balanced six-vertex model for all 0 < c ≤ 2, variance multiplier 1/arcsin(c/2); no Lean.

  152. 226 The double-dimer loop ensemble converges to CLE<sub>4</sub>

    Awaiting review

    Claims half-plane double-dimer loops converge to nested CLE₄ as curves (Temperleyan case of Kenyon’s conjecture); no Lean; no expert reaction found.

  153. 227 Critical SK autocorrelation processes and dynamics across the temperature transition

    Lean Awaiting review; here: October 2026: the arXiv stream of conjectures settled with disclosed AI help continues

    Claims SK Glauber mixing across the transition (cutoff, n^(2/3) at criticality); Lean for several; Du–Huang–Mohanty–Rajaraman and Hou–Liu–Yu treat it as concurrent work.

  154. 228 Continuum phase transitions for radial pair potentials

    Lean Awaiting review

    Claims stable radial pair potentials with a first-order continuum phase transition, the type sought in Barry Simon’s problem; Lean-formalized.

  155. 229 Exact three- and four-state reconstruction thresholds and four-state tree capacity

    Lean Awaiting review

    Claims exact Kesten–Stigum reconstruction thresholds for 3- and 4-state tree channels and the 3-community block-model threshold; partial Lean.

  156. 230 Exact Hausdorff gauges for SLE

    Lean Awaiting review; here: OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems

    Claims exact Hausdorff gauges for SLE_κ (Schramm’s question); partial Lean; Dapeng Zhan used the companion to identify natural length.

  157. 231 The free uniform spanning forest is a factor of IID

    Lean Awaiting review

    Claims the free uniform spanning forest is a factor of IID on every graph (Lyons’s question); Lean-formalized; no reaction found.

  158. 232 Gaussian fields and interfaces for triangular-lattice Lipschitz heights

    Updated by OpenAI; here: OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems

    Claims GFF limits for triangular-lattice Lipschitz heights and an SLE₄ interface; three manuscripts revised 7 Oct after proof repairs; no Lean.

  159. 236 The exact factor-of-IID threshold for free Ising spins on trees

    Lean Awaiting review

    Claims the free Ising state on d-regular trees is a factor of IID exactly when tanh β ≤ 1/√(d−1) (Lyons); Lean-formalized.

  160. 238 Optimal logarithmic mixing of the Thorp shuffle

    Lean Awaiting review

    Claims Θ(log N) mixing of the Thorp shuffle for N = 2^d cards, settling its order; 12 manuscripts with Lean; cutoff open.

  161. 239 Sharp singularity rates for symmetric random sign matrices

    Awaiting review

    Claims P(det A_n = 0) = (1/2+o(1))^n for symmetric random sign matrices, and the biased-sign rate; no Lean; no expert reaction found.

  162. 240 Shelah’s eventual categoricity and the prescribed-threshold obstruction

    Lean Awaiting review

    Claims Shelah’s eventual categoricity conjecture in ZFC; Lean covers only the CH obstruction; Espíndola disputes Proposition 7.2.

  163. 241 Rigidity of the Turing degrees

    Lean Confirmed by an independent expert; here: OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems

    Claims the Turing degrees are rigid; Lean; Andrew Marks re-proved the key lemma; Kjos-Hanssen adapted it to truth-table degrees.

  164. 242 Single-fold Diophantine representations and undecidability under an at-most-one-solution promise

    Lean Awaiting review

    Claims every r.e. set has a single-fold Diophantine representation (Davis–Matiyasevich–Robinson question); Lean-formalized; no reaction found.

  165. 243 Separating choiceless counting from polynomial time and witnessed choice

    Lean Awaiting review

    Claims choiceless polynomial time with counting does not capture PTIME (Blass–Gurevich–Shelah); Lean-formalized; no reaction found.

  166. 245 Weak normalization implies strong normalization in pure type systems

    Lean Awaiting review

    Claims weak normalization implies strong normalization for all pure type systems (Barendregt–Geuvers–Klop); Lean-formalized; no reaction found.

  167. 249 A finitely generated Eilenberg–Ganea counterexample

    Lean Awaiting review

    Claims a finitely generated group with cohomological dimension 2 and geometric dimension 3, refuting Eilenberg–Ganea; Lean; Avramidi ties it to Bestvina–Brady.

  168. 250 Boone–Higman embeddings with higher finiteness

    Lean Awaiting review

    Claims the Boone–Higman conjecture with F∞ simple overgroups; Lean; Zaremsky says it shows his group’s sufficient condition always works.

  169. 251 Amenability, unitarizability, and strong Ulam stability

    Lean Awaiting review

    Claims Dixmier’s unitarizability problem (unitarizable groups are amenable) and strong Ulam stability. Lean covers Dixmier part. Kourovka 20.62: ‘unverified AI solution’.

  170. 253 An infinite finitely presented simple amenable group

    Lean Awaiting review

    Infinite finitely presented simple amenable group; Lean (existence) accepted. Zaremsky struck it from his list: ‘I’ll just cross out problems solved by AI.’

  171. 255 Quasi-isometric recognition of virtually polycyclic groups

    Lean Awaiting review

    Eskin–Fisher–Whyte conjecture: groups quasi-isometric to virtually polycyclic groups are virtually polycyclic. Lean scope note exists, Comparator accepted. No reactions found.

  172. 256 Nonsingular systems of equations over arbitrary groups

    Lean Confirmed by an independent expert; here: Kervaire’s conjecture: OpenAI proof confirmed in the Kourovka Notebook

    Kervaire’s conjecture and its nonsingular-systems extension (Howie). Kourovka 17.94 and 18.87(a): ‘AI solution confirmed by N. V. Bogachev’. Lean covers single-relator case. Own entry (30 Oct).

  173. 257 A hyperbolic group without a geometric CAT(0) action

    Lean Awaiting review

    Word-hyperbolic group with no geometric CAT(0) action, so not every hyperbolic group is CAT(0). Lean accepted; two-dimensionality not formalized. Lupini builds on it.

  174. 258 Gersten’s conjecture and virtual compact specialness of one-relator groups

    Awaiting review

    Gersten’s conjecture: Baumslag–Solitar-free one-relator groups are hyperbolic; hyperbolic ones virtually compact special. Kharlampovich–Miasnikov use it, explicitly conditionally.

  175. 259 A group without fixed price

    Awaiting review

    Negative answer to Gaboriau’s fixed price problem: a finitely generated group with free actions of different costs. No Lean; no reactions found.

  176. 262 Sharp finite-matrix Lieb–Thirring inequalities and all equality cases

    Lean Awaiting review

    Sharp one-dimensional Lieb–Thirring constant for 1/2<γ<3/2 (scalar conjecture), matrix version and equality cases. Lean (scalar constant) Comparator-accepted.

  177. 263 The ionization and generalized ionization conjectures

    Lean Awaiting review

    Ionization conjecture forms: molecules bind at most Z+CM electrons; universal ionization-energy and radius bounds; generalized asymptotics (Lean). Chen–Wu prove a TFDW analogue.

  178. 269 Uniform Laughlin gap and stability under bounded scalar disorder

    Lean Awaiting review

    Laughlin spectral-gap conjecture at filling 1/3, stable under weak disorder. Lean covers unperturbed gap. Qiang Gao’s SDP improves the bound from 1/25 to 1/5.

  179. 270 Threshold and positive-energy bound states of the BFSS matrix model

    Awaiting review

    BFSS matrix model: unique SU(N) threshold bound state; infinitely many SU(2) positive-energy bound states, contradicting the original BFSS paper. No Lean; no expert reaction found.

  180. 272 Entanglement without distillable secret key

    Lean Awaiting review

    Entangled state with zero distillable secret key; disproves Christandl’s PPT-squared conjecture with a 21-dimensional channel. Lean covers the PPT-squared counterexamples only.

  181. 273 The entropy photon-number inequality

    Lean Awaiting review

    Entropy photon-number inequality (Guha–Shapiro conjecture) for beam splitters in any number of modes. Lean Comparator-accepted. No expert reaction found.

  182. 274 Parity is not in QAC<sup>0</sup>

    Lean Awaiting review

    Parity is not in QAC⁰ (Moore’s conjecture, measured-output model). Lean accepted. Aaronson: ‘one of the great questions of quantum complexity theory since 1999’.

  183. 282 From scale symmetry to local conformal symmetry in four-dimensional QFT

    Awaiting review

    Scale invariance implies local conformal invariance in 4D QFT under stated algebraic-QFT hypotheses (conditional). A 2013 claim by Farnsworth–Luty–Prelipina was withdrawn.

  184. 283 Polynomial-time unitary synthesis from a Boolean oracle

    Awaiting review

    Positive answer to the Aaronson–Kuperberg unitary synthesis problem. Aaronson: ‘the opposite of what most of us expected’; SciAm highlight; Dakshita Khurana is working through it.

  185. 284 The optimal quartic separation between randomized and quantum queries

    Awaiting review

    R(f)=O(Q(f)^4) is tight for total Boolean functions, refuting the cubic conjecture. Aaronson: ‘this finally closes that story’. No Lean.

  186. 286 Rigidity and arithmetic of lattice von Neumann algebras

    Awaiting review

    Lattice case of Connes’ rigidity: classification of finite-index bimodules of property-(T) lattice factors. Cyril Houdayer ‘genuinely thrilled’ (Proofs and Prompts).

  187. 289 Strong Kadison–Kastler stability and its spatial boundaries

    Lean Awaiting review

    Strong Kadison–Kastler conjecture: nearby von Neumann algebras are conjugate by a near-identity unitary, plus boundary counterexamples. Lean (uniform statement) accepted.

  188. 290 Relative bicentralizers and modular spectral recovery

    Lean Awaiting review

    Relative Connes bicentralizer conjecture. Houdayer: it builds on Marrakchi’s methods; Houdayer–Marrakchi solved the absolute case in September. Lean partial.

  189. 291 Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stability

    Lean Awaiting review

    Unital Toms–Winter conjecture and equivariant Jiang–Su stability (Szabó). Overlaps human papers (Evington et al., Thiel); our Toms–Winter entry covers the human proof.

  190. 292 Kirchberg’s $`\mathcal O_2`$ norm-ultrapower embedding problem

    Lean Awaiting review

    Kirchberg’s O₂ norm-ultrapower embedding problem answered negatively with an explicit full group C*-algebra. Lean accepted.

  191. 293 Invariant projections, hyperinvariant subspaces, and transitive algebras

    Lean Awaiting review

    Operator on Hilbert space with no nontrivial hyperinvariant subspace; proper transitive commutant; II₁ operator with no invariant projection. Lean accepted.

  192. 294 Kaplansky’s quasitrace conjecture and failure of tensor-product stable finiteness

    Lean Awaiting review; here: Kaplansky’s quasitrace conjecture reported disproved by an unreleased OpenAI model

    Kaplansky’s quasitrace conjecture disproved; Lean accepted. Arulseelan–Hanson fully reproduce it. Our entry wrongly called the manuscript unpublished; corrected 29 Oct.

  193. 295 The Kadison–Ringrose cohomology conjecture

    Lean Awaiting review

    Kadison–Ringrose conjecture: bounded Hochschild cohomology of a von Neumann algebra in itself vanishes in degrees ≥2. Lean accepted.

  194. 296 The generator problem for finite factors

    Lean Awaiting review

    Generator problem: every II₁ factor with separable predual is singly generated. Lean accepted. Elliott–Li–Niu apply it (arXiv 2610.17411).

  195. 297 A ZFC counterexample to Naimark’s problem

    Lean Awaiting review

    Second ZFC counterexample to Naimark’s problem, after Tanaka’s. Nik Weaver (MathOverflow): against his expectation. Lean accepted with a definition-body caveat.

  196. 298 Two notions of free entropy differ even when both are finite

    Lean Awaiting review

    Microstates and non-microstates free entropy differ while both finite (Voiculescu’s question). Lean accepted; Jekel cites it as the first example.

  197. 302 Radius of comparison equals half the mean dimension

    Awaiting review

    Radius of comparison equals half the mean dimension for minimal homeomorphisms (Phillips–Toms). Elliott–Niu build on it (arXiv 2610.11143). No Lean.

  198. 306 The purely cosmetic surgery conjecture

    Awaiting review

    Purely cosmetic surgery conjecture for knots in S³. No Lean. Ichihara–Kishimoto posted independent partial results (arXiv 2610.10019).

  199. 307 Failure of rational injectivity for maximal coarse assembly

    Lean Awaiting review

    Rational coarse Novikov conjecture disproved: maximal and reduced coarse assembly fail rational injectivity. Lean (reduced case) accepted.

  200. 308 Finite Smith–Toda complexes at every height

    Awaiting review; here: Smith–Toda V(4) for p ≥ 11, after OpenAI’s p = 1009

    Finite Smith–Toda complexes V(n) at every height for varying primes; V(4) at p=1009. Angeltveit extends V(4) to p≥11 (own entry).

  201. 309 The Kervaire invariant problem at the prime three

    Awaiting review

    Odd-primary Kervaire invariant problem at p=3: classes survive only in stems 10, 106 and 322. No Lean; no reactions found.

  202. 310 Quillen’s conjecture in rational homology

    Awaiting review

    Quillen’s conjecture on p-subgroup posets, in rational homology, for every finite group and prime. No Lean; no reactions found.

  203. 311 The Hovey–Strickland and Chai conjectures

    Awaiting review; here: Hovey–Strickland: author says OpenAI’s paper matches his ChatGPT-uploaded draft

    Chai and Hovey–Strickland conjectures. Chenglong Ma (arXiv 2610.10072): OpenAI’s strategy and notation ‘identical’ to his draft uploaded to ChatGPT on 8 Sept; Ningyi Li proved it independently. Own entry.

  204. 312 The Grothendieck homotopy hypothesis

    Lean Awaiting review

    Grothendieck’s homotopy hypothesis for Grothendieck ∞-groupoids (Ara–Henry convention). Lean covers the elementary-expansion step only; Yao Xu’s project claims more.

  205. 313 Finite generation for the $`K(n)`$-local sphere

    Awaiting review

    Every homotopy group of the K(n)-local sphere is finitely generated over ℤ_p (Hovey–Strickland question). No Lean.

  206. 315 The four-dimensional Singer conjecture

    Awaiting review

    Four-dimensional Singer conjecture for aspherical 4-manifolds and PD4 complexes. No Lean; no reactions found.

  207. 316 Curtis’s conjecture

    Awaiting review

    Curtis’s conjecture on the mod-2 stable Hurewicz image of the sphere. No Lean; no reactions found.

  208. 318 Chromatic splitting: filtrations and counterexamples

    Awaiting review

    Chromatic splitting conjecture counterexamples (strong at height 3; weak at heights p, p+1). Beaudry–Schlank, with Claude, show weak splitting fails at n=p.

  209. 321 A counterexample to Wall’s finite D(2) problem

    Awaiting review

    Counterexample to Wall’s D(2) problem. No OpenAI Lean; Pyronis WallD2 offers a conditional Lean formalization.

  210. 322 Tingley’s sphere-isometry problem

    Lean Awaiting review

    Tingley’s problem solved for all real Banach spaces. Lean accepted. Kudaybergenov et al. independently treat a finite-dimensional class (arXiv 2610.19626).

  211. 323 Independence of the separable quotient problem

    Lean Awaiting review

    Separable quotient problem is independent of ZFC (relative to a measurable cardinal). Lean covers the CH counterexample. Mitchell Taylor: ‘truly spectacular’.

  212. 324 Lipschitz equivalent Banach spaces need not be linearly isomorphic

    Lean Awaiting review

    Lipschitz-equivalent separable Banach spaces need not be linearly isomorphic. Lean accepted. No reactions found.

  213. 325 The complete Crouzeix conjecture

    Lean Awaiting review

    Complete (matrix-valued) Crouzeix conjecture with constant 2 on any Hilbert space. Lean accepted. The scalar case was proved in July (our 2026-07-27 entry).

  214. 327 Markov type characterizes superreflexivity

    Lean Awaiting review

    Naor’s renorming question: nontrivial Markov type characterizes superreflexivity. Lean accepted.

  215. 328 Nonexpansive fixed points in reflexive Banach spaces

    Lean Awaiting review

    Kirk’s problem: every reflexive Banach space has the fixed-point property for nonexpansive maps. Lean accepted. No reactions found.

  216. 329 A counterexample to metric-entropy duality

    Lean Awaiting review

    Pietsch’s dimension-free duality conjecture for metric entropy disproved. Lean accepted.

  217. 332 Metric Markov cotype of ℓ<sub>1</sub> and Hilbert-space Lipschitz extension

    Awaiting review

    Real ℓ₁ has metric Markov cotype 2 (Mendel–Naor question), giving Ball-type extension from Hilbert space into ℓ₁. No Lean.

  218. 333 Smooth isometric immersions of surfaces into ℝ<sup>4</sup>

    Lean Awaiting review

    Every closed smooth surface isometrically immerses in ℝ⁴. Lean accepted. Kitamura claims a strengthening to embeddings on GitHub.

  219. 334 A smooth surface metric with no local isometric immersion in ℝ<sup>3</sup>

    Lean Awaiting review

    Smooth surface metric with no local isometric immersion in ℝ³, answering the classical local problem negatively. Lean accepted.

  220. 336 Spectral scalar curvature, Urysohn width, and macroscopic dimension

    Awaiting review

    Gromov-type width and macroscopic-dimension bounds under spectral scalar curvature. No Lean. Yuchen Bi adapts its ideas (arXiv 2610.28390).

  221. 337 Sharp Cartan–Hadamard isoperimetry and rigidity

    Lean Awaiting review

    Cartan–Hadamard isoperimetric conjecture in every dimension with rigidity; sharp CAT(0) fillings. Lean covers only the CAT(0) integral-current form.

  222. 339 Katok’s entropy rigidity conjecture

    Awaiting review

    Katok’s entropy rigidity conjecture in dimension ≥3. Tristan Humbert (Proofs and Prompts) called the paper ‘mostly unreadable slop’. No Lean.

  223. 341 Donaldson’s hypersymplectic deformation conjecture

    Updated by OpenAI

    Donaldson’s hypersymplectic deformation conjecture, cohomology-preserving form. Revised 7 Oct (criterion clarified, cone citation removed). No Lean.

  224. 342 Donaldson’s tamed-to-compatible conjecture

    Lean Updated by OpenAI

    Donaldson’s tamed-to-compatible conjecture on closed 4-manifolds. Revised 7 Oct (cone-equality claim corrected). Lean accepted.

  225. 344 The metric Blaschke conjecture

    Awaiting review

    Metric Blaschke conjecture: injectivity radius equal to diameter forces a compact rank-one symmetric space. No Lean; no reactions found.

  226. 346 Sharp singular-set bounds for stationary integral varifolds

    Awaiting review

    Stationary integral varifolds: singular set of dimension ≤ m−1 and almost-everywhere regularity (Brena–Decio–De Lellis conjectures). No Lean; no reactions found.

  227. 347 Counterexamples to stable-Morse and strong Arnold fixed-point bounds

    Lean Awaiting review

    Counterexamples to stable-Morse lower bounds and the strong Arnold conjecture (three fixed points on the quadric threefold). Lean covers the strong Arnold case.

  228. 348 Nonnegative-curvature Einstein classification and an L<sup>2</sup> topological gap

    Lean Awaiting review

    Einstein 4-manifolds with nonnegative sectional curvature classified, with an L² gap theorem. Lean covers only strictly positive curvature.

  229. 349 The Solomon–Yau least-volume conjecture

    Awaiting review

    Solomon–Yau least-volume conjecture for minimal hypersurfaces in spheres. No Lean. Jingwen Chen uses it (arXiv 2610.20453).

  230. 351 Scalar curvature and finite-time Ricci-flow singularities

    Awaiting review

    Four-dimensional Ricci flow extends while scalar curvature stays bounded; counterexample in higher dimension. No Lean.

  231. 352 A finite-time singularity of Calabi flow

    Awaiting review

    Chen’s long-time existence conjecture for Calabi flow disproved: finite-time singularity on CP¹⁰ in the Fubini–Study class. No Lean.

  232. 353 Affine Bernstein rigidity through dimension nine and a smooth dimension-ten counterexample

    Lean Awaiting review

    Affine Bernstein problem: rigidity in dimensions 3–9, smooth counterexample in 10. Trudinger–Wang independently give n≥10 examples. Lean covers graph case.

  233. 355 Unique tangent flows at the first surface singularity

    Awaiting review

    Uniqueness of tangent flows at the first singular time for embedded surfaces under mean curvature flow. No Lean.

  234. 359 Negative Kähler curvature without bounded holomorphic coordinates

    Lean Awaiting review

    Contractible domain in ℂ³ with negatively pinched Kähler metric but no bounded holomorphic coordinates. Lean accepted.

  235. 361 Failure of integer-degree harmonic dimension comparison

    Lean Awaiting review

    Yau’s harmonic-function dimension comparison fails for integer growth. Lean covers a 16-dimensional instance, not the paper’s ℝ³ claim.

  236. 364 Kinetic limits and fluctuations over the Boltzmann lifespan

    Awaiting review

    Boltzmann equation derived from Newtonian gases over the full kinetic lifespan, with Gaussian fluctuations. No Lean.

  237. 365 Joint metric and connection recovery from one boundary patch

    Lean Awaiting review

    One-patch recovery of metric and connection; L∞ conductivities in 3D with identical Calderón data (Lean). Mikko Salo flags direct interest.

  238. 366 The planar Mumford–Shah regularity conjecture and local weak-L<sup>4</sup> gradient bounds

    Awaiting review

    Planar Mumford–Shah regularity conjecture. No Lean. A separate Astra-generated claim (Deangelis, 22 Sept) has our entry; OpenAI’s version has none.

  239. 367 The critical dimension for the one-phase Bernoulli problem

    Lean Awaiting review

    Critical dimension seven for one-phase Bernoulli minimizers. OpenAI Lean covers the dimension-7 example; William Feldman’s Lean proves flatness up to dimension six.

  240. 368 The three-dimensional Ball–Evans approximation problem

    Awaiting review

    Ball–Evans approximation problem in 3D: Sobolev homeomorphisms are limits of diffeomorphisms. No Lean.

  241. 370 The Lane–Emden and Hénon–Lane–Emden conjectures

    Lean Awaiting review; here: AI-assisted results in the 19 Oct 2026 arXiv listing

    Subcritical Lane–Emden and Hénon–Lane–Emden conjectures. Lean accepted. Mei–Wei and Li–Lu–Zhang extend it to fractional cases (listing entry).

  242. 371 Stable blowup for the defocusing Schrödinger equation

    Lean Awaiting review

    Stable finite-time blowup for defocusing NLS on 𝕋¹². Lean accepted with definition-body caveat; covers arbitrarily large odd powers, not all.

  243. 372 Global uniqueness in smooth isotropic elasticity

    Lean Awaiting review

    Global uniqueness of smooth Lamé parameters from boundary data in 3D. Lean accepted. Diao–Durdiev claim the same theorem (arXiv 2610.14741).

  244. 376 Universal computation in forced Navier–Stokes flows

    Lean Updated by OpenAI

    Forced Navier–Stokes flows perform universal computation. Revised 7 Oct (decay estimates). Lean partial. Anders Sandberg called it his favourite family.

  245. 377 Interior $`C^{1,\alpha}`$ regularity for infinity-harmonic functions

    Awaiting review

    Interior C^{1,α} regularity for infinity-harmonic functions in every dimension d≥3. No Lean.

Specialist results 40

Technical results inside one area.

  1. 027 Potential integral density on curve character varieties

    Lean Awaiting review

    Determinant-one curve case of Litt’s integral-density question for SL_r character varieties. Lean covers a supporting construction only.

  2. 035 Log-canonical threefold abundance in numerical dimension one

    Awaiting review

    Log abundance for lc threefolds in characteristic p > 3 in numerical dimension one. Manuscript only.

  3. 068 Anticanonical nonvanishing in every dimension

    Awaiting review

    Smooth semipositive anticanonical bundle forces a section of −mK_X. Seven manuscripts; only AI-written digests found.

  4. 093 Dimension-free logarithmic Sobolev inequality for subgaussian log-concave measures

    Awaiting review

    Dimension-free log-Sobolev inequality for centered log-concave densities with subgaussian marginals. Manuscript only.

  5. 133 The computational complexity of Weisfeiler–Leman refinement

    Lean Awaiting review

    Claims n^Ω(k) time lower bounds and EXPTIME-completeness for Weisfeiler–Leman equivalence; Lean in part; concurrent AI-assisted work by Curticapean, Liu, Neuen, Seppelt.

  6. 135 Homogeneous depth-five lower bounds for iterated matrix multiplication

    Lean Awaiting review

    Claims sharp n^Θ(√n) homogeneous depth-five circuit bounds for iterated matrix multiplication over characteristic zero; Lean-formalized.

  7. 137 One-tape time simulation in two-fifths-power space

    Lean Awaiting review

    Claims one-tape time-T machines can be simulated in O(T^(2/5) polylog T) space, improving the square-root exponent; Lean-formalized.

  8. 139 Subpolynomial query complexity for log-concave sampling

    Lean Awaiting review

    Claims well-conditioned log-concave sampling needs only C_ε·d^ε value-and-gradient queries, with a log d lower bound; Lean-formalized.

  9. 140 Memory–sample lower bounds for noiseless Gaussian regression

    Lean Awaiting review

    Claims one-pass learners with O(d²) memory bits need Ω(d log(1/ε)) noiseless Gaussian samples; six manuscripts; Lean-formalized.

  10. 190 Polynomial removal fails for ordered binary matrices

    Lean Awaiting review; here: Mid-October 2026: arXiv results with disclosed AI help

    Disproves polynomial removal for ordered binary matrices with a 66×66 pattern; Lean; Zinan Wang found a 4×4 obstruction (arXiv 2610.15370).

  11. 192 Boolean functions violate the square-root degree bound by arbitrary factors

    Lean Awaiting review

    Disproves the Gopalan–Servedio square-root degree bound on linear Fourier coefficients by arbitrary factors; Lean-formalized.

  12. 204 Tensor saturation for even spin groups

    Awaiting review

    Claims saturation factor one for Spin(2n), the type-D case of the simply-laced saturation conjecture; no Lean.

  13. 233 The joint critical Ashkin–Teller current limit

    Updated by OpenAI; here: OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems

    Claims the joint critical Ashkin–Teller height and current scaling limit; revised 7 Oct (transmission, boundary-collar repairs); no Lean.

  14. 234 All-temperature pressure of orthogonally invariant Ising spin glasses

    Lean Awaiting review

    Claims all-temperature variational pressure formulas for orthogonally invariant Ising spin glasses; Lean-formalized; specialist result.

  15. 275 QMA-hardness of continuum Coulomb energy

    Lean Awaiting review

    QMA-hardness of approximating the continuum Coulomb ground-state energy. Lean Comparator-accepted.

  16. 276 Classical capacity of generalized amplitude damping

    Lean Awaiting review

    Exact classical capacity of every qubit generalized amplitude-damping channel, with additivity. Lean (capacity) accepted.

  17. 277 Threshold repetition for entangled games

    Lean Awaiting review

    Exponential threshold parallel repetition for entangled two-player games. Lean accepted; Rahul Jain compares rates in arXiv 2610.21410.

  18. 278 Failure of Kohn–Sham ensemble representation

    Awaiting review

    Kohn–Sham ensemble representability fails for a three-electron molecule in L^{3/2}+L^∞. No Lean; Haycraft’s note argues representability in a larger class.

  19. 279 Exact quantum factoring over a fixed finite gate set

    Lean Awaiting review

    Exact (probability-one) polynomial-time quantum factoring over one fixed finite gate set. Lean accepted.

  20. 280 Unitary vertex operator algebras and conformal nets

    Lean Awaiting review

    Strongly rational unitary vertex operator algebras give completely rational conformal nets (strong locality). Lean covers the first construction step only.

  21. 281 QAOA attains the SK optimum in the thermodynamic-first limit

    Lean Awaiting review

    QAOA reaches the Sherrington–Kirkpatrick ground-state energy when size grows before depth. Lean covers Parisi identities, not QAOA convergence.

  22. 299 The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stability

    Lean Awaiting review

    Kirchberg–Rørdam character criterion for Jiang–Su stability; Dadarlat–Toms question. Lean accepted; Bruce–Geffen apply it to Thompson’s group F.

  23. 300 Approximation and quadratic strong-operator paving

    Awaiting review

    Popa–Vaes quadratic strong-operator paving conjecture. No Lean; no reactions found.

  24. 301 Trace cones and Razak–Jacelon stabilization

    Lean Awaiting review

    Robert’s trace-cone question: classification after Razak–Jacelon stabilization. Lean covers a supporting ideal-transport result.

  25. 303 Weak pure infiniteness and Cuntz-algebra absorption

    Lean Awaiting review

    Kirchberg–Rørdam question: proper infiniteness of positive elements implies strong pure infiniteness. Lean accepted.

  26. 314 Cyclic length and chromatic fixed-point loss

    Awaiting review

    Optimal chromatic fixed-point loss equals cyclic subnormal chain length for p-groups. No Lean.

  27. 317 Thomason model structures in all strict higher dimensions

    Lean Awaiting review

    Ara–Maltsiniotis conjecture: Thomason model structures on strict n-categories for all n. Lean accepted.

  28. 319 Counterexamples to finite generation at chromatic height two

    Awaiting review

    Hahn–Wilson finite-generation conjecture refuted at chromatic height two for large primes. No Lean.

  29. 326 The cotype–cotype conjecture under the approximation property

    Lean Awaiting review

    Cotype–cotype conjecture for real Banach spaces with the approximation property. Lean accepted.

  30. 330 A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces

    Lean Awaiting review

    Kalton’s question: uniformly discrete space whose Lipschitz-free space has AP but not BAP. Lean accepted.

  31. 331 Reflexive midpoint convexity and diamond distortion

    Lean Awaiting review

    Reflexive space separating midpoint from asymptotic uniform convexity; diamond distortion bounds. Lean accepted.

  32. 343 Symplectic ball packing in higher dimensions

    Lean Awaiting review

    Siegel–Yao symplectic ball-packing criterion in dimension ≥6. Lean accepted.

  33. 354 The isoperimetric profile of the cubic three-torus

    Lean Awaiting review

    Isoperimetric profile and all minimizers of the cubic flat 3-torus. Lean accepted.

  34. 356 Gigli’s characterization of Alexandrov curvature

    Lean Awaiting review

    Gigli’s characterization of Alexandrov curvature through RCD conditions. Lean covers a supporting Hessian lemma.

  35. 357 Bi-Lipschitz coordinates at every regular RCD point

    Awaiting review

    Bi-Lipschitz charts at every regular point of noncollapsed RCD spaces. No Lean.

  36. 358 A three-manifold without conjugate points or nonpositive curvature

    Lean Awaiting review

    Closed 3-manifold with a no-conjugate-points metric but no nonpositively curved metric. Lean accepted.

  37. 360 Weak MTW curvature gives convexity and regular optimal transport

    Lean Awaiting review

    Villani’s conjecture: weak MTW curvature gives convex injectivity domains and Hölder optimal transport. Lean accepted.

  38. 363 Nonuniqueness with local conservation for the hard-sphere Boltzmann equation

    Lean Awaiting review

    Two distinct global entropy solutions of the hard-sphere Boltzmann equation from the same data. Lean accepted.

  39. 373 Nonattainment of the three-marginal Coulomb Monge problem

    Lean Awaiting review

    Monge non-attainment for three-marginal Coulomb optimal transport. Lean accepted for the 3D case.

  40. 374 Sharp one-third stability of Brenier maps

    Lean Awaiting review

    Sharp one-third stability of Brenier maps, refuting Letrouit’s square-root conjecture. Lean accepted with definition caveat; concurrent human papers.

See also: the release, AI and open problems: claimed vs checked.