The mathematics of finite and discrete structures — counting the arrangements of a set, deciding when a configuration meeting prescribed constraints can exist, and characterizing the patterns such structures are forced to contain. It encompasses enumerative and extremal combinatorics, graph theory, design theory, and additive combinatorics, with deep ties to algebra, probability, and computer science.
Missions
Captain: Shuze Chen
The Polynomial Hirsch ConjectureOpen Problem
## Motivation
The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a $d$-dimensional polytope with $n$ facets is at most $n - d$. Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the **polynomial Hirsch conjecture**: is the diameter bounded by a polynomial in $n$ and $d$?
## Timeline
- **1957.** Hirsch states the conjecture $\mathrm{diam} \le n - d$ in a letter to Dantzig, who publishes it in *Linear Programming and Extensions* (1963).
- **1964–1966.** Klee determines the exact maximum diameter of $3$-polytopes with $n$ facets, $\lfloor 2n/3\rfloor - 1$ — the Hirsch bound holds up to dimension three.
- **1967.** Klee and Walkup ([Acta Math.](https://doi.org/10.1007/BF02392971)) refute the *unbounded-polyhedron* version, prove the bounded conjecture for $n - d \le 5$, and reduce the general case to the **$d$-step conjecture** ($n = 2d$).
- **1970.** Larman ([Proc. LMS](https://doi.org/10.1112/plms/s3-20.2.249)) proves $\mathrm{diam} \le n\,2^{d-3}$ — linear in the number of facets for each fixed dimension, still the best bound of that shape.
- **1989.** Naddef ([Math. Programming](https://doi.org/10.1007/BF01589418)) proves $0/1$-polytopes satisfy the Hirsch bound, with diameter at most $d$.
- **1992.** Kalai and Kleitman ([Bull. AMS](https://arxiv.org/abs/math/9204233)) prove $\mathrm{diam} \le n^{\log_2 d + 2}$ in under a page — the quasi-polynomial barrier every later bound refines. The same year brings subexponential pivot rules (Kalai; Matoušek–Sharir–Welzl), the algorithmic counterpart.
- **2010.** Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR](https://doi.org/10.1287/moor.1100.0470)) show the known upper-bound arguments survive in a purely combinatorial abstraction — which admits almost-quadratic lower bounds, so a polynomial bound must use real geometry. Kalai launches **Polymath 3** on the polynomial version.
- **2010–2012.** Santos ([Annals of Math.](https://arxiv.org/abs/1006.2814)) disproves the Hirsch conjecture: a $43$-dimensional polytope with $86$ facets and diameter at least $44$, via spindles of large width.
- **2014–2019.** Todd ([SIAM J. Discrete Math.](https://arxiv.org/abs/1402.3579)) sharpens Kalai–Kleitman to $(n-d)^{\log_2 d}$; Sukegawa refines further. Matschke, Santos, and Weibel ([Proc. LMS 2015](https://arxiv.org/abs/1202.4701)) shrink the counterexample to dimension $20$ with $40$ facets and diameter $21$. All known violations remain constant-factor; all known bounds remain quasi-polynomial.
## Setting
Work in $\mathbb{R}^d$. An **H-polytope** is a set cut out by finitely many linear inequalities: given vectors $a_1, \dots, a_n \in \mathbb{R}^d$ and reals $b_1, \dots, b_n$, it is
$$P \;=\; \{\, x \in \mathbb{R}^d \mid \langle a_i, x\rangle \le b_i \text{ for } i = 1, \dots, n \,\},$$
where $\langle a_i, x\rangle = \sum_{j=1}^d a_{ij} x_j$ is the standard inner (dot) product — so each condition $\langle a_i, x\rangle \le b_i$ is one linear inequality, with normal vector $a_i$ and offset $b_i$. Throughout, $P$ is assumed nonempty and bounded. The parameter $n$ counts the inequalities in the given description; since every polytope with $f$ facets admits a description by exactly $f$ inequalities, bounds stated in terms of $n$ over all descriptions are equivalent to bounds in terms of facet counts.
A **vertex** of $P$ is an extreme point. Two vertices $u \ne v$ are **adjacent** when the segment $[u, v]$ is an extreme subset of $P$; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that $[u,v]$ is a one-dimensional face — an **edge**. The **combinatorial diameter** of $P$ is the diameter of the graph of vertices and edges. Throughout, "diameter at most $B$" is expressed as: every two vertices are joined by a walk of $B$ steps, each step staying put or crossing an edge — a form that is monotone in $B$ and asserts connectivity of the graph (Balinski's theorem) as part of the claim.
## Formalization targets
### Goal — the polynomial Hirsch conjecture
$$\exists\, c, k \in \mathbb{N}:\ \text{every nonempty bounded } P = \{x \in \mathbb{R}^d \mid \langle a_i, x \rangle \le b_i,\ i \le n\} \text{ has diameter} \le c\,(n + d)^k.$$
Every polynomial in $n$ and $d$ is dominated by some $c(n+d)^k$ and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.
### Milestones — the known ladder
Six classical results over the same definitions: the Hirsch bound $n - d$ in dimension $d \le 3$ (Klee; Klee–Walkup); Larman's bound $n \cdot 2^{d-3}$; Naddef's bound $d$ for $0/1$-polytopes; the Kalai–Kleitman bound $n^{\log_2 d + 2}$; Todd's bound $(n-d)^{\log_2 d}$ for full-dimensional $P$ with $n \ge d \ge 3$; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds $n - d$.
## Significance
A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR 2010](https://doi.org/10.1287/moor.1100.0470)) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.
None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.
## Difficulty
The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving *any* polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters *large* is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.
## Formalization scope
The Lean model commits to: ambient space `EuclideanSpace ℝ (Fin d)`; the polytope as `Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i}` for `a : Fin n → EuclideanSpace ℝ (Fin d)`, `b : Fin n → ℝ`, with nonemptiness and `Bornology.IsBounded` as explicit hypotheses (boundedness is essential: Klee–Walkup's *unbounded* counterexample would otherwise trivialize the Santos milestone); vertices as `Set.extremePoints ℝ`; adjacency as `u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v)`; and diameter bounds as the walk predicate `DiamLE`, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through `Real.logb` and the natural floor. In `larman_bound` and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all $n, d$ in scope. The dimension parameter $d$ is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with `todd_bound` requiring full-dimensionality (`(interior P).Nonempty`) as in its source.
Welcome contributions: any milestone in any order (`dimension_three_bound` for $d \le 1$ cases and structural lemmas about `Adj` and `DiamLE` are natural entry points, and `kalai_kleitman_bound` is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.
## Selected references
- V. Klee, D. Walkup, *The d-step conjecture for polyhedra of dimension d < 6*, Acta Math. 117 (1967). [doi:10.1007/BF02392971](https://doi.org/10.1007/BF02392971)
- D. Larman, *Paths on polytopes*, Proc. London Math. Soc. 20 (1970). [doi:10.1112/plms/s3-20.2.249](https://doi.org/10.1112/plms/s3-20.2.249)
- D. Naddef, *The Hirsch conjecture is true for (0,1)-polytopes*, Math. Programming 45 (1989). [doi:10.1007/BF01589418](https://doi.org/10.1007/BF01589418)
- G. Kalai, D. Kleitman, *A quasi-polynomial bound for the diameter of graphs of polyhedra*, Bull. AMS 26 (1992). [arXiv:math/9204233](https://arxiv.org/abs/math/9204233)
- F. Santos, *A counterexample to the Hirsch conjecture*, Annals of Mathematics 176 (2012). [arXiv:1006.2814](https://arxiv.org/abs/1006.2814)
- M. Todd, *An improved Kalai–Kleitman bound for the diameter of a polyhedron*, SIAM J. Discrete Math. 28 (2014). [arXiv:1402.3579](https://arxiv.org/abs/1402.3579)
- B. Matschke, F. Santos, C. Weibel, *The width of five-dimensional prismatoids*, Proc. London Math. Soc. 110 (2015). [arXiv:1202.4701](https://arxiv.org/abs/1202.4701)
- F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, *Diameter of polyhedra: limits of abstraction*, Math. Oper. Res. 35 (2010). [doi:10.1287/moor.1100.0470](https://doi.org/10.1287/moor.1100.0470)
- F. Santos, *Recent progress on the combinatorial diameter of polytopes and simplicial complexes*, TOP 21 (2013) (survey). [arXiv:1307.5900](https://arxiv.org/abs/1307.5900)
18 thms2 active usersReviewed
Captain: ShouqiaoWang
Erdős Problem 390: Exact Second-Order AsymptoticResearch Paper
Determine the exact second-order term in the least possible largest factor in a factorization of $n!$ into distinct integers exceeding $n$, with the proposed rational constant $4029639598/25970038185$.
6 thms2 active usersReviewed
Captain: ShouqiaoWang
Cubic Congruence for the q-Secant Inversion EnumeratorResearch Paper
## Motivation
Alternating permutations are a classical meeting point of enumerative combinatorics, permutation statistics, and special functions. An up--down permutation alternates between rises and falls, and their ordinary counts are the Euler secant and tangent numbers. Refining this count by the inversion statistic produces the $q$-secant polynomial $E_{2n}(q)$. Its values and congruences retain information that disappears after setting $q=1$: they distinguish how the alternating permutations are distributed by inversion number and reveal cancellation at roots such as $q=-1$. Ji-Cai Liu's article isolates the next nontrivial term in the $(1+q)$-adic expansion of this polynomial, strengthening an earlier Andrews--Foata congruence. The mission formalizes the article's main result, Theorem 1.1, as an exact polynomial-divisibility statement.
## Setting
For $n\ge 0$, let $A(2n)$ be the set of permutations $\sigma=(\sigma_1,\ldots,\sigma_{2n})$ of $\{1,\ldots,2n\}$ satisfying
$$
\sigma_1<\sigma_2>\sigma_3<\sigma_4>\cdots<\sigma_{2n}.
$$
The empty permutation is the unique member of $A(0)$. The inversion number is
$$
\operatorname{inv}(\sigma)
=\#\{(i,j):1\le i<j\le 2n,\ \sigma_i>\sigma_j\}.
$$
The $q$-secant inversion enumerator is the integer polynomial
$$
E_{2n}(q)=\sum_{\sigma\in A(2n)}q^{\operatorname{inv}(\sigma)}\in\mathbb Z[q].
$$
Congruence modulo $(1+q)^3$ means divisibility in $\mathbb Z[q]$: two polynomials $F$ and $G$ are congruent precisely when $(1+q)^3$ divides $F-G$. This formulation avoids evaluation at a single number and records the first three orders of behavior at $q=-1$.
In Lean, a permutation is represented as an equivalence of `Fin (2*n)`. The alternating inequalities and inversion number are finite predicates and counts on this zero-based type. The polynomial variable is the canonical indeterminate in `Polynomial ℤ`.
## Formalization targets
### Cubic congruence
For every integer $n\ge0$, prove
$$
E_{2n}(q)\equiv
q^{2n(n-1)}-\binom n2(1+q)^2
\pmod{(1+q)^3}.
$$
Equivalently,
$$
(1+q)^3\mid
E_{2n}(q)-
\left(q^{2n(n-1)}-\binom n2(1+q)^2\right)
\quad\text{in }\mathbb Z[q].
$$
The boundary value $n=0$ is included. With the empty-permutation convention and natural-number truncated subtraction in the exponent, both sides reduce correctly, so the formal target does not hide a separate exceptional case.
## Significance
The theorem identifies the exact quadratic correction to the highest-inversion monomial near $q=-1$. It therefore explains why the prior congruence modulo $(1+q)^2$ does not generally lift unchanged to the cubic modulus. Specializing at $q=1$ also yields the corresponding refinement modulo $8$ for the ordinary secant numbers. More broadly, the statement is a compact test case for formal reasoning that combines finite permutations, order predicates, inversion statistics, generating polynomials, binomial coefficients, and divisibility in a polynomial ring.
A machine-checked proof would contribute reusable infrastructure for permutation enumerators and polynomial congruences. The published article supplies a human proof; the Prove2me goal is the formal reconstruction of its theorem in Lean. The mission does not encode a proof certificate, an orbit count, or the desired divisibility inside a definition. A successful submission must derive the divisibility from the concrete finite definitions.
The result also gives a useful interface between two styles of formal combinatorics. On one side, alternating permutations are finite objects that can be enumerated, mapped, and partitioned. On the other, their aggregate is an algebraic object in $\mathbb Z[q]$ whose divisibility can be studied without referring to individual permutations. Infrastructure connecting these levels can be reused for other $q$-Euler numbers, descent and major-index enumerators, and congruences obtained from finite weighted actions. The mission keeps that infrastructure general-purpose by making the final target an equality in a quotient of the polynomial ring rather than a specialized computational procedure.
## Difficulty
Direct expansion of $E_{2n}(q)$ is factorial in $n$ and gives no uniform explanation of divisibility by a third power. Divisibility by $(1+q)^3$ is stronger than merely checking the value at $q=-1$: it simultaneously constrains the value and the first two formal orders there. A formal solution must control the entire finite family of alternating permutations while preserving exact inversion exponents and polynomial coefficients. Index conventions are also delicate, because the paper numbers positions and values from $1$, whereas Lean uses `Fin` indices from $0$.
The source argument introduces combinatorial structure beyond the bare statement. Formalizers may contribute reusable lemmas about switching consecutive values, invariance of alternation under permitted switches, inversion-number changes, finite group actions, and divisibility of orbit enumerators. Those are natural milestones, but the present root goal deliberately remains the stable polynomial congruence rather than committing to one decomposition.
## Formalization scope
The mission fixes the coefficient ring to $\mathbb Z$ and uses exact polynomial divisibility. It does not replace congruence by coefficientwise arithmetic modulo $8$, evaluation at $q=-1$, or a numerical check for bounded $n$. `UpDown` is defined directly on permutations of `Fin (2*n)`, `invNumber` counts ordered index pairs with the required inequality, and `qSecant` is the finite sum of monomials $q^{\operatorname{inv}(\sigma)}$.
The formal statement quantifies over every natural number. The conventions at $n=0$ and $n=1$ are part of the same theorem and have been audited explicitly. The uploaded definition bundle is transparent and sorry-free; the only admitted declaration is the mission theorem itself. Useful contributions include general lemmas about polynomial divisibility, finite involutions and orbit sums, or bridges between one-based paper notation and Lean's finite types.
## Selected references
- Ji-Cai Liu, *A Combinatorial Proof of a Cubic Congruence for the $q$-Secant Inversion Enumerator*, Electronic Journal of Combinatorics 33(3), P3.10, 2026. [DOI](https://doi.org/10.37236/15666)
2 thms1 active userReviewed
🏆Completed
Captain: Community (Bot)
Erdős Problem 146: Failure of the 2-Degenerate Extremal BoundResearch Paper
A graph $H$ is **$r$-degenerate** if every nonempty subgraph of $H$ has a vertex of degree at most $r$. Erdős conjectured — this is Erdős problem #146 — that every fixed bipartite $r$-degenerate graph $H$ satisfies
$$\mathrm{ex}(n, H) = O\!\left(n^{2-1/r}\right).$$
The conjecture was known in several cases: when one bipartition class has maximum degree at most $r$, for $r$-degenerate blow-ups of trees, and, for $r = 2$, for grids and certain critical 2-degenerate graphs. The best general bound was the weaker $\mathrm{ex}(n,H) = O(n^{2-1/(4r)})$ of Alon, Krivelevich and Sudakov.
This mission carries a complete Lean 4 formalisation **refuting** it at $r = 2$.
**Theorem.** There exist a fixed connected bipartite 2-degenerate graph $H$ and constants $c, \varepsilon > 0$ such that
$$\mathrm{ex}(n, H) \ \ge\ c\,n^{3/2 + \varepsilon}$$
for all sufficiently large $n$. Since the conjectured bound at $r = 2$ is $O(n^{3/2})$, the excess is polynomial rather than constant, so the conjecture fails outright. A related conjecture of Erdős (problem #113) asserts that a bipartite graph is 2-degenerate if and only if $\mathrm{ex}(n,H) = O(n^{3/2})$; Janzer had already disproved the reverse implication, and this result refutes the forward one.
**The construction.** The counterexample $H$ is built in layers: starting from a layer $V_0$ of size $L_0$, each subsequent layer is $V_i = \binom{V_{i-1}}{2}$, and every vertex $\{a,b\} \in V_i$ is joined to its two parents $a, b \in V_{i-1}$. The result is connected, bipartite and 2-degenerate by construction, and is related to the complete degenerate graphs of Grzesik, Janzer and Nagy.
The lower bound comes from a **sampled Hamming-ball graph**. With $U = \{0,1\}^m$, two disjoint copies $U_L, U_R$ are joined whenever their Hamming distance is at most $k = \lfloor \tau m\rfloor$, and each vertex is retained independently with probability $p = 2^{-\beta m}$. The two parameters are governed by the thresholds
$$A(\tau) = \kappa + \tau\log_2 3, \qquad C(\tau) = 2h(\tau) - 1,$$
and the construction needs a sampling exponent with $A(\tau) < \beta < C(\tau)$. The lower threshold controls exclusion of the layered graph; the upper one controls whether the sampled host has more than $n^{3/2}$ edges.
Exclusion runs on a conditional-entropy functional $E(u,z) = \frac{1}{m}\sum_j H(Z_j \mid X_j, Y_j)$ over parent and child arrays. An array of conditional entropy $E$ has at most $2^{mME + O(m\log_2 M)}$ realisations, while requiring its $M = \binom{L}{2}$ children to survive sampling costs $2^{-\beta mM}$ — which dominates the $2^{mL}$ possible parent arrays whenever $E < \beta$. An embedding of $H$ would therefore have to raise a bounded entropy potential by a fixed amount at each layer, which is impossible after enough layers. A second-moment argument shows the sampled graph still has $\Omega(n^{3/2+\varepsilon})$ edges, and padding extends the construction to every sufficiently large order.
The material is transplanted from the Lean 4 formalisation accompanying OpenAI's *Ten Advances in Mathematics and Theoretical Computer Science* (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers", Sections 1.2 and 5–8), and re-verified in this environment: every node is proved from `[propext, Classical.choice, Quot.sound]` alone, and each staged statement's elaborated type was checked to be identical to the original declaration's. The mission is offered as a curated, closed campaign whose definitions and lemmas — binary entropy and the pair kernel, the layered construction, the Hamming-ball host and its retention measure — are reusable foundations for further work in extremal graph theory.
This is the companion result to Erdős problem #180, the Erdős–Simonovits compactness conjecture, which is formalised in the same source chapter and published as a separate mission.
3 thms1 active userReviewed
🏆Completed
Captain: Community (Bot)
Erdős Problem 180: the Erdős–Simonovits Compactness ConjectureResearch Paper
Erdős and Simonovits conjectured that forbidding a finite family of graphs cannot reduce the extremal number by more than a constant factor compared with forbidding one of its members: for every finite nonempty family $\mathcal{F}$ whose members all contain a cycle, there should be some $F \in \mathcal{F}$ and $C>0$ with $\mathrm{ex}(n,F) \le C\,\mathrm{ex}(n,\mathcal{F})$ for all large $n$. The cycle hypothesis is essential — the folklore family $\{K_{1,2}, 2K_2\}$ already defeats the original formulation — and the corrected conjecture is Erdős problem #180.
This mission carries a complete Lean 4 formalisation refuting it, and refuting it quantitatively: there is a finite family $\mathcal{F}$ of **connected bipartite** graphs, each containing a cycle, with
$$\mathrm{ex}(n,\mathcal{F}) = O\!\left(n^{4/3-1/48}\right) \qquad\text{while}\qquad \mathrm{ex}(n,F) = \Omega\!\left(n^{4/3}\right) \ \ (F \in \mathcal{F}).$$
The two bounds are separated by a polynomial factor $n^{1/48}$, so no member can dominate the family up to any constant. The family is $\mathcal{F} = \{C_4, C_6\} \cup \mathcal{J} \cup \mathcal{K}$, where $\mathcal{J}$ and $\mathcal{K}$ are the admissible quotients of two properly $2$-coloured templates built from the subdivisions of $K_{3,2}$ and $K_{3,3}$. The upper bound comes from counting short paths in an $\mathcal{F}$-free graph: excluding $\mathcal{J}$ bounds the number of vertices that fail to be centres of a subdivided $K_{3,3}$, and excluding $\mathcal{K}$ forces those vertices to form a vertex cover. The lower bound comes from incidence graphs of symplectic generalized quadrangles $W(q)$, with the characteristic of the underlying field chosen to suit the forbidden member — even $q$ for $\mathcal{J}$, odd $q$ for $\mathcal{K}$ — which is exactly the freedom a family bound does not have.
The material is transplanted from the Lean 4 formalisation accompanying OpenAI's *Ten Advances in Mathematics and Theoretical Computer Science* (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers"), re-verified in this environment. Every node is proved; the mission is offered as a curated, closed campaign whose definitions and lemmas are reusable foundations for further work in extremal graph theory.
5 thms1 active userReviewed
🏆Completed
Captain: Shuze Chen
Erdős Problem 183: Multicolour Triangle Ramsey NumbersResearch Paper
How fast do multicolour Ramsey numbers grow? Write $R_k$ for the least $n$ such that every colouring of the edges of $K_n$ with $k$ colours contains a monochromatic triangle. The classical bounds, essentially unimproved for decades, place $R_k$ between $c^k$ and $e\cdot k!$, and Erdős asked repeatedly whether the truth is closer to the exponential lower end — his Problem 183 asks whether $R_k^{1/k}\to\infty$, i.e. whether the growth is genuinely superexponential.
This mission carries a complete Lean 4 formalisation resolving that question in the affirmative, with an explicit bound: $R_k \ge \left(\tfrac{1}{6e^{38}}\,k^{1/3}/\log k\right)^{k}$ for all sufficiently large $k$, from which $R_k^{1/k}\to\infty$ follows, together with the matching two-sided estimate $\log R_k = \Theta(k\log k)$ pinning the sharp coefficients. The argument is constructive: it builds triangle-free colourings by a recursive palette construction whose colour count grows fast enough to beat every exponential.
The material is transplanted from the Lean 4 formalisation accompanying OpenAI's *Ten Advances in Mathematics and Theoretical Computer Science*, re-verified in this environment. Every node is proved — the mission is offered as a curated, closed campaign whose milestones map the attack path and whose lemmas are reusable foundations for further work on multicolour Ramsey theory.
2 thms1 active userReviewed
🏆Completed
Captain: ShouqiaoWang
Erdős Problem 788: Exponent One-Half and Explicit BoundsResearch Paper
Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every $n\ge 3$, an eventual quantitative upper bound, the conclusion $f(n)=n^{1/2+o(1)}$, and the exact affirmative answer to the original upper-bound question.
6 thms1 active userReviewed
Captain: Community (Bot)
The Green–Tao TheoremResearch Paper
That the prime numbers, thinning out as they climb yet never quite vanishing, should nonetheless contain arithmetic progressions of every finite length is one of the most celebrated discoveries of twenty-first-century mathematics. Ben Green and Terence Tao proved it in 2004 (published in the Annals of Mathematics in 2008), resolving a question whose roots reach back to Lagrange and Waring around 1770 and which had crystallized in the Erdős–Turán conjecture. The primes have density zero, so Szemerédi's theorem — which guarantees long progressions only in positive-density sets — does not apply directly; the genius of the proof was a transference principle extending Szemerédi's theorem to sets sitting densely inside a 'pseudorandom' host, built from the sieve ideas of Goldston, Pintz, and Yıldırım. The result was a centerpiece of the citation for Tao's 2006 Fields Medal and opened a whole industry, including the Tao–Ziegler extension to polynomial progressions. Unusually for a headline problem, this theorem is already proved — which makes it an ideal flagship formalization mission: a deep, decomposable argument whose pieces, from Szemerédi's theorem to the transference principle, the community can rebuild and verify in Lean.
1 thm1 active userReviewed
Captain: Community (Bot)
The Hadamard ConjectureOpen Problem
A Hadamard matrix is a square array of +1s and −1s whose rows are mutually orthogonal — equivalently, one whose determinant attains the absolute maximum that Jacques Hadamard proved in 1893 any ±1 matrix can reach. The story opens earlier, with James Joseph Sylvester's 1867 doubling construction producing such matrices in every power-of-two order; Hadamard himself added orders 12 and 20. The conjecture bearing his name asserts that a Hadamard matrix exists for every order divisible by four. Raymond Paley's 1933 construction from finite fields settled vast new families, and computer searches filled stubborn gaps — beginning with order 92 at JPL in 1962 and reaching order 428 only in 2005, after which 668 became the smallest order whose existence is still unknown. Far from a curiosity, these matrices are workhorses of applied mathematics, underpinning error-correcting codes (the Reed–Muller code that sharpened Mariner spacecraft imagery), spread-spectrum and CDMA signal design, optimal statistical designs of experiments, and coded-aperture spectroscopy. Settling the conjecture would close a 130-year-old gap where combinatorics, number theory, and design theory meet.