Fifty open problems for short AI + Lean + CAS campaigns

I optimized for crisp statements with a plausible dent: a new finite case, a certified construction or obstruction, a better exponent or constant, or a reusable formal lemma. The status cutoff is 2026-08-16. I favored living surveys and primary papers, and screened out several newly stale targets (including non-sofic-group existence, the old real sum-product conjecture, Erdős–Hajnal for graphs on at most five vertices, lonely runner through 13 runners, and the recently announced order-668 Hadamard construction). “Open” below means that the cited current source still treats the stated target as open and I found no later accepted resolution; where that check is less decisive, I say so explicitly. A dent need not settle the headline conjecture.

P01. Quantitative arithmetic removal in the integers

• Slug: quantitative-arithmetic-removal
• Area: Additive combinatorics
• Why open: If (A\subseteq[N]) has at most $\varepsilon N^2$ solutions to (x+y=z), the arithmetic removal lemma gives deletion of (o_\varepsilon(N)) elements to make (A) sum-free, but no remotely satisfactory dependence of the deletion fraction on $\varepsilon$ is known.
• Attack shape: bound
• Why an AI stack might dent it: Finite cyclic models, energy increment recurrences, and exact optimization of small cases can be explored computationally, while Lean can certify a quantitatively improved chain of inequalities.
• Sources: Ben Green, 100 Open Problems, Problem 8 (December 2025 update); Green, A Szemerédi-type regularity lemma in abelian groups

P02. A logarithmic saving for five-term progression-free sets

• Slug: five-term-progression-log-saving
• Area: Additive combinatorics
• Why open: Writing (r_5(N)) for the largest subset of ([N]) with no nontrivial five-term arithmetic progression, it is still unknown whether (r_5(N)\ll N(\log N)^{-c}) for some absolute (c>0).
• Attack shape: bound
• Why an AI stack might dent it: A campaign can isolate one quantitative loss in the (U^4)-inverse/density-increment pipeline, test finite-field analogues, and formalize the combinatorial bookkeeping that often hides improvable constants.
• Sources: Ben Green, 100 Open Problems, Problem 9(ii); Gowers, A new proof of Szemerédi's theorem

P03. Four-term progressions in Fourier-uniform sets

• Slug: four-ap-fourier-uniform
• Area: Additive combinatorics
• Why open: For a density-$\alpha$ set (A\subseteq\mathbb Z/N\mathbb Z) with all nontrivial Fourier coefficients (o(N)), it is unknown whether (A) must contain at least (\gg \alpha^{100}N^2) four-term arithmetic progressions.
• Attack shape: counterexample
• Why an AI stack might dent it: Structured two-step nilsequence families can be parameter-searched for counterexamples, with exact rational or algebraic certificates replacing floating-point evidence.
• Sources: Ben Green, 100 Open Problems, Problem 13; Gowers, A new proof of Szemerédi's theorem

P04. The Möbius-ladder Cayley–Sidorenko inequality

• Slug: mobius-ladder-cayley-sidorenko
• Area: Extremal graph theory / additive combinatorics
• Why open: The Cayley-graph instance of Sidorenko's conjecture for the first unresolved graph (K_{5,5}\setminus C_{10}) asks for the corresponding ten-variable configuration count to be at least its random-density value; this special inequality remains open.
• Attack shape: proof
• Why an AI stack might dent it: The target is a finite multilinear inequality amenable to sum-of-squares searches, flag-algebra experiments, and Lean verification of a discovered Cauchy–Schwarz certificate.
• Sources: Ben Green, 100 Open Problems, Problem 12; Conlon, Fox, and Sudakov, An approximate version of Sidorenko's conjecture

P05. Extremal affine copies of $\{0,1,3\}$

• Slug: affine-013-copies
• Area: Extremal additive combinatorics
• Why open: For an (n)-element integer set (A), the conjectured maximum number of affine copies of $\{0,1,3\}$ is ((1/3+o(1))n^2), but even the asymptotic constant is unknown.
• Attack shape: bound
• Why an AI stack might dent it: Exhaustive extremizer searches can suggest stability structure, after which compression and charging arguments are compact enough to formalize.
• Sources: Ben Green, 100 Open Problems, Problem 24; Aaronson, A note on the maximum number of three-term patterns

P06. Sumsets with no uniquely represented element

• Slug: no-unique-sum-mod-p
• Area: Additive combinatorics
• Why open: The minimum size of a nontrivial (A\subseteq\mathbb Z/p\mathbb Z) for which every element of (A+A) has at least two representations is only known to lie between (\omega(p)\log p) and (O(\log^2p)).
• Attack shape: bound
• Why an AI stack might dent it: SAT search over small primes can expose reusable algebraic patterns, and additive-energy lemmas can be checked symbolically and then certified in Lean.
• Sources: Ben Green, 100 Open Problems, Problem 27; Bedert, On unique sums in finite abelian groups

P07. The second term for Sidon subsets of $[N]$

• Slug: sidon-second-term
• Area: Additive combinatorics
• Why open: For the largest Sidon subset (F(N)\subseteq[N]), the gap between the construction (\sqrt N+O(1)) and the upper bound (\sqrt N+0.98183N^{1/4}+O(1)) remains; any strict improvement on either side for infinitely many (N) is open.
• Attack shape: bound
• Why an AI stack might dent it: Difference-set searches, modular unwrapping, Fourier optimization, and exact verification make this a natural hybrid construction-and-proof target.
• Sources: Erdős Problem #30; Ben Green, 100 Open Problems, Problem 31

P08. A long gap in a dilate modulo a prime

• Slug: long-gap-dilate-mod-prime
• Area: Additive combinatorics
• Why open: If (A\subseteq\mathbb Z/p\mathbb Z) has size about (\sqrt p), it is unknown whether some nonzero dilate of (A) misses an interval of length (100\sqrt p); only the constant 2 is currently guaranteed by the cited polynomial-method result.
• Attack shape: bound
• Why an AI stack might dent it: Small-prime extremizers can be enumerated and clustered, and polynomial-method certificates are especially compatible with CAS discovery and Lean checking.
• Sources: Ben Green, 100 Open Problems, Problem 32; Shakan, On higher moments of Fourier coefficients

P09. Thin cyclic additive bases

• Slug: thin-cyclic-additive-bases
• Area: Additive combinatorics / design theory
• Why open: It is unknown whether infinitely many (q) admit (A\subseteq\mathbb Z/q\mathbb Z) with (A+A=\mathbb Z/q\mathbb Z) and (|A|=(\sqrt2+o(1))\sqrt q), the counting-optimal constant.
• Attack shape: proof
• Why an AI stack might dent it: Algebraic and difference-family ansätze can be searched over finite fields, with one infinite parametric family enough for a substantive advance.
• Sources: Ben Green, 100 Open Problems, Problem 33; Caprace and de la Harpe, Groups with irreducibly unfaithful subsets for unitary representations

P10. A polynomial-size core in an approximate group

• Slug: approximate-group-polynomial-core
• Area: Additive combinatorics / group theory
• Why open: For a (K)-approximate group (A), it is unknown whether there is (S\subseteq A) with (|S|\ge K^{-O(1)}|A|) and (S^8\subseteq A^4); the known dependence is not polynomial in (K).
• Attack shape: bound
• Why an AI stack might dent it: The task invites automated Ruzsa-calculus exploration and proof-term reuse, and even a better exponent or a proof for a new group class would count.
• Sources: Ben Green, 100 Open Problems, Problem 29; Breuillard, Green, and Tao, The structure of approximate groups

P11. A composite in a sumset below the square-root threshold

• Slug: composite-in-thin-sumset
• Area: Additive number theory
• Why open: It is unknown whether every (A,B\subseteq[N]) with (|A|=|B|=N^{0.49}) have a composite in (A+B); a positive answer would rule out a strong form of inverse Goldbach decomposition.
• Attack shape: proof
• Why an AI stack might dent it: Modular sieves and inverse-large-sieve structure can be tested on adversarial finite sets, then converted into a sharply scoped lemma for one exponent above the current frontier.
• Sources: Ben Green, 100 Open Problems, Problem 58; Elsholtz, The inverse Goldbach problem

P12. Two smooth summands for every integer

• Slug: two-smooth-summands
• Area: Additive number theory
• Why open: For fixed (\varepsilon>0), it remains unknown whether every (n\le N) is a sum of two integers whose prime factors are all at most (N^\varepsilon), for all sufficiently large (N).
• Attack shape: proof
• Why an AI stack might dent it: Residue-cover searches can reveal finite local templates, while smooth-number estimates and CRT arguments are amenable to modular formalization.
• Sources: Ben Green, 100 Open Problems, Problem 59; Erdős Problem #334

P13. Positive density of the Hofstadter $ab-1$ closure

• Slug: hofstadter-ab-minus-one-density
• Area: Computational number theory
• Why open: Let (A) be the smallest set containing 2 and 3 and closed under (a,b\mapsto ab-1); whether (A) has positive natural density is open.
• Attack shape: proof
• Why an AI stack might dent it: This explicitly invites computation: fast closure generation can identify covering recurrences or missing congruence classes, and any finite covering certificate can be checked exactly.
• Sources: Erdős Problem #424; OEIS A005244; Ben Green, 100 Open Problems, Problem 63

P14. A smaller constant in the two-squares gap

• Slug: two-squares-short-gap
• Area: Number theory
• Why open: It is unknown whether every sufficiently large (X) has a sum of two squares in $[X-\tfrac1{10}X^{1/4},X]$; the elementary (O(X^{1/4})) scale is known, but this explicit constant target is not.
• Attack shape: bound
• Why an AI stack might dent it: Continued fractions, lattice reduction, and exhaustive study of near-extremal gaps can suggest a finite case split whose inequalities are CAS-checkable.
• Sources: Ben Green, 100 Open Problems, Problem 66; Erdős Problem #143

P15. Chowla's cosine problem

• Slug: chowla-cosine
• Area: Harmonic analysis / additive combinatorics
• Why open: For every (n)-element integer set (A), it is conjectured that some (\theta$satisfies$\sum_{a\in A}\cos(2\pi a\theta)\le -c\sqrt n$ for an absolute (c>0); the square-root negative excursion is still unproved.
• Attack shape: bound
• Why an AI stack might dent it: Semidefinite searches can optimize auxiliary trigonometric polynomials, and Lean can certify the resulting finite Fourier inequality.
• Sources: Ben Green, 100 Open Problems, Problem 81; Open Problem Garden, Chowla's cosine problem

P16. Zeros of integer cosine sums

• Slug: zeros-of-cosine-sums
• Area: Harmonic analysis
• Why open: For (|A|=n), the best universal lower bound on the number of zeros of $\sum_{a\in A}\cos(2\pi a\theta)$ grows only like ((\log\log n)^{1-o(1)}), while examples give only an (O(n^{2/3}\log^{2/3}n)) upper barrier; the true order is unknown.
• Attack shape: bound
• Why an AI stack might dent it: Exact root isolation for structured families can test conjectured extremizers, and symbolic sign-change arguments can yield certified incremental lower bounds.
• Sources: Ben Green, 100 Open Problems, Problem 82; Bedert, The number of zeros of cosine polynomials

P17. Irreducibility of random $0/1$ polynomials

• Slug: random-zero-one-polynomial-irreducibility
• Area: Probabilistic number theory
• Why open: For (P_n(x)=1+a_1x+\cdots+a_{n-1}x^{n-1}+x^n) with independent Bernoulli (a_i), it remains unknown unconditionally whether $\Pr(P_n\text{ irreducible over }\mathbb Z)\to1$; GRH-conditional and broader-alphabet results are known.
• Attack shape: proof
• Why an AI stack might dent it: Massive exact factor statistics can isolate the remaining factor-degree regimes, while finite-field and sieve lemmas can be developed and formalized independently.
• Sources: Ben Green, 100 Open Problems, Problem 93; Breuillard and Varjú, Irreducibility of random polynomials of large degree

P18. Close the worst-case trace-reconstruction gap

• Slug: worst-case-trace-reconstruction-gap
• Area: Coding theory / theoretical computer science
• Why open: For deletion probability (1/2), worst-case binary trace reconstruction has a polynomial lower bound (about (n^{3/2}), up to logs) versus an $\exp(O(n^{1/5}\log^5 n))$ upper bound; even a changed exponent is open.
• Attack shape: bound
• Why an AI stack might dent it: The problem mixes complex-polynomial inequalities, adversarial string search, and exact probabilistic estimates, letting computation target one bottleneck rather than the whole gap.
• Sources: Ben Green, 100 Open Problems, Problem 92; Chase, New upper bounds for trace reconstruction; New Bounds for Circular Trace Reconstruction, ITCS 2026

P19. Full asymptotics for the $n$-queens count

• Slug: n-queens-full-asymptotic
• Area: Enumerative combinatorics
• Why open: The exponential-scale formula (Q(n)=((1+o(1))ne^{-\alpha})^n) is known, but a true asymptotic equivalent, including the subexponential factor, remains open.
• Attack shape: bound
• Why an AI stack might dent it: The entropy optimizer can be computed at high precision, finite counts can test correction terms, and switching arguments admit formal local verification.
• Sources: Ben Green, 100 Open Problems, Problem 97; Simkin, The number of n-queens configurations

P20. Density of the Ulam sequence

• Slug: ulam-sequence-density
• Area: Additive combinatorics / OEIS
• Why open: For the classical Ulam sequence beginning (1,2), it is unknown whether its natural density exists or is positive, and its striking Fourier concentration lacks a proof-level explanation.
• Attack shape: proof
• Why an AI stack might dent it: Fast exact generation, spectral experiments, automaton discovery, and proof search for a finite-state or interval recurrence fit the available Python–Lean stack unusually well.
• Sources: Ben Green, 100 Open Problems, Problem 7; OEIS A002858; Steinerberger, A hidden signal in the Ulam sequence

P21. Shannon capacity of the 7-cycle

• Slug: shannon-capacity-c7
• Area: Zero-error information theory / additive combinatorics
• Why open: The Shannon capacity of (C_7) lies between (367^{1/5}\approx3.2578) and (7\cos(\pi/7)/(1+\cos(\pi/7))\approx3.3177), and neither endpoint is known to be exact.
• Attack shape: bound
• Why an AI stack might dent it: Maximum independent sets in graph powers can be attacked by SAT/ILP with symmetry, while semidefinite dual certificates can be converted to exact algebraic data.
• Sources: Ben Green, 100 Open Problems, Problem 38; Bohman and Holzman, A nontrivial lower bound on the Shannon capacities of the complements of odd cycles

P22. Density loss for linear radius-two covering codes

• Slug: linear-covering-code-radius-two
• Area: Coding theory
• Why open: For linear binary covering codes of fixed radius 2, Green's normalization (f(2)) satisfies (1\le f(2)\le1.4238), and it is not even known whether (f(2)=1).
• Attack shape: bound
• Why an AI stack might dent it: Finite-field linear algebra, SAT searches for parity-check matrices, and exact covering certificates directly match the environment; new constructions or obstructions both move the constant.
• Sources: Ben Green, 100 Open Problems, Problem 40; Cohen et al., Covering Codes

P23. The first open no-three-in-line grid regime

• Slug: no-three-in-line-grid
• Area: Discrete geometry
• Why open: The maximum size of a subset of ([N]^2) with no three collinear is unknown asymptotically; in particular, it is open whether (2N) points are impossible for every sufficiently large (N).
• Attack shape: bound
• Why an AI stack might dent it: Constraint programming can extend or rule out structured (2N)-point configurations for new (N), and incidence-count certificates can be independently checked.
• Sources: Ben Green, 100 Open Problems, Problem 72; Guy and Kelly, The no-three-in-line problem

P24. Cubic stability for large finite-field arcs

• Slug: finite-field-arc-cubic-stability
• Area: Finite geometry
• Why open: If (A\subseteq\mathbb F_p^2) meets every line in at most two points, it is unknown whether all but (o(p)) points of (A) must lie on a cubic curve.
• Attack shape: proof
• Why an AI stack might dent it: Finite-prime classification can identify exceptional arc geometries, and Gröbner-basis interpolation can turn experimental structure into exact low-degree certificates.
• Sources: Ben Green, 100 Open Problems, Problem 68; Green and Tao, On sets defining few ordinary lines

P25. Improve the Heilbronn triangle exponent

• Slug: heilbronn-triangle-exponent
• Area: Discrete geometry
• Why open: For (n) points in a unit-area region, the conjectural smallest forced triangle area is (n^{-2+o(1)}), whereas the best published general upper bound cited in the 2025 update is (n^{-7/6+o(1)}).
• Attack shape: bound
• Why an AI stack might dent it: Incidence configurations and energy inequalities can be searched for the exact step losing exponent, with symbolic optimization and formal inequality checking.
• Sources: Ben Green, 100 Open Problems, Problem 77; Cohen, Pohoata, and Zakharov, A new upper bound for the Heilbronn triangle problem

P26. Carbery's large rectangle problem

• Slug: carbery-large-rectangle
• Area: Geometric measure theory / combinatorics
• Why open: If an open (A\subseteq[0,1]^2) has measure (\alpha), it is unknown whether four points of (A) form an axis-parallel rectangle of area at least (c\alpha^2); the best elementary guarantee loses a logarithm.
• Attack shape: bound
• Why an AI stack might dent it: Discretizations become dense bipartite graph problems suitable for extremal search, and a discovered dyadic or entropy inequality can be formally certified.
• Sources: Ben Green, 100 Open Problems, Problem 85; Carbery, Christ, and Wright, Multidimensional van der Corput and sublevel set estimates

P27. Exact Cohn–Elkies certificate for planar circle packing

• Slug: cohn-elkies-planar-certificate
• Area: Sphere packing / Fourier analysis
• Why open: It remains unknown whether the Cohn–Elkies linear-programming scheme itself can attain the sharp hexagonal circle-packing density in dimension 2, equivalently whether an exact admissible auxiliary function with the required optimal ratio exists.
• Attack shape: proof
• Why an AI stack might dent it: Numerical linear programming can guess a Gaussian-polynomial or modular-form ansatz, CAS can recognize exact coefficients, and Lean can certify the finite analytic reductions.
• Sources: Ben Green, 100 Open Problems, Problem 42; Cohn and Elkies, New upper bounds on sphere packings I

P28. The chromatic number of the plane

• Slug: hadwiger-nelson-plane-coloring
• Area: Discrete geometry / graph coloring
• Why open: The Hadwiger–Nelson number is known to be one of (5,6,7); no finite unit-distance graph forcing six colors and no valid coloring of the whole plane with five or six colors is known.
• Attack shape: counterexample
• Why an AI stack might dent it: Algebraic-coordinate graph generation plus SAT coloring can search for a finite 6-chromatic witness, with exact squared-distance and DRAT certificates.
• Sources: de Grey, The chromatic number of the plane is at least 5; current Hadwiger–Nelson problem summary

P29. Shrink the 509-vertex five-chromatic unit-distance graph

• Slug: smaller-five-chromatic-unit-distance-graph
• Area: Computational discrete geometry
• Why open: The smallest known planar five-chromatic unit-distance graph has 509 vertices, but minimality is unknown; finding any smaller exact-coordinate example is a clean open construction problem.
• Attack shape: counterexample
• Why an AI stack might dent it: Graph minimization, SAT unsatisfiability cores, algebraic-coordinate pruning, and exact certificate checking are precisely the demonstrated successful toolkit here.
• Sources: Parts, Graph minimization, focusing on 5-chromatic unit-distance graphs; Voronov et al., Constructing 5-chromatic unit distance graphs

P30. The five-dimensional kissing number

• Slug: kissing-number-dimension-five
• Area: Discrete geometry / spherical codes
• Why open: The exact kissing number (\tau_5) is between 40 and 44 and is widely expected to equal 40, but no proof excludes configurations of sizes 41–44.
• Attack shape: bound
• Why an AI stack might dent it: Semidefinite and interval-arithmetic searches can produce exact dual certificates for restricted configurations, with Lean checking the polynomial positivity core.
• Sources: current kissing-number bounds and bibliography; Boyvalenkov, Dodunekov, and Musin, A survey on the kissing numbers

P31. Existence of a projective plane of order 12

• Slug: projective-plane-order-twelve
• Area: Finite geometry / design theory
• Why open: Neither a projective plane of order 12 nor a proof of nonexistence is known; it would be a (2 ext{-}(157,13,1)) design, equivalently a complete set of 11 mutually orthogonal Latin squares of order 12.
• Attack shape: counterexample
• Why an AI stack might dent it: Symmetry-breaking SAT, exact-cover, and group-action decompositions can certify new forbidden automorphism types or produce a construction.
• Sources: Moorhouse, Projective Planes of Small Order; 2026 literature and catalogue audit

P32. The missing degree-57 Moore graph

• Slug: moore-graph-degree-57
• Area: Algebraic graph theory
• Why open: It is unknown whether a 57-regular graph on 3250 vertices with diameter 2 and girth 5 exists; a 2026 result further shows that any such graph has no involutory automorphism.
• Attack shape: counterexample
• Why an AI stack might dent it: The full graph is huge, but coherent-configuration equations, spectral modules, and automorphism cases yield smaller exact SAT and integer-algebra subproblems.
• Sources: Faber and Keegan, Existence of a Moore graph of degree 57 is still open; Ishida, No involutions in the missing Moore graph

P33. Frankl's union-closed sets conjecture

• Slug: union-closed-sets
• Area: Extremal set theory
• Why open: Every finite nontrivial union-closed family is conjectured to have an element appearing in at least half its sets; despite the 2022 constant-frequency breakthrough and many verified finite cases, the (1/2) threshold remains open.
• Attack shape: proof
• Why an AI stack might dent it: Integer programming can classify near-extremal frequency vectors, and entropy or averaging inequalities arising from those classifications are short enough for formal proof.
• Sources: Bruhn and Schaudt, The journey of the union-closed sets conjecture; Gilmer, A constant lower bound for the union-closed sets conjecture

P34. The $1/3$–$2/3$ conjecture for posets

• Slug: one-third-two-thirds-posets
• Area: Order theory / combinatorics
• Why open: Every finite non-chain poset is conjectured to contain incomparable (x,y) for which the probability that (x<y) in a random linear extension lies in ([1/3,2/3]); the general case is still open beyond many special classes.
• Attack shape: proof
• Why an AI stack might dent it: Exact linear-extension counting can classify minimal counterexamples under structural constraints, and reduction lemmas can be verified against exhaustive small-poset data.
• Sources: Chan and Pak, Linear extensions of finite posets; Open Conjecture Formalizations status list

P35. The three-sunflower conjecture

• Slug: three-sunflower-conjecture
• Area: Extremal set theory / complexity
• Why open: For a family of (w)-element sets with no three-sunflower, the best upper bound has base (O(\log w)), while Erdős–Rado predicts a constant base (C^w); the conjecture remains open even for three petals.
• Attack shape: bound
• Why an AI stack might dent it: Compression rules, entropy inequalities, and automated searches for robust-sunflower lemmas can target removal of one logarithmic factor.
• Sources: Rao, The story of sunflowers (2026); Alweiss, Lovett, Wu, and Zhang, Improved bounds for the sunflower lemma

P36. Caccetta–Häggkvist for directed triangles

• Slug: caccetta-haggkvist-k3
• Area: Directed graph theory
• Why open: The first open case asks whether every (n)-vertex digraph of minimum out-degree at least (n/3) contains a directed triangle.
• Attack shape: proof
• Why an AI stack might dent it: Flag-algebra SDP, exhaustive small counterexample search, and formal discharging can attack restricted degree profiles and improve the numerical threshold.
• Sources: AIM, A Summary of Problems and Results related to the Caccetta–Häggkvist Conjecture; Egres Open problem page

P37. Seymour's second-neighborhood conjecture

• Slug: seymour-second-neighborhood
• Area: Directed graph theory
• Why open: Every oriented graph is conjectured to contain a vertex with at least as many second out-neighbors as first out-neighbors; it remains widely open despite proofs for tournaments and several classes.
• Attack shape: proof
• Why an AI stack might dent it: Minimal-counterexample constraints can be SAT-enumerated, and a new reducible configuration or proof for another hereditary class is a meaningful short-campaign result.
• Sources: Espuny Díaz et al., Seymour's second neighbourhood conjecture: random graphs and reductions; 2026 small-order study

P38. Tuza's triangle packing-covering conjecture

• Slug: tuza-triangle-packing-covering
• Area: Extremal graph theory
• Why open: For every graph (G), Tuza conjectured that the minimum number (\tau(G)) of edges meeting all triangles satisfies (\tau(G)\le2\nu(G)), where (\nu(G)) is the maximum number of edge-disjoint triangles; it is open even for split graphs in full generality.
• Attack shape: proof
• Why an AI stack might dent it: ILP can identify extremal split or bounded-treewidth cases and synthesize local exchange rules that Lean can verify.
• Sources: Haxell, Packing and covering triangles in graphs; Botler et al., On Tuza's conjecture in dense graphs

P39. Push graph reconstruction beyond 13 vertices

• Slug: graph-reconstruction-next-order
• Area: Graph theory / computation
• Why open: The Kelly–Ulam reconstruction conjecture is verified for all graphs through 13 vertices but remains open in general; a fully certified verification at the next order, or a structural reduction that makes it possible, is itself open.
• Attack shape: bound
• Why an AI stack might dent it: Canonical labeling, deck hashing, symmetry reduction, and independently checkable certificates make the next finite frontier more realistic than attacking the whole conjecture.
• Sources: McKay, Reconstruction of small graphs and digraphs; 2026 current-status summary

P40. Erdős–Hajnal for the six-vertex path

• Slug: erdos-hajnal-p6
• Area: Ramsey theory / induced subgraphs
• Why open: The 2026 proof for (P_5) completed every forbidden graph on at most five vertices; the polynomial homogeneous-set bound for (P_6) is a sharp next case for which I found no resolution. Because six-vertex cases are moving quickly, recheck status immediately before launch.
• Attack shape: proof
• Why an AI stack might dent it: The recent (P_5) machinery supplies a concrete proof skeleton, while exhaustive decomposition of prime (P_6)-free graphs can suggest the missing structural lemma.
• Sources: Nguyen, Scott, and Seymour, Induced subgraph density VII: The five-vertex path; Erdős Problem #61 current history; Erdős–Hajnal beyond the five-vertex path

P41. Determine $R(5,5)$

• Slug: ramsey-r55
• Area: Ramsey theory
• Why open: The diagonal Ramsey number satisfies (43\le R(5,5)\le46) as of the April 2026 dynamic survey; deciding any of the three remaining gaps is open.
• Attack shape: bound
• Why an AI stack might dent it: Modern SAT with isomorph rejection can seek a 43-vertex Ramsey graph or certify nonexistence at 45, and proof logs can be independently checked.
• Sources: Radziszowski, Small Ramsey Numbers, revision 18 (2026); Angeltveit and McKay, $R(5,5)\le46$

P42. Determine the van der Waerden number $W(2,7)$

• Slug: van-der-waerden-w27
• Area: Ramsey theory / SAT
• Why open: (W(2,7)), the least (N) forcing a monochromatic seven-term arithmetic progression in every 2-coloring of ([N]), is the first unknown diagonal two-color value; only (W(2,7)>3703) and enormous general upper bounds are known.
• Attack shape: bound
• Why an AI stack might dent it: Symmetry-aware SAT and cyclic-zipper constructions can improve the lower bound with compact coloring certificates, even if exact determination remains out of reach.
• Sources: OEIS A005346; Rabung and Lotts, Improving the use of cyclic zippers in finding lower bounds for van der Waerden numbers

P43. Improve the lower bound for the seventh Schur number

• Slug: schur-number-seven-bound
• Area: Ramsey theory / additive combinatorics
• Why open: Only (S(1),\dots,S(5)) are known exactly, and (S(7)\ge1696) is far from general upper bounds; finding a larger certified seven-color sum-free partition is open.
• Attack shape: bound
• Why an AI stack might dent it: This is a direct SAT/CP construction task with tiny certificates relative to a proof of optimality, and the July 2026 shifted-template work exposes a fresh machine-discovered search language.
• Sources: Rowley, An Improved Lower Bound for $S(7)$; Bengone et al., Shifted S-templates and improved lower bounds for Schur numbers

P44. Lonely runner for 14 runners

• Slug: lonely-runner-fourteen
• Area: Diophantine approximation / computational combinatorics
• Why open: Computer-assisted work in 2025–26 established the conjecture through 13 runners; the next case, 14 runners (13 nonzero relative speeds), remains open to the best of the current literature screen.
• Attack shape: proof
• Why an AI stack might dent it: The recent finite-reduction and modular-sieving code path is explicit and designed to scale one case at a time, with rational interval certificates available for verification.
• Sources: Sungkawichai and Trakulthongchai, Eleven, twelve, and thirteen lonely runners; Trakulthongchai, Nine and Ten Lonely Runners

P45. The 33-point Erdős–Szekeres problem

• Slug: erdos-szekeres-seven
• Area: Discrete geometry / Ramsey theory
• Why open: (ES(7)) is the first unknown happy-ending number; the conjecture predicts (ES(7)=33), i.e. every 33 points in general position contain seven in convex position.
• Attack shape: proof
• Why an AI stack might dent it: Oriented-matroid encodings and SAT proof logging already reduced the (ES(6)) verification from thousands of CPU-hours to seconds, and recent notes focus specifically on the 33-point case.
• Sources: Notes on the 33-point Erdős–Szekeres problem; 2026 JCTA paper, The Erdős–Szekeres conjecture revisited

P46. The Brocard–Ramanujan factorial-square equation

• Slug: brocard-ramanujan-factorial-square
• Area: Diophantine equations
• Why open: The only known positive solutions of (n!+1=m^2) have (n=4,5,7); proving there are no others, or producing another, remains open.
• Attack shape: proof
• Why an AI stack might dent it: Modular obstruction mining, (p)-adic valuation arguments, and exact computation can eliminate new infinite residue families even if the full conjecture is out of reach.
• Sources: Google DeepMind Formal Conjectures issue #1417; Berndt and Galway, On the Brocard–Ramanujan Diophantine equation; OEIS A085692

P47. Uniqueness of Markov numbers

• Slug: markov-number-unicity
• Area: Diophantine equations
• Why open: Frobenius's unicity conjecture says a Markov triple is determined, up to ordering, by its largest entry; despite many equivalent formulations and special cases, the general statement remains open.
• Attack shape: proof
• Why an AI stack might dent it: The Markov tree, continued fractions, cluster mutations, and symbolic inequalities give a discrete search space where equality cases can be mined and formalized.
• Sources: Aigner, Markov's Theorem and 100 Years of the Uniqueness Conjecture; Fisac, Markov's conjecture on integral necklaces

P48. Amenability of Thompson's group $F$

• Slug: thompson-f-amenability
• Area: Geometric group theory
• Why open: Whether Thompson's group (F) is amenable remains unresolved after decades; note that the broader existence of non-sofic groups was settled in August 2026, but it does not decide this problem.
• Attack shape: counterexample
• Why an AI stack might dent it: Large finite Cayley subgraphs, diagram-group normal forms, and group-ring equations permit certified searches for better Følner ratios or explicit nonamenability witnesses.
• Sources: Guba, Amenability problem for Thompson's group F: state of the art; OpenAI, Ten Advances (non-sofic result, for status separation)

P49. Expansion from random generators of alternating groups

• Slug: random-alternating-group-expansion
• Area: Group theory / expander graphs
• Why open: For fixed (k\ge2), it is unknown whether (k) random elements of (A_n) almost surely form an expanding generating set, equivalently whether the associated random walk mixes in (O(n\log n)).
• Attack shape: bound
• Why an AI stack might dent it: Representation-theoretic calculations can be automated for restricted cycle types, and a new spectral-gap estimate for one structured random model would be a genuine partial advance.
• Sources: Ben Green, 100 Open Problems, Problem 79; Helfgott, Seress, and Żuk, Random generators of the symmetric group: diameter, mixing time and spectral gap

P50. Remove the logarithmic loss in permanent formula lower bounds

• Slug: permanent-formula-log-loss
• Area: Arithmetic circuit complexity
• Why open: The August 2026 bound says division-free arithmetic formulas for the (n\times n) permanent require (\Omega(n^4/\log n)) leaves; proving (\Omega(n^4)), or any asymptotic improvement that removes part of the logarithmic loss, is a sharp open continuation.
• Attack shape: bound
• Why an AI stack might dent it: The new argument is already Lean-certified and decomposes into algebraic-geometry and matching lemmas, giving a trustworthy base from which automated proof search can target exactly the loss-producing step.
• Sources: OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, Chapter 5; Lean certificates repository

Most dentable 10

My rough overnight/short-campaign ranking is: P43 (a better (S(7)) construction), P29 (shrink the 509-vertex graph), P13 (structure in the Hofstadter closure), P44 (scale the new lonely-runner sieve one case), P06 (small-prime structure for unique-sum-free sets), P23 (new no-three-in-line finite records or obstructions), P21 (a better (C_7) graph-power bound), P39 (certified reconstruction at the next finite frontier), P42 (improve the (W(2,7)) lower bound), and P22 (new radius-two linear covering-code construction or obstruction). These rank highly because a finite certificate or a strict bound improvement would already be publishable residue, even without resolving the parent conjecture.