Skip
← Map

Combinatorics

37 families · 33 verified by lean

This page gathers the 37 result families that the openai/math repository catalogues under Combinatorics. Each claim comes from a manuscript; 33 of them have a Lean formalization checked by software, and the other 4 are still to be verified. Open any card to read a plain-language explainer, the original statement and its sources.

№ 155

A counterexample to periodic tiling in dimension three

Constructs a finite translational tile in ℤ3 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 ℝ3, even with arbitrary real translation vectors.

Verified by Lean1 manuscript
№ 156

Borsuk's conjecture fails in dimension nine

Constructs a compact subset of ℝ9 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 ℝ4, with the Frobenius metric.

Verified by Lean1 manuscript
№ 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 , where is the largest clique-minor order. Also disproves the fractional Colin de Verdière chromatic bound . In the positive direction, every finite nonempty graph satisfies for a universal constant C.

Verified by Lean3 manuscripts
№ 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.

Verified by Lean1 manuscript
№ 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 with no nonconstant k-term progression has size at most , with positive constants depending only on k.

Verified by Lean Reasoning summary1 manuscript
№ 160

Superexponential van der Waerden numbers

Resolves Erdős's superexponential-growth question for van der Waerden numbers. If is the least interval length forcing a monochromatic k-term progression in every r-coloring, then for an absolute c > 0, all r ≥ 2 and sufficiently large k, uniformly in r. In particular, for each fixed r.

Verified by Lean1 manuscript
№ 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.

Verified by Lean1 manuscript
№ 162

Counterexamples to Ryser’s covering conjecture

Disproves Ryser's covering conjecture by constructing intersecting -partite, -uniform hypergraphs with covering number , 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.

Verified by Lean2 manuscripts
№ 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.

To be verified1 manuscript
№ 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.

Verified by Lean2 manuscripts
№ 166

The higher-dimensional Erdős distinct-distances conjecture

For every fixed d ≥ 3, any n ≥ 2 distinct points in ℝd determine at least distinct distances, with 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.

To be verified1 manuscript
№ 167

Planar distinct distances and unit-distance bounds

Proves the weak pinned Erdős distance conjecture: for every fixed ε > 0, all but points of any n-point planar set determine at least distinct nonzero distances. A complementary theorem bounds the number of unit-distance pairs by for an absolute δ > 0.

Verified by Lean2 manuscripts
№ 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.

Verified by Lean1 manuscript
№ 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 . The coefficients count explicitly described permutations, giving a combinatorial explanation of positivity.

Verified by Lean1 manuscript
№ 170

Sharp logarithmic exponents for off-diagonal Ramsey numbers

For every fixed integer s ≥ 5, proves as , determining the logarithmic exponent and matching the classical upper bound at that scale. Here is the least number of vertices forcing an s-clique or a t-vertex independent set.

Verified by Lean2 manuscripts
№ 171

The hypercube Ramsey conjecture

Resolves the Burr–Erdős hypercube Ramsey conjecture: the two-color Ramsey number of the n-dimensional cube is . 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.

To be verified1 manuscript
№ 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.

Verified by Lean1 manuscript
№ 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.

Verified by Lean1 manuscript
№ 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 fraction of the edges of every cut. Such a tree can be found deterministically in polynomial time, even with binary-encoded parallel-edge multiplicities.

Verified by Lean2 manuscripts
№ 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.

Verified by Lean3 manuscripts
№ 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 is at most , with universal C. Here is the least density at which every subgraph of H has expected copy count at least 1/2.

Verified by Lean1 manuscript
№ 177

Bounded-degree coboundary expanders

Constructs arbitrarily large finite d-dimensional simplicial complexes, for every d ≥ 3, with uniformly bounded vertex degrees and uniform 𝔽2 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.

Verified by Lean1 manuscript
№ 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 and . A deterministic algorithm outputs the full adjacency list in polynomial bit time, with exponent depending on d.

To be verified1 manuscript
№ 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 .

Verified by Lean1 manuscript
№ 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.

Verified by Lean1 manuscript
№ 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 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.

Verified by Lean1 manuscript
№ 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 avoiding nonzero values as differences has size , with 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.

Verified by Lean3 manuscripts
№ 183

Power savings for planar halving lines and k-sets

Improves the planar halving-line bound to for sets with no three collinear and an absolute ε > 0. More generally, an n-point set with no three collinear has strictly separable k-subsets for , with an absolute . The constants and positive exponents are nonquantitative.

Verified by Lean1 manuscript
№ 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 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 Kr-free graph of average degree d ≥ 2 has an independent set of size .

Verified by Lean2 manuscripts
№ 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.

Verified by Lean1 manuscript
№ 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 , every nontrivial increasing relabeling-invariant property crosses from probability ε to within width for graphs and for r-uniform hypergraphs, r ≥ 3. The hypergraph influence bound also applies to nonmonotone properties.

Verified by Lean2 manuscripts
№ 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.

Verified by Lean1 manuscript
№ 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 , with mean-square convergence after normalization by n3/2. This proves the triangle case of the Joos–Kühn sharp-constant conjecture.

Verified by Lean1 manuscript
№ 189

Cycle–clique Ramsey numbers

Proves the Erdős–Faudree–Rousseau–Schelp conjecture: for every , except . This is the exact threshold forcing a red m-cycle or a blue n-clique in every red–blue coloring of a complete graph.

Verified by Lean1 manuscript
№ 190

Polynomial removal fails for ordered binary matrices

Disproves polynomial ordered binary matrix removal with one fixed 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.

Verified by Lean1 manuscript
№ 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 for one absolute c > 0. This disproves the conjectured almost-n−2 upper bound in Heilbronn's triangle problem, which asks how large the smallest determined triangle can be.

Verified by Lean1 manuscript
№ 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 . Thus its total signed correlation with individual input bits can exceed the proposed bound by an arbitrary factor.

Verified by Lean1 manuscript