Subjects

Combinatorics

37 results from OpenAI’s math release. 37 explained so far. OpenAI has published Lean proofs for 33: 29 of the main theorem, 4 of part of the claim.

See these in the full list, with search and filters.

• 155 A counterexample to periodic tiling in dimension three

  Constructs a finite translational tile in ℤ³ that tiles space but admits no fully periodic tiling, disproving the periodic tiling conjecture in the smallest possible lattice dimension. Its unit-cube thickening gives the same counterexample in ℝ³, even with arbitrary real translation vectors.

  ▶Episode, 6:54 OpenAI published a Lean proof of the main theorem.

• 156 Borsuk's conjecture fails in dimension nine

  Constructs a compact subset of ℝ⁹ that cannot be covered by ten sets of strictly smaller diameter, disproving Borsuk's covering assertion already in dimension nine. The example consists of rank-one orthogonal projectors onto lines in ℝ⁴, with the Frobenius metric.

  ▶Episode, 6:00 OpenAI published a Lean proof of the main theorem.

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

  Disproves Hadwiger's conjecture even for fractional coloring: arbitrarily large finite simple graphs with independence number at most two satisfy $\chi_f(G)\gt h(G)$, where $h(G)$ is the largest clique-minor order. Also disproves the fractional Colin de Verdière chromatic bound $\chi_f(G)\le\mu(G)+1$. In the positive direction, every finite nonempty graph satisfies $\chi_{\mathrm{list}}(G)\le C h(G)$ for a universal constant C.

  3 papers ▶Episode, 6:47 OpenAI published a Lean proof of the main theorem.

• 158 The Euclidean plane cannot be colored with five colors

  Proves that every five-coloring of the Euclidean plane has a monochromatic pair at distance one, with no restriction on the color classes. This advances the Hadwiger–Nelson problem: together with the classical seven-coloring, only six and seven remain possible chromatic numbers of the plane.

  ▶Episode, 6:33 OpenAI published a Lean proof of the main theorem.

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

  Proves Erdős's conjecture that every set of positive integers with divergent reciprocal sum contains arithmetic progressions of every finite length. Quantitatively, for each fixed k ≥ 3, every subset of $\{1,\ldots,N\}$ with no nonconstant k-term progression has size at most $C_kN\exp[-c_k(\log N)^{\varepsilon_k}]$, with positive constants depending only on k.

  ▶Episode, 6:10 OpenAI published a Lean proof of the main theorem.

• 160 Superexponential van der Waerden numbers

  Resolves Erdős's superexponential-growth question for van der Waerden numbers. If $W_r(k)$ is the least interval length forcing a monochromatic k-term progression in every r-coloring, then $W_r(k)\gt k^{ck\lfloor\log_2 r\rfloor}$ for an absolute c > 0, all r ≥ 2 and sufficiently large k, uniformly in r. In particular, $W_r(k)^{1/k}\to\infty$ for each fixed r.

  ▶Episode, 6:28 OpenAI published a Lean proof of the main theorem.

• 161 Counterexamples to Sidorenko’s conjecture and the forcing conjecture

  Disproves Sidorenko's conjecture with a connected bipartite pattern on 35 vertices and 66 edges that occurs less frequently than in a random graph of the same edge density. The same pattern disproves the forcing conjecture of Skokan and Thoma: matching its density and the edge density of a constant graphon need not force quasirandomness.

  ▶Episode, 6:29 OpenAI published a Lean proof of the main theorem.

• 162 Counterexamples to Ryser’s covering conjecture

  Disproves Ryser's covering conjecture by constructing intersecting $(q+1)$-partite, $(q+1)$-uniform hypergraphs with covering number $q+1$, rather than the predicted bound q, for every sufficiently large prime q. A separate construction over extension fields also disproves Gyárfás's monochromatic tree-cover conjecture.

  2 papers ▶Episode, 6:31 OpenAI published a Lean proof of the main theorem.

• 164 Hindman’s finite sums and products conjecture

  Proves Hindman's finite sums and products conjecture: every finite coloring of the positive integers contains sets of any prescribed finite size whose nonempty subset sums and nonempty subset products all have one common color.

  ▶Episode, 5:42

• 165 The Harary–Hill and Zarankiewicz crossing-number formulas

  Resolves the Harary–Hill conjecture and Turán's brickyard problem in the Zarankiewicz formulation, determining the crossing numbers of every complete and complete bipartite graph. The result proves the optimality of the classical drawings among all plane drawings with continuous edge arcs.

  2 papers ▶Episode, 5:53 OpenAI published a Lean proof of the main theorem.

• 166 The higher-dimensional Erdős distinct-distances conjecture

  For every fixed d ≥ 3, any n ≥ 2 distinct points in ℝ^d determine at least $c_dn^{2/d}$ distinct distances, with $c_d\gt 0$ depending only on dimension. This matches the integer-grid order and resolves the higher-dimensional Erdős distinct-distances conjecture with a constant-factor bound.

  ▶Episode, 5:48

• 167 Planar distinct distances and unit-distance bounds

  Proves the weak pinned Erdős distance conjecture: for every fixed ε > 0, all but $o(n)$ points of any n-point planar set determine at least $n^{1-\varepsilon}$ distinct nonzero distances. A complementary theorem bounds the number of unit-distance pairs by $O(n^{4/3-\delta})$ for an absolute δ > 0.

  2 papers ▶Episode, 6:52 OpenAI published a Lean proof of the main theorem.

• 168 Combinatorial invariance of Kazhdan–Lusztig polynomials

  Resolves the full combinatorial invariance conjecture: isomorphic Bruhat intervals in arbitrary Coxeter systems have identical equal-parameter Kazhdan–Lusztig polynomials. Thus the abstract order of the interval determines the polynomial, even across different Coxeter systems.

  ▶Episode, 5:47 OpenAI published a Lean proof of the main theorem.

• 169 Shareshian–Wachs elementary positivity

  Resolves the elementary-positivity part of the Shareshian–Wachs conjecture: the chromatic quasisymmetric function of every natural unit interval graph has elementary-basis coefficients in $\mathbb N[q]$. The coefficients count explicitly described permutations, giving a combinatorial explanation of positivity.

  ▶Episode, 5:44 OpenAI published a Lean proof of the main theorem.

• 170 Sharp logarithmic exponents for off-diagonal Ramsey numbers

  For every fixed integer s ≥ 5, proves $r(s,t)=t^{s-1}/(\log t)^{s-2+o(1)}$ as $t\to\infty$, determining the logarithmic exponent and matching the classical upper bound at that scale. Here $r(s,t)$ is the least number of vertices forcing an s-clique or a t-vertex independent set.

  2 papers ▶Episode, 5:36 OpenAI published a Lean proof of the main theorem.

• 171 The hypercube Ramsey conjecture

  Resolves the Burr–Erdős hypercube Ramsey conjecture: the two-color Ramsey number of the n-dimensional cube is $\Theta(2^n)$. Thus every red-blue coloring of a complete graph on a universal constant times the cube's number of vertices contains a monochromatic copy of the cube.

  ▶Episode, 5:49

• 172 Classification of finite Euclidean Ramsey configurations

  Classifies finite point configurations that occur monochromatically, at their original scale, in every finite coloring of sufficiently high-dimensional Euclidean space. The characterization is an algebraic condition over the coordinate field. It also disproves the Leader–Russell–Walters conjecture that every such configuration is a subset of a finite transitive set.

  ▶Episode, 6:22 OpenAI published a Lean proof of the main theorem.

• 173 Seymour’s second-neighborhood conjecture

  Proves Seymour's second-neighborhood conjecture: every nonempty finite oriented graph has a vertex with at least as many vertices at directed distance exactly two as at directed distance one. Oriented graphs may be arbitrary apart from the exclusion of loops and oppositely directed edge pairs.

  ▶Episode, 5:24 OpenAI published a Lean proof of the main theorem.

• 174 Deterministic construction of strong thin spanning trees

  Resolves the strong thin-tree conjecture constructively. Every finite loopless k-edge-connected multigraph on at least two vertices has a spanning tree containing at most a universal $C/k$ fraction of the edges of every cut. Such a tree can be found deterministically in polynomial time, even with binary-encoded parallel-edge multiplicities.

  2 papers ▶Episode, 6:55 OpenAI published a Lean proof of the main theorem.

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

  Proves that integral and fractional expectation thresholds differ by at most a universal factor, and resolves Talagrand's discrete-convexity conjecture. An application proves the Ascoli–He–Park–Talagrand graph-decomposition conjecture: every graph's edges split into a universally bounded number of fixed pieces, each with containment threshold at most a universal constant times the original graph's integral expectation threshold. The pieces' embeddings need not agree on shared vertices.

  3 papers ▶Episode, 7:13 OpenAI published a Lean proof of the main theorem.

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

  Proves the second Kahn–Kalai conjecture: for every finite simple graph H with h ≥ 1 edges and at most n vertices, its appearance threshold in $G(n,p)$ is at most $C p_{\mathrm E}(n,H)(1+\log_2 h)$, with universal C. Here $p_{\mathrm E}$ is the least density at which every subgraph of H has expected copy count at least 1/2.

  ▶Episode, 5:37 OpenAI published a Lean proof of the main theorem.

• 177 Bounded-degree coboundary expanders

  Constructs arbitrarily large finite d-dimensional simplicial complexes, for every d ≥ 3, with uniformly bounded vertex degrees and uniform 𝔽₂ coboundary expansion in every degree below d. Together with the known graph and two-dimensional cases, this establishes the existence of such expanders in every positive dimension.

  ▶Episode, 6:52 OpenAI published a Lean proof of the main theorem.

• 178 Deterministic nonbipartite Ramanujan graphs in every fixed degree

  For every fixed d ≥ 3, constructs a simple d-regular nonbipartite Ramanujan graph on every sufficiently large even number n of vertices, with every nonconstant adjacency eigenvalue strictly between $-2\sqrt{d-1}$ and $2\sqrt{d-1}$. A deterministic algorithm outputs the full adjacency list in polynomial bit time, with exponent depending on d.

  ▶Episode, 7:05

• 179 The circulant Hadamard and Barker-sequence conjectures

  Proves that real circulant Hadamard matrices exist exactly in orders 1 and 4, resolving the circulant Hadamard conjecture. Together with classical Barker-sequence results, this shows that binary sequences whose nontrivial aperiodic autocorrelations have magnitude at most 1 exist at lengths n > 1 exactly when $n\in\{2,3,4,5,7,11,13\}$.

  ▶Episode, 6:00 OpenAI published a Lean proof of the main theorem.

• 180 Barnette’s Hamiltonian-cycle conjecture

  Proves that every finite simple cubic bipartite planar 3-vertex-connected graph has a Hamiltonian cycle, resolving Barnette's conjecture. Equivalently, every three-edge path in a finite simple cubic 3-vertex-connected bipartite Pfaffian graph lies in a Hamiltonian cycle.

  ▶Episode, 5:48 OpenAI published a Lean proof of the main theorem.

• 181 The Erdős–Gallai cycle-decomposition conjecture

  Proves that the edges of every finite simple undirected graph on n vertices can be partitioned into at most $Cn$ simple cycles and single edges, for an absolute constant C. This resolves the Erdős–Gallai cycle-decomposition conjecture, bounding the number of pieces linearly even for dense graphs.

  ▶Episode, 7:04 OpenAI published a Lean proof of the main theorem.

• 182 Power savings for intersective polynomial differences and prime arguments

  For every fixed intersective integer polynomial h of degree k ≥ 2 with positive leading coefficient, proves that a subset of $\{1,\ldots,N\}$ avoiding nonzero values $h(1),h(2),\ldots$ as differences has size $O_h(N^{1-c_k})$, with $c_k\gt 0$ depending only on degree. Here intersective means having a root modulo every modulus. For prime arguments, a power saving also holds when h has a unit root modulo every modulus, with exponent allowed to depend on h.

  3 papers ▶Episode, 7:01 OpenAI published a Lean proof of part of the claim.

• 183 Power savings for planar halving lines and k-sets

  Improves the planar halving-line bound to $O(n^{4/3-\varepsilon})$ for sets with no three collinear and an absolute ε > 0. More generally, an n-point set with no three collinear has $O(n(k+1)^{1/3-\varepsilon_0})$ strictly separable k-subsets for $1\le k\le n/2$, with an absolute $\varepsilon_0\gt 0$. The constants and positive exponents are nonquantitative.

  ▶Episode, 5:59 OpenAI published a Lean proof of the main theorem.

• 184 Correspondence coloring with a fixed forbidden subgraph

  Proves the Alon–Krivelevich–Sudakov coloring conjecture in correspondence-coloring form: graphs avoiding any fixed subgraph F need $O_F(\Delta/\log\Delta)$ colors when their maximum degree Δ is sufficiently large. Also proves the Ajtai–Erdős–Komlós–Szemerédi independence conjecture: for fixed r ≥ 4, every n-vertex K_r-free graph of average degree d ≥ 2 has an independent set of size $\Omega_r(n\log d/d)$.

  2 papers ▶Episode, 8:18 OpenAI published a Lean proof of part of the claim.

• 185 Counterexamples to infinite matroid intersection and packing/covering

  Disproves the unrestricted infinite matroid intersection and packing/covering conjectures in ZFC, using two self-dual partitional matroids on a countably infinite ground set. The same examples answer Joó’s partitional-matroid question negatively. They are neither finitary nor cofinitary, so Nash-Williams’ original finitary conjecture remains outside the result.

  ▶Episode, 7:36 OpenAI published a Lean proof of the main theorem.

• 186 Uniform influence and sharp thresholds for graph and hypergraph properties

  Proves the Friedgut–Kalai threshold-width conjectures for graphs and fixed-uniformity hypergraphs. For fixed $0\lt \varepsilon\lt 1/2$, every nontrivial increasing relabeling-invariant property crosses from probability ε to $1-\varepsilon$ within width $O((\log n)^{-2})$ for graphs and $O_r((\log n)^{-r/(r-1)})$ for r-uniform hypergraphs, r ≥ 3. The hypergraph influence bound also applies to nonmonotone properties.

  2 papers ▶Episode, 8:42 OpenAI published a Lean proof of part of the claim.

• 187 Snaky in 21 Maker moves

  Settles the Snaky achievement problem: Maker can force the six-cell Snaky shape within 21 of its own moves on the initially empty infinite square board. Maker moves first, each player claims one free cell per turn, and translations, rotations and reflections count as wins.

  ▶Episode, 6:46 OpenAI published a Lean proof of the main theorem.

• 188 The sharp terminal leave in random triangle removal

  Starting from the complete graph on n vertices, repeatedly delete a uniformly chosen remaining triangle. The terminal edge count is asymptotic to $n^{3/2}/(2\sqrt2)$, with mean-square convergence after normalization by n^3/2. This proves the triangle case of the Joos–Kühn sharp-constant conjecture.

  ▶Episode, 6:30 OpenAI published a Lean proof of the main theorem.

• 189 Cycle–clique Ramsey numbers

  Proves the Erdős–Faudree–Rousseau–Schelp conjecture: $R(C_m,K_n)=(m-1)(n-1)+1$ for every $m\ge n\ge3$, except $R(C_3,K_3)=6$. This is the exact threshold forcing a red m-cycle or a blue n-clique in every red–blue coloring of a complete graph.

  ▶Episode, 6:46 OpenAI published a Lean proof of the main theorem.

• 190 Polynomial removal fails for ordered binary matrices

  Disproves polynomial ordered binary matrix removal with one fixed $66\times66$ zero–one pattern. Matrices can require many binary-entry changes to become pattern-free while their copy density is smaller than every proposed polynomial bound in that distance. Copies preserve row and column orders and match both zeros and ones.

  ▶Episode, 7:29 OpenAI published a Lean proof of the main theorem.

• 191 A power improvement in the Heilbronn triangle lower bound

  For every sufficiently large n, constructs n points in the unit square such that every triangle has area at least $n^{-2+c}$ for one absolute c > 0. This disproves the conjectured almost-n⁻² upper bound in Heilbronn's triangle problem, which asks how large the smallest determined triangle can be.

  ▶Episode, 7:02 OpenAI published a Lean proof of part of the claim.

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

  Disproves the proposed square-root bound relating a Boolean function's linear Fourier coefficients to its polynomial degree. For every C > 0, there is a sign-valued Boolean function f with $\sum_i\widehat f(\{i\})\gt C\sqrt{\deg(f)}$. Thus its total signed correlation with individual input bits can exceed the proposed bound by an arbitrary factor.

  ▶Episode, 5:59 OpenAI published a Lean proof of the main theorem.

Summary and paper titles from OpenAI’s catalog, used under the Apache License 2.0. Last checked October 19, 2026.