All missions

Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the even case: for squarefree even n, the representation-count identity 2|C_n| = |D_n| — where C_n and D_n count integer solutions of n = 8x² + 2y² + 64z² and n = 8x² + 2y² + 16z² — implies that n is a congruent number.

Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the odd case: for squarefree odd n, the representation-count identity 2|A_n| = |B_n| — where A_n and B_n count integer solutions of n = 2x² + y² + 32z² and n = 2x² + y² + 8z² — implies that n is a congruent number.

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.

In a 1999 Vienna doctoral thesis, Gerhard Zauner conjectured that in every finite dimension d one can find d² unit vectors in complex d-space that are mutually as spread out as possible — any two sharing the same squared overlap 1/(d+1). Such a configuration, a symmetric informationally complete positive operator-valued measure (SIC-POVM), is the optimal minimal measurement for reconstructing an unknown quantum state, which is why the idea was rediscovered and named by Renes, Blume-Kohout, Scott, and Caves in 2004 and became central to quantum tomography, quantum cryptography, and the QBist reading of quantum mechanics. Geometrically these are maximal sets of complex equiangular lines; physically they are the most efficient quantum measurements; and, remarkably, they appear to be governed by deep number theory — recent work by Appleby, Flammia, Kopp, and others ties exact SICs to Stark units and Hilbert's twelfth problem on explicit class field theory. Exact solutions have been hand-built in scores of dimensions and numerical ones found in every dimension checked, yet a general existence proof remains out of reach. Formalizing Zauner's conjecture gives this problem — straddling quantum information, geometry, and algebraic number theory — a precise shared target.

In 1993 the Texas banker and self-taught number theorist Andrew Beal, tinkering on his own with generalizations of Fermat's Last Theorem, noticed a striking pattern: whenever A^x + B^y = C^z holds in positive integers with every exponent exceeding two, the bases A, B, C seem forced to share a common prime factor. Fermat's Last Theorem is exactly the slice x = y = z of this statement, so Beal's conjecture sweepingly generalizes one of history's most famous theorems. Beal backed his question with money, raising the prize from $5,000 in 1997 to$1,000,000, now held in trust by the American Mathematical Society. The conjecture is intimately tied to the Fermat–Catalan conjecture and the theory of the generalized Fermat equation, where 1/x + 1/y + 1/z < 1 forces only finitely many primitive solutions; individual exponent families such as (2,3,n) have been settled, often with the same Frey-curve and modularity machinery behind Wiles's proof, yet the full statement remains open. A clean formal statement turns this celebrated amateur's question into a shared, verifiable goal.

Prove that every Dirichlet L-function is nonzero in the strict half-plane $\operatorname{Re}(s)>0.8749570698$, excluding the principal-character pole at $s=1$.

The boundary is exactly $4374785349/5000000000$. It must hold uniformly for every positive modulus, every complex Dirichlet character, and every height. This strengthens the $7/8$ baseline in Towards the Generalized Riemann Hypothesis.

The source is LW56e2's quasi-Riemann refinement, specifically RH.Transport.dirichlet_nonvanishing. It builds on OpenAI's original quasi-Riemann development. Original authorship and upstream notices are retained under the repository's Apache-2.0 license.

The upstream proof is being checked and prepared for import into the campaign's Lean environment. This mission remains Open until its complete proof has been accepted here. The source also contains Hecke and zeta results; the mission goal is the uniform all-Dirichlet statement.

Motivation

An open book decomposition of a contact $3$-manifold whose pages are transverse to the Reeb flow turns questions on the three-dimensional flow into questions on a surface map. Hofer, Wysocki and Zehnder produced such decompositions of $S^3$ with disk-like pages for dynamically convex Reeb flows (Ann. of Math. 148, 1998), with pages that are projections of embedded fast finite-energy planes. Hryniewicz isolated exactly what is required (U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Theorem 2.5, arXiv:0812.4076): one embedded fast plane asymptotic to an orbit $P$ of Conley–Zehnder index at least $3$, together with compactness of the sets $\Lambda(K,P)$ of normalized embedded fast planes, gives a whole $S^1$-family of such planes whose projections foliate the complement of $P$, every page being a global surface of section.

This mission formalizes that theorem for the symplectization of a strictly star-shaped hypersurface $S\subset\mathbb{R}^4$. It is the twelfth mission in a series on symplectic field theory, and builds on the published definitions and results of the previous missions: finite-energy curves and their punctures, the winding numbers, the sets $\Theta(K,P)$ and $\Lambda(K,P)$ with their compactness, and the families of embedded fast planes through a given one.

Setting

All objects are those of FiniteEnergyPlane_Setting, FiniteEnergyPlane_Asymptotics, FiniteEnergyPlane_Winding, FiniteEnergyPlane_Compactness and FiniteEnergyPlane_Fredholm with $n=1$: a strictly star-shaped level $S=H^{-1}(1)\subset\mathbb{R}^4$ with Reeb field $R$ and contact planes $\xi$, a compatible complex structure $J$ on $\xi$, and finite-energy $\tilde J$-holomorphic curves in $\mathbb{R}\times S\cong\mathbb{R}^4\setminus\{0\}$, $y=e^{2a}x$.

• Reeb trajectories. Maps $y:\mathbb{R}\to S$ with $y'=R(y)$. No flow map appears in the statements.
• Families of planes. A family is a map $U:\mathbb{R}\times\mathbb{C}\to\mathbb{R}^4$, with $S$-component $\mathrm{pageMap}\,H\,U=\mathrm{proj}\circ U$. A family along $y$ has $U(t,\cdot)\in\Lambda(\{y(t)\},P)$ for all $t$, which is Hryniewicz's $\Lambda_t$ of (101).
• Open books of planes. IsPlaneOpenBook says that $U$ is $C^l$ and $1$-periodic in the first variable, that its slices are embedded fast planes asymptotic to $P$, and that $\mathrm{pageMap}\,H\,U$ maps $[0,1)\times\mathbb{C}$ bijectively onto $S\setminus x(\mathbb{R})$, with injective derivative, positively against the Reeb field.

Formalization targets

Goal: open books from a fast plane (Hryniewicz 2012, Theorem 2.5)

Let $P$ be a periodic Reeb orbit with $\mu_{CZ}(P)\ge3$ such that every orbit of period at most $T_P$ is nondegenerate, let $\gamma>0$ be below these periods and their nonzero differences, and suppose $\Lambda(K,P)$ is sequentially compact in $C^\infty_{loc}$ for every compact $K\subset\mathbb{R}^4\setminus\{0\}$ off the cylinder over $P$. If there is an embedded fast plane asymptotic to $P$, then for every $l\ge1$ there is a $C^l$ map $U$ with IsPlaneOpenBook, and every Reeb trajectory off $x(\mathbb{R})$ meets every leaf at arbitrarily large and arbitrarily negative times.

Milestones

1. Uniqueness of normalized planes (Lemma 7.1). Two planes in $\Lambda(\{y_0\},P)$ differ by a rotation of the domain.
2. Local families (Lemmas 7.2, 7.3). A plane in $\Lambda(\{y(t_0)\},P)$ belongs to a local $C^l$ family of planes in $\Lambda(\{y(t)\},P)$ whose $S$-components form an embedding, and which contains the nearby embedded fast planes up to translation and affine reparametrization.
3. Comparing families (Lemma 7.4). Two $C^l$ families of normalized planes along the same trajectory differ on their common interval by a $C^l$ rotation of the domain.
4. Continuation along a trajectory (Lemma 7.8). Under the compactness hypothesis, a plane in $\Lambda(\{y(0)\},P)$ extends to a $C^l$ family along $y$ over $(-\delta,\tau)$, for every $\tau>0$.
5. Trajectories near the orbit (Lemma 6.9). A Reeb trajectory whose $\omega$-limit (or $\alpha$-limit) set meets $x(\mathbb{R})$ meets the projection of every fast plane asymptotic to $P$ at arbitrarily large (or arbitrarily negative) times.
6. Returns to a leaf (§ 7.2.1). Under the compactness hypothesis, some Reeb trajectory leaves a plane in $\Lambda(\{y(0)\},P)$ and meets its projection again at a positive time.
7. Foliation over an interval (Lemma 7.7). A return of the trajectory to the leaf yields a $C^l$ family over an interval $(-\delta,L+\delta)$ whose leaves foliate the complement in $S$ of $x(\mathbb{R})$ and of the leaf at $t=0$.
8. Periodic family (§ 7.2.2). A foliation over an interval gives a $C^l$ map, $1$-periodic in the first variable, whose slices are embedded fast planes and whose $S$-component parametrizes $S\setminus x(\mathbb{R})$.
9. Global surfaces of section (§ 7.2.3). Every Reeb trajectory off $x(\mathbb{R})$ meets every leaf at arbitrarily large and arbitrarily negative times.

Significance

The results. Theorem 2.5 of Hryniewicz 2012 is the passage from single fast planes to global dynamics: together with the existence of one embedded fast plane and the compactness of $\Lambda(K,P)$, it gives the disk-like global surfaces of section of Hofer–Wysocki–Zehnder and the characterization of their binding orbits by Hryniewicz, since the Poincaré return map to a page is then an area-preserving map of an open disk. The theorem also holds for orbits of Conley–Zehnder index above $3$ and for hypotheses on compactness alone, which is the form in which it applies outside the dynamically convex case (Hryniewicz–Salomão 2011).

Formalizing them. All results are classical and proved in the cited sources. None of them has been formalized in Lean or another interactive theorem prover, as far as a literature search shows; Mathlib has no pseudoholomorphic curves and no global surfaces of section.

Difficulty

The hypotheses concern one plane and the compactness of sets of planes, while the conclusion is a statement about all of the closed $3$-manifold $S$: the map $U$ must be periodic, must parametrize $S\setminus x(\mathbb{R})$ bijectively with injective derivative, and must have the regularity asserted for every $l$. The last clause concerns every trajectory on $S$.

Formalization scope

• Namespace FiniteEnergyPlane; the definition module FiniteEnergyPlane_OpenBook imports FiniteEnergyPlane_Fredholm (previous mission).
• Dimension three ($n=1$, $S\subset\mathbb{R}^4$) throughout. IsReebTrajectory and pageMap are defined for general $n$.
• A single level. The goal has the form of the goals of the previous missions, for one strictly star-shaped level in the coordinates of HryniewiczCriterion.
• Hypotheses as in the source. The embedded fast plane and the compactness of $\Lambda(K,P)$ are hypotheses of the goal. Nondegeneracy is required only for orbits of period at most $T_P$, where the source assumes it for all contractible orbits.
• Regularity. The map $U$ is $C^l$ for each $l$, as in the source; its pages are compared on the open disk $\mathbb{C}$, and no statement is made about the closure of a page at $x(\mathbb{R})$.
• The index is that of the orbit. Conditions in the source comparing indices of planes over the same orbit hold automatically on a star-shaped level, where $\xi$ has a global frame, and are not restated.
• Not included. The Bishop family (Hryniewicz 2012, Theorem 2.4), which gives the existence of an embedded fast plane, is left to a later mission.

Contributions welcome: general lemmas on Reeb trajectories on a star-shaped level and on $C^l$ families of planes.

Selected references

• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931, §§ 2, 6 and 7. https://arxiv.org/abs/0812.4076
• H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289.
• U. Hryniewicz, P. Salomão, On the existence of disk-like global sections for Reeb flows on the tight 3-sphere, Duke Math. J. 160 (2011), 415–465. https://doi.org/10.1215/00127094-1444278
• U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014). https://arxiv.org/abs/1105.2077

Motivation

Fast finite-energy planes are the pseudoholomorphic planes in the symplectization of a contact $3$-manifold whose asymptotic winding is as small as possible; their projections are immersions transverse to the Reeb flow. The pages of the open book decompositions that give disk-like global surfaces of section for dynamically convex Reeb flows on $S^3$ are projections of such planes (H. Hofer, K. Wysocki, E. Zehnder, Ann. of Math. 148, 1998). Compactness of sets of fast planes was the subject of the previous mission. This mission formalizes the second analytic theorem about them: an embedded fast plane is a member of a two-parameter family of embedded fast planes, it does not meet the cylinder over its asymptotic orbit, and it projects to a proper embedding into the complement of that orbit (U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Theorem 2.3, arXiv:0812.4076). This statement extends Theorem 1.5 of H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectizations III: Fredholm theory (1999), from Conley–Zehnder index $3$ and nondegenerate orbits to index at least $3$ and possibly degenerate orbits.

The mission follows Hryniewicz 2012, §§ 2, 4.7 and 6, for the symplectization of a strictly star-shaped hypersurface $S\subset\mathbb{R}^4$. It is the eleventh mission in a series on symplectic field theory, and builds on the published definitions and results of the previous missions: finite-energy curves and their punctures, the winding numbers $\mathrm{wind}_\pi$, $\mathrm{wind}_\infty$, and the sets $\Theta(K,P)$ with their compactness.

Setting

All objects are those of FiniteEnergyPlane_Setting, FiniteEnergyPlane_Asymptotics, FiniteEnergyPlane_Winding and FiniteEnergyPlane_Compactness with $n=1$: a strictly star-shaped level $S=H^{-1}(1)\subset\mathbb{R}^4$ with Reeb field $R$ and contact planes $\xi$, a compatible complex structure $J$ on $\xi$, and finite-energy $\tilde J$-holomorphic curves in $\mathbb{R}\times S\cong\mathbb{R}^4\setminus\{0\}$, $y=e^{2a}x$.

• Embedded planes. A plane $u:\mathbb{C}\to\mathbb{R}^4$ is embedded if it is an injective immersion. For finite-energy planes with a nondegenerate puncture at $\infty$, which are proper maps, this is the usual notion.
• Translations. $c\cdot u$ is $z\mapsto e^{2c}u(z)$; it adds $c$ to the $\mathbb{R}$-coordinate and leaves the $S$-component unchanged.
• The set $\Lambda(K,P)$ (Hryniewicz (8)) consists of the embedded planes in $\Theta(K,P)$.
• Conley–Zehnder index. $\mu_{CZ}(P)\ge3$ is P.IsCZAtLeast 3 of the previous mission, measured in the global frame of $\xi$ on the star-shaped level. The orbit $P$ may be degenerate.

Formalization targets

Goal: Fredholm theory of embedded fast planes (Hryniewicz 2012, Theorem 2.3)

Let $u$ be an embedded fast finite-energy plane asymptotic to $P=(x,T)$ at $\infty$ with $\mu_{CZ}(P)\ge3$. Then $\mathrm{proj}\circ u$ does not meet $x(\mathbb{R})$ and is a proper embedding of $\mathbb{C}$ into $S\setminus x(\mathbb{R})$. For every $l\ge1$ there are $r>0$ and a $C^l$ embedding $f:\mathbb{C}\times B_r(0)\to\mathbb{R}^4$ with $f(\cdot,0)=u$, such that every $f(\cdot,\tau)$ is an embedded fast plane asymptotic to $P$, and every sequence of such planes converging in $C^\infty_{loc}$ to some $f(\cdot,\tau_0)$ is eventually of the form $u_k(z)=f(A_kz+B_k,\tau_k)$ with $\tau_k\to\tau_0$, $A_k\to1$, $B_k\to0$.

Milestones

1. Persistence of intersections (McDuff 1991, Theorem 1.1, immersed case). An isolated intersection of two finite-energy pseudoholomorphic immersions persists, near the same point, for curves $C^\infty_{loc}$-close to them.
2. Non-isolated intersections (McDuff 1991, Lemma 2.7, immersed case). Near a non-isolated intersection point, one finite-energy pseudoholomorphic immersion is a holomorphic reparametrization of the other.
3. Families of fast planes (Hryniewicz 2012, Lemmas 6.10 and 6.20). An embedded fast plane asymptotic to an orbit with $\mu_{CZ}\ge3$ lies in a $C^l$ two-parameter family of embedded fast planes asymptotic to the same orbit, which contains its small translations up to image.
4. Proper embedding (Lemma 6.22). The $S$-component of a fast plane that does not meet its asymptotic orbit is a proper embedding into the complement of the orbit.
5. Equal or disjoint images (Lemma 6.23). Two embedded fast planes asymptotic to the same orbit and not meeting it have equal or disjoint images in $S$.
6. Missing the orbit (Lemma 6.24). An embedded fast plane asymptotic to an orbit with $\mu_{CZ}\ge3$ does not meet the cylinder over that orbit.
7. Equal images (Lemma 6.25). Two embedded fast planes asymptotic to the same orbit with $\mu_{CZ}\ge3$ and with the same image in $S$ agree up to an affine reparametrization and a translation.
8. Embedded limits (§ 4.7). A fast plane that is a $C^\infty_{loc}$ limit of embedded fast planes is embedded.
9. Compactness of $\Lambda$ (Theorem 2.2 (2)). Under the orbit hypotheses of the previous mission's goal, the set $\Lambda(K,P)$ is sequentially compact in $C^\infty_{loc}$.

Significance

The results. Theorem 2.3 of Hryniewicz 2012, together with the compactness of $\Lambda(K,P)$, is what produces a whole $S^1$-family of pages of an open book decomposition from a single embedded fast plane (Hryniewicz 2012, Theorem 2.5). In that setting it holds for possibly degenerate binding orbits, which is what makes it applicable to arbitrary contact forms on $S^3$, and this is the case that occurs for the characterization of the binding orbits of disk-like global surfaces of section (Hryniewicz 2014). Milestones 1 and 2 are the immersed case of the local description of intersections of pseudoholomorphic curves in dimension four, a basic tool of the subject, and are stated for general finite-energy curves.

Formalizing them. All results are classical and proved in the cited sources. Lemma 6.20 of Hryniewicz 2012 is sketched there. None of these results has been formalized in Lean or another interactive theorem prover, as far as a literature search shows; Mathlib has no pseudoholomorphic curves.

Difficulty

The goal combines the analysis of a nonlinear elliptic equation along a noncompact curve with global geometric information: the family must consist of planes of the same kind, with the same asymptotic orbit, and every nearby embedded fast plane must already belong to it. The hypothesis allows Conley–Zehnder index above $3$ and degenerate orbits, which goes beyond the setting of Hofer–Wysocki–Zehnder 1999. The intersection statements are local but have to be established for pseudoholomorphic curves, not holomorphic ones, in a four-dimensional target.

Formalization scope

• Namespace FiniteEnergyPlane; the definition module FiniteEnergyPlane_Fredholm imports FiniteEnergyPlane_Compactness (previous mission).
• Dimension three ($n=1$, $S\subset\mathbb{R}^4$) throughout. IsEmbeddedPlane and the translation are defined for general $n$.
• A single level. The goal has the form of the goal of the previous mission, for one strictly star-shaped level in the coordinates of HryniewiczCriterion.
• The index is that of the orbit. Conditions in the source that compare indices or classes of trivializations of two planes over the same orbit hold automatically on a star-shaped level, where $\xi$ has a global frame, and are not restated. The Formalization Notes of the items say where.
• The parameter space of the family is the open ball $B_r(0)\subset\mathbb{C}$, standing for Hryniewicz's $B_r(0)\subset\mathbb{R}^2$.
• Not included. The open book decomposition (Hryniewicz 2012, Theorem 2.5) and the Bishop family (Theorem 2.4) are left to later missions.

Contributions welcome: general lemmas on pseudoholomorphic immersions and on $C^\infty_{loc}$ convergence of finite-energy curves.

Selected references

• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931, §§ 2, 4.7 and 6. https://arxiv.org/abs/0812.4076
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectizations III: Fredholm theory, in Topics in Nonlinear Analysis, Birkhäuser 1999, 381–475. https://doi.org/10.1007/978-3-0348-8765-6_18
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations II: Embedding controls and algebraic invariants, Geom. Funct. Anal. 5 (1995), 270–328. https://doi.org/10.1007/BF01895669
• D. McDuff, The local behaviour of holomorphic curves in almost complex 4-manifolds, J. Differential Geom. 34 (1991), 143–164. https://doi.org/10.4310/jdg/1214446994
• U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014). https://arxiv.org/abs/1105.2077
• H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289.

Motivation

Many manufacturers buy transport or production capacity under contracts with volume flexibility: in every period a base capacity $k_n$ can be sourced at the contracted unit price $c$, and any volume above it is still available but costs an extra flexibility premium $c_p$ per unit. The sourcing cost per period is therefore piecewise linear and convex, with slopes $c$ and $c + c_p$. When demand peaks exceed base capacity, a firm can either pay the premium or order earlier, using slack base capacity in earlier periods and carrying the inventory forward.

For the stochastic version of this problem, the optimal policy is known to have a two-level base-stock structure (Porteus, 1990). Its period-dependent parameters, however, have no closed form. Gijsbrechts, Imdahl, Boute and Van Mieghem (POM 2023) instead study a robust rolling-horizon formulation. In each period a linear program is solved over a planning horizon of $H$ periods, against worst-case cumulative demands over an uncertainty set, in the tradition of Bertsimas and Thiele (2006) and Mamani, Nassiri and Wagner (2017). Only the first-period order is implemented. Their Theorem 1 states that the solution of this linear program is a simple, explicit generalized base-stock rule, the Lookahead Peak-Shaving (LPS) policy.

Timeline:

• Porteus (1990) characterizes the optimal stochastic policy for piecewise-linear convex ordering costs.
• Bertsimas and Thiele (2006) introduce robust optimization for inventory control.
• Mamani et al. (2017) give closed-form robust base-stock levels for linear sourcing costs under CLT-type uncertainty sets.
• Gijsbrechts et al. (2023) extend this to volume flexibility, which is the paper this mission formalizes.

Setting

Fix one decision period $t$ and index the planning horizon by $n \in \{0,\dots,H-1\}$, where $n = 0$ is the current period $t$. The data are:

• holding cost $h$, backorder penalty $b$, contracted unit cost $c$ and premium $c_p$;
• the starting net inventory $x = x_{t-1}$, which may be negative (backlog);
• base capacities $k_n$;
• an uncertainty set $\Omega \subseteq \mathbb{R}^H$ of demand vectors.

The worst-case cumulative demands are

The robust problem is the linear program (4) over orders $q$, mismatch costs $y$ and premium costs $z$:

subject to, for every $n$:

• $y_n \ge h(x+\sum_{i\le n} q_i-\underline D_n)$;
• $y_n \ge -b(x+\sum_{i\le n} q_i-\overline D_n)$;
• $z_n \ge c_p(q_n-k_n)$;
• $z_n, q_n \ge 0$.

Removing the premium constraints gives the uncapacitated system. Its cumulative base stock is

Its orders $\hat q_n$ (eq. (6)) raise the cumulative order to $\hat S_n - x$, except in the final periods in which a unit costs more to buy than to backlog until the end of the horizon.

The shifting need over a lookahead of $s$ periods (Definition 1) is

The LPS order (Definition 2, eq. (11)) is the generalized base-stock order with lower level $\hat S_0$ and upper level $\hat S_0+\tau^s$:

Formalization targets

Goal: Theorem 1 (optimality of the Lookahead Peak-Shaving policy)

Assume the following:

• $h>0$, $c\ge 0$ and $k_n\ge 0$;
• $\Omega$ is nonempty and bounded, and contains only nonnegative demand vectors;
• Assumption 1: $h<c_p<b$;
• Assumption 2: $\lfloor c_p/h\rfloor<H$ and $\lfloor c/b\rfloor<H$;
• the no-end-effect condition $c+c_p\le b\,(H-s)$ with $s=\lfloor c_p/h\rfloor$.

Then the LP (4) has an optimal solution whose first-period order is the LPS order with lookahead $s$:

The statement is existential ("the policy is robustly optimal"). It does not claim that every optimal solution orders $q^{\mathrm{LPS}}$ in the current period, because ties can make the optimum non-unique.

Significance

Theorem 1 reduces a horizon-long linear program to an explicit two-threshold rule. That gives closed-form policy parameters ($\hat S_t$ and $\tau^s_t$, made fully explicit for the symmetric CLT uncertainty set in the paper's Theorem 2). It also gives the sensitivity results of Section 5 and an implementable policy that matches the structure of the stochastic optimum. A machine-checked proof fixes the exact conditions under which this reduction is valid, as the next paragraph shows.

On the extra hypothesis. With only Assumptions 1–2, the statement is false near the end of the planning horizon. Take $H=2$, $h=1$, $c_p=1.5$, $b=2$, $c=3$, $x=0$, $k=(1,1)$ and deterministic demand $(10,10)$. LPS orders 10 units, and the best plan that starts this way costs $63.5$. The LP optimum instead orders 1 unit and costs $59$: paying $c+c_p$ for a unit is worse than backlogging it for the two remaining periods. The added condition $c+c_p\le b\,(H-s)$ keeps such end-of-horizon effects out of the lookahead window. On randomly generated instances satisfying it, LPS matched the LP optimum in every case. Whether a weaker condition suffices is open and of independent interest. The paper's proof (Appendix A of its Supporting Information) has not been formalized anywhere.

Difficulty

The paper argues by repeatedly applying Lemma 1, a pairwise exchange that advances $\omega$ units from a capacity-tight period $n$ to a slack period $j$ at extra holding cost $h\omega(n-j)$ and a saving of $c_p\omega$, together with the convexity of the LP. Turning this into a proof needs a global optimality certificate. Local improvement arguments do not by themselves show that no combination of advances, postponements and changes in total ordered volume beats the LPS order. A natural route is an explicit optimal primal solution with matching LP dual multipliers, which requires handling the interaction between the positive-part shifting need, the lookahead cut-off $s=\lfloor c_p/h\rfloor$ and the end-of-horizon periods.

Formalization scope

Periods are Fin H, with index $0$ as the current period. Data are bundled in RobustVolumeFlex.Params, and LP (4) is stated literally with variables $q,y,z:\mathrm{Fin}\,H\to\mathbb{R}$.

• $\underline D_n,\overline D_n$ are real sInf/sSup over $\Omega$, which is assumed nonempty and bounded so that these are genuine bounds.
• Demand nonnegativity, $h>0$, $c\ge 0$ and $k_n\ge 0$ are the model's standing conventions, made explicit.
• In eq. (6), the published index ranges for the end-of-horizon periods are inconsistent. The formalization orders in period $n$ exactly when $c\le b\,(H-n)$, so the last $u$ periods (with $ub<c\le(u+1)b$) order nothing. Under the no-end-effect hypothesis, this choice does not affect the shifting need.
• The positive part in Definition 1 is written as a fold of $\max$ from $0$.
• The boundary cases of (11), left unspecified in the paper, are assigned to the later case; the order is continuous there, so the choice does not change its value.

Useful contributions include LP duality and optimality-certificate lemmas for finite-horizon inventory LPs, which would be reusable across robust inventory missions. Formalizing the paper's Lemma 1, Corollaries 1–3, Propositions 1–3 and Theorem 2 as milestones is also welcome.

Selected references

• J. Gijsbrechts, C. Imdahl, R. N. Boute, J. A. Van Mieghem, Optimal robust inventory management with volume flexibility: Matching capacity and demand with the lookahead peak-shaving policy, Production and Operations Management 32 (2023) 3357–3373. https://doi.org/10.1111/poms.14069
• E. Porteus, Stochastic inventory theory, Handbooks in Operations Research and Management Science 2 (1990) 605–652.
• D. Bertsimas, A. Thiele, A robust optimization approach to inventory theory, Operations Research 54(1) (2006) 150–168.
• H. Mamani, S. Nassiri, M. R. Wagner, Closed-form solutions for robust inventory management, Management Science 63(5) (2017) 1625–1643.
• C. Bandi, D. Bertsimas, Tractable stochastic analysis in high dimensions via robust optimization, Mathematical Programming 134(1) (2012) 23–70.
• J. Sun, J. A. Van Mieghem, Robust dual sourcing inventory management: Optimality of capped dual index policies, Manufacturing & Service Operations Management 21(4) (2019) 912–931.

Motivation

A matroid records which subsets of a finite set are independent, in the way that sets of columns of a matrix are linearly independent or sets of edges of a graph are acyclic. The matroids that come from matrices over a field $\mathbb F$ are the $\mathbb F$-representable matroids, and deciding which matroids are representable over a given finite field is one of the oldest structural questions of the subject. The class of $\mathrm{GF}(q)$-representable matroids is closed under deletion and contraction, so it is determined by its excluded minors, the minor-minimal matroids outside the class. Listing them is the matroid analogue of Kuratowski's and Wagner's theorems for planar graphs.

Timeline.

• 1958 — Tutte proves that a matroid is binary, i.e. $\mathrm{GF}(2)$-representable, if and only if it has no minor isomorphic to $U_{2,4}$: there is exactly one excluded minor (Tutte 1958).
• 1971 — Rota conjectures that for every finite field the list of excluded minors is finite (Rota 1971).
• 1979 — Bixby and Seymour independently prove that the excluded minors for $\mathrm{GF}(3)$ are $U_{2,5}$, $U_{3,5}$, $F_7$ and $F_7^*$ (Bixby 1979, Seymour 1979).
• 2000 — Geelen, Gerards and Kapoor determine the seven excluded minors for $\mathrm{GF}(4)$ (Geelen–Gerards–Kapoor 2000).
• 2008 — Mayhew and Royle enumerate the matroids on at most nine elements and find hundreds of excluded minors for $\mathrm{GF}(5)$ among them; the complete list for $\mathrm{GF}(5)$ is unknown (Mayhew–Royle 2008).
• 2014 — Geelen, Gerards and Whittle announce a proof of Rota's conjecture built on their matroid minors structure theory. The argument gives no explicit bound on the number of excluded minors, and the full write-up has not appeared (Geelen–Gerards–Whittle 2014).

Setting

A matroid $M$ on a finite ground set $E$ is given by a family $\mathcal I$ of subsets of $E$, the independent sets, such that $\emptyset\in\mathcal I$, every subset of an independent set is independent, and whenever $I,J\in\mathcal I$ with $|I|<|J|$ there is some $x\in J\setminus I$ with $I\cup\{x\}\in\mathcal I$. The maximal independent sets are the bases.

Let $p$ be a prime, $m\ge 1$ an integer, and $\mathrm{GF}(p^m)$ the field with $p^m$ elements. $M$ is $\mathrm{GF}(p^m)$-representable if there are a vector space $W$ over $\mathrm{GF}(p^m)$ and a map $v\colon E\to W$ such that a set $I\subseteq E$ is independent in $M$ exactly when the family $(v(x))_{x\in I}$ is linearly independent.

The deletion $M\backslash D$ has ground set $E\setminus D$ and the independent sets of $M$ contained in $E\setminus D$. The dual $M^*$ has the same ground set, and a set is independent in $M^*$ when its complement contains a base of $M$. The contraction is $M/C := (M^*\backslash C)^*$. A minor of $M$ is a matroid $M/C\backslash D$ with $C,D\subseteq E$ disjoint; it is proper if it differs from $M$. For a class $\mathcal C$ of matroids closed under minors, an excluded minor for $\mathcal C$ is a matroid outside $\mathcal C$ all of whose proper minors lie in $\mathcal C$. Write $\mathrm{EX}(q)$ for the set of excluded minors for $\mathrm{GF}(q)$-representability, counted up to isomorphism.

The challenge is scaled by two natural numbers. For $r,B\in\mathbb N$ let $S(r,B)$ be the statement

$S(r,B)$ implies $S(r',B')$ whenever $r'\le r$ and $B'\ge B$; a contestant chooses $r$ and $B$ and proves $S(r,B)$.

Formalization targets

Goal

This is Rota's conjecture: every finite field has only finitely many excluded minors up to isomorphism. It asserts only the shape of the truth, an unspecified finite bound for each field, and so remains the goal whatever explicit bounds are proved.

Rungs

These are Tutte's theorem, the Bixby–Seymour theorem and the Geelen–Gerards–Kapoor theorem. An explicit bound $B$ with $S(5,B)$ is the first open rung.

Significance

Excluded-minor characterisations are the standard route to recognition algorithms and to the structure theory of a class; for $\mathrm{GF}(2)$, $\mathrm{GF}(3)$ and $\mathrm{GF}(4)$ they underlie the theory of regular, ternary and quaternary matroids. The lists are complete for exactly these three fields. Rota's conjecture settles finiteness in general, but its announced proof gives no bound: an explicit $B$ for $\mathrm{GF}(5)$ would be the first quantitative information on the size of $\mathrm{EX}(5)$ beyond lower bounds from computer search.

Formalizing the rungs produces the representability theory that Mathlib lacks: matrix representations and their duals, uniform matroids, the Fano plane and its relatives, and the minor-closure of representable classes. None of the three theorems has a machine-checked proof; Tutte's theorem alone is a substantial project, and the $\mathrm{GF}(4)$ case is a long paper. The goal itself is proved in the literature only in announced form and is not formalized anywhere.

Difficulty

The obvious attack, enumerating small matroids and testing representability, cannot work: nothing bounds the size of an excluded minor in advance, and bounding it is precisely the content of the problem. Tutte's theorem requires showing that a non-binary matroid can be reduced by deletions and contractions to $U_{2,4}$, which needs either his homotopy theorem or one of the later shorter arguments; the $\mathrm{GF}(3)$ and $\mathrm{GF}(4)$ cases rest on connectivity and splitter-type reductions that are far longer. Counting excluded minors up to isomorphism also forces one to compare matroids on different ground sets.

Formalization scope

Matroids are Mathlib's Matroid α, with ground set M.E : Set α and independence predicate M.Indep; finiteness is M.Finite. Representability is the predicate IsGFRepresentable p m M: there exist a type W with an additive group structure, a module structure over GaloisField p m, and a map v : α → W such that M.Indep I ↔ LinearIndepOn (GaloisField p m) v I for every set I. Because non-independent sets include every set containing an element outside the ground set, a representation sends such elements to $0$. Minors are Mathlib's strict minor order N <m M; IsExcludedMinorFor P M says that $M$ fails $P$ while every strict minor satisfies $P$. Isomorphism is the explicit Matroid.IsIso: a bijection between the ground sets, as subtypes, carrying independent sets exactly to independent sets. ExcludedMinorsAtMost p m B says that some finite set $S$ of at most $B$ matroids on the ground type $\mathbb N$ contains, up to isomorphism, every finite excluded minor for $\mathrm{GF}(p^m)$-representability on any ground type in Type. The rung statement_02 r B quantifies over all primes $p$ and all $m\ge 1$ with $p^m\le r$; it is vacuous for $r\le 1$, and the goal is ∀ r, ∃ B, statement_02 r B.

There is no trivialising reading: $B=0$ is impossible for $r\ge 2$ since $U_{2,4}$ is not binary, and the representatives in $S$ are unconstrained, so the statement is exactly a bound on the number of isomorphism classes. The Lean definitions are copied verbatim from the Ten Challenges repository, so that a proof accepted here is a proof of the benchmark statement. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: an API for matrix representations and duality, the standard small matroids ($U_{2,4}$, $U_{2,5}$, $U_{3,5}$, $F_7$, $F_7^*$) and their non-representability, minor-closure of representable classes, decompositions of the rungs.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 2).
• W. T. Tutte, A homotopy theorem for matroids, I, II, Trans. Amer. Math. Soc. 88 (1958), 144–174. https://doi.org/10.1090/S0002-9947-1958-0101526-0
• R. E. Bixby, On Reid's characterization of the ternary matroids, J. Combin. Theory Ser. B 26 (1979), 174–204. https://doi.org/10.1016/0095-8956(79)90056-X
• P. D. Seymour, Matroid representation over GF(3), J. Combin. Theory Ser. B 26 (1979), 159–173. https://doi.org/10.1016/0095-8956(79)90055-8
• J. F. Geelen, A. M. H. Gerards, A. Kapoor, The excluded minors for GF(4)-representable matroids, J. Combin. Theory Ser. B 79 (2000), 247–299. https://doi.org/10.1006/jctb.2000.1963
• G.-C. Rota, Combinatorial theory, old and new, Actes du Congrès International des Mathématiciens (Nice, 1970), vol. 3, Gauthier-Villars, 1971, 229–233. https://www.mathunion.org/icm/proceedings
• J. Geelen, B. Gerards, G. Whittle, Solving Rota's conjecture, Notices Amer. Math. Soc. 61 (2014), 736–743. https://doi.org/10.1090/noti1139
• D. Mayhew, G. F. Royle, Matroids with nine elements, J. Combin. Theory Ser. B 98 (2008), 415–431. https://doi.org/10.1016/j.jctb.2007.07.005
• J. Oxley, Matroid Theory, 2nd edition, Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001

Motivation

How many copies of a fixed graph $H$ must a graph $G$ of given edge density contain? For bipartite $H$, Sidorenko's conjecture gives the cleanest possible answer: the random graph of the same density contains the fewest, so the homomorphism density of $H$ in $G$ is at least the edge density of $G$ raised to the number of edges of $H$. The statement was conjectured independently by Erdős and Simonovits and by Sidorenko; it is equivalent to a family of integral inequalities for graphons and is a benchmark problem of extremal graph theory, with consequences for quasirandomness, graph norms and the counting of subgraphs in dense graphs (Conlon–Fox–Sudakov 2010, Szegedy 2015).

Timeline.

• 1984/1991 — Erdős and Simonovits, and Sidorenko, pose the conjecture; Sidorenko proves it for trees, even cycles, complete bipartite graphs, and bipartite graphs with at most four vertices on one side (Sidorenko 1991, Sidorenko 1993).
• 2010 — Hatami proves it for hypercubes via graph norms (Hatami 2010); Conlon, Fox and Sudakov prove it for every bipartite graph with a vertex adjacent to all vertices on the other side (Conlon–Fox–Sudakov 2010).
• 2011 — Li and Szegedy extend the vertex-complete case to graphs obtained by gluing (Li–Szegedy 2011).
• 2015 — Szegedy's entropy method and the tree-arrangeable graphs of Kim, Lee and Lee enlarge the known classes (Szegedy 2015, Kim–Lee–Lee 2016).
• 2018 — Conlon, Kim, Lee and Lee prove it for strongly tree-decomposable graphs and for the first bipartite graphs without the vertex-complete property (Conlon–Kim–Lee–Lee 2018); Conlon and Lee prove it for all graphs obtained by gluing enough copies of a bipartite graph along one side (Conlon–Lee 2021).

The smallest bipartite graph for which the conjecture is open is $K_{5,5}$ minus a $10$-cycle, the Möbius ladder on ten vertices; it has five vertices on each side.

Setting

All graphs are finite and simple. A homomorphism from $H$ to $G$ is a map $f\colon V(H)\to V(G)$ with $f(u)f(v)\in E(G)$ for every edge $uv\in E(H)$; $\hom(H,G)$ is the number of homomorphisms and the homomorphism density is

For the single edge $K_2$, $t(K_2,G)=2|E(G)|/|V(G)|^2$ is the edge density. Sidorenko's inequality for $H$ in $G$ is

A graph $H$ is bipartite with sides bounded by $r$ if $V(H)=X\cup Y$ for disjoint sets $X,Y$ with every edge between $X$ and $Y$, $|X|\le r$ and $|Y|\le r$. For $r\in\mathbb N$ let $\mathrm{Sid}(r)$ be the statement

Formalization targets

Goal

Sidorenko's conjecture itself. It is equivalent to $\mathrm{Sid}(r)$ for all $r$, since every finite bipartite graph has sides bounded by some $r$.

Rungs

$\mathrm{Sid}(r)$ for $r\le 4$ follows from Sidorenko's theorem on bipartite graphs with at most four vertices on one side. $\mathrm{Sid}(5)$ is the first open rung; it contains the Möbius ladder $K_{5,5}\setminus C_{10}$.

Significance

The conjecture determines the minimum number of copies of every bipartite graph in graphs of given density, the bipartite half of the subgraph-counting problem whose non-bipartite half (for which the random graph is not extremal, by Thomason's examples) is far less understood. It is equivalent to the statement that every bipartite graph is "common" in the sense of Erdős and to the positivity of a class of graphon integrals; it would also settle a conjecture of Simonovits on the Turán numbers of bipartite graphs in the degenerate regime. The rungs with $r\le 4$ are proved; every further rung is open.

Formalizing the conjecture builds homomorphism counting on Mathlib's SimpleGraph, which has graph homomorphisms but no density theory: the Cauchy–Schwarz and tensor-power arguments for trees and even cycles, the entropy method, and the vertex-complete theorem would all become reusable. No case of Sidorenko's conjecture has a machine-checked proof.

Difficulty

The obvious approach, applying Cauchy–Schwarz edge by edge, proves the inequality only for graphs that can be built by repeated "gluing" along stars, which is why trees, even cycles and complete bipartite graphs are the easy cases. The known proofs for harder graphs replace Cauchy–Schwarz by entropy inequalities on random homomorphisms, and the entropy method is known to fail for some graphs on five plus five vertices. A counterexample, if one exists, would need to beat the random graph in a quantity for which every known test (graph norms, local Sidorenko, forcing) is positive.

Formalization scope

Graphs are Mathlib's SimpleGraph on finite types W (for $H$) and V (for $G$), both in Type; the host $G$ has [Nonempty V], so $|V(G)|\ge 1$ and the density is a genuine quotient. homDensity H G : ℝ is Nat.card of the subtype of maps $W\to V$ sending adjacent vertices to adjacent vertices, divided by $|V|^{|W|}$ as real numbers; SidorenkoFor H G is the inequality $t(H,G)\ge t(K_2,G)^{e(H)}$ with $K_2$ = completeGraph (Fin 2) and $e(H)$ = Nat.card H.edgeSet. BipartiteBoundedBy H k asks for sets $X,Y$ with Mathlib's H.IsBipartiteWith X Y (disjoint, every edge between them), $X\cup Y$ the whole vertex set, and X.ncard ≤ k, Y.ncard ≤ k. The rung statement_04 r quantifies over all such $H$ and all nonempty finite $G$. The goal states the conjecture directly: for every finite $H$ admitting sets $X,Y$ with H.IsBipartiteWith X Y and $X\cup Y$ the whole vertex set, and every nonempty finite $G$, SidorenkoFor H G; it is equivalent to ∀ r, statement_04 r, the universal form of the benchmark.

No trivialising reading: both sides are real numbers in $[0,1]$, the exponent counts edges of $H$ exactly, and for $r=0$ the only admissible $H$ is the empty graph, for which both sides equal $1$. The Lean definitions are copied verbatim from the Ten Challenges repository. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: the multiplicativity of $\hom$ over disjoint unions, $t(K_2,G)=2e(G)/n^2$, the tree and even-cycle cases, a reduction of $\mathrm{Sid}(r)$ to a finite list of graphs $H$ for small $r$.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 4).
• A. F. Sidorenko, Inequalities for functionals generated by bipartite graphs, Diskret. Mat. 3 (1991), 50–65 (Russian); English translation Discrete Math. Appl. 2 (1992), 489–504. https://doi.org/10.1515/dma.1992.2.5.489
• A. F. Sidorenko, A correlation inequality for bipartite graphs, Graphs Combin. 9 (1993), 201–204. https://doi.org/10.1007/BF02988307
• H. Hatami, Graph norms and Sidorenko's conjecture, Israel J. Math. 175 (2010), 125–150. https://doi.org/10.1007/s11856-010-0005-1
• D. Conlon, J. Fox, B. Sudakov, An approximate version of Sidorenko's conjecture, Geom. Funct. Anal. 20 (2010), 1354–1366. https://doi.org/10.1007/s00039-010-0097-0
• J. L. X. Li, B. Szegedy, On the logarithmic calculus and Sidorenko's conjecture, 2011. https://arxiv.org/abs/1107.1153
• B. Szegedy, An information theoretic approach to Sidorenko's conjecture, 2015. https://arxiv.org/abs/1406.6738
• J. H. Kim, C. Lee, J. Lee, Two approaches to Sidorenko's conjecture, Trans. Amer. Math. Soc. 368 (2016), 5057–5074. https://doi.org/10.1090/tran/6487
• D. Conlon, J. H. Kim, C. Lee, J. Lee, Some advances on Sidorenko's conjecture, J. London Math. Soc. 98 (2018), 593–608. https://doi.org/10.1112/jlms.12142
• D. Conlon, J. Lee, Sidorenko's conjecture for blow-ups, Discrete Analysis 2021:2. https://doi.org/10.19086/da.21472

Motivation

Ramsey's theorem guarantees that every graph on $n$ vertices has a clique or an independent set of size about $\tfrac12\log_2 n$, and random graphs show that this is best possible. The Erdős–Hajnal conjecture says that forbidding any single induced subgraph $H$ changes the picture completely: $H$-free graphs should contain cliques or independent sets of polynomial size $n^{c_H}$. The conjecture is a central problem of structural graph theory, linking induced subgraphs, perfect graphs and Ramsey theory (Chudnovsky 2014).

Timeline.

• 1977/1989 — Erdős and Hajnal pose the conjecture and prove that $H$-free graphs contain cliques or independent sets of size $\exp(c\sqrt{\log n})$ (Erdős–Hajnal 1989).
• 2001 — Alon, Pach and Solymosi show that the conjecture is closed under substitution, giving it for a family of graphs built from small cases (Alon–Pach–Solymosi 2001).
• 2008 — Chudnovsky and Safra prove it for the bull (Chudnovsky–Safra 2008).
• 2023 — Chudnovsky, Scott, Seymour and Spirkl prove it for the five-vertex cycle (Chudnovsky–Scott–Seymour–Spirkl 2023).
• 2023 — Bucić, Nguyen, Scott and Seymour improve the general bound to $\exp(c\sqrt{\log n\log\log n})$ (Bucić–Nguyen–Scott–Seymour 2023).
• 2023/2026 — Nguyen, Scott and Seymour prove it for the five-vertex path $P_5$, completing all graphs on five vertices; they also show that for every path $P$ and every $d<1$, $P$-free graphs contain cliques or independent sets of size $2^{(\log n)^d}$ (Nguyen–Scott–Seymour, ISD V, ISD VII).

The conjecture is open for the six-vertex path $P_6$, and for every longer path.

Setting

All graphs are finite and simple. A set of vertices is a clique if its vertices are pairwise adjacent and an independent set (or stable set) if they are pairwise non-adjacent. For graphs $G$ and $H$, $G$ is $H$-free if no induced subgraph of $G$ is isomorphic to $H$. The path $P_r$ has $r$ vertices $v_1,\dots,v_r$ and edges $v_iv_{i+1}$. For $r\in\mathbb N$ let $\mathrm{EH}(r)$ be the statement

The constant $c$ may depend on $r$ but not on $G$.

Formalization targets

Goal

Rungs

$\mathrm{EH}(4)$ ($P_4$-free graphs are cographs, hence perfect, and $c=\tfrac12$ works), $\mathrm{EH}(5)$ (Nguyen, Scott, Seymour), and the first open rung $\mathrm{EH}(6)$. The rungs $r\le 3$ are exercises: $P_2$-free graphs are edgeless, $P_3$-free graphs are disjoint unions of cliques.

Significance

Paths are the test case for the conjecture: a proof for all paths would, by the substitution theorem and the known closure properties, settle it for a large class of graphs, and the methods developed for $P_5$ (sparse–dense dichotomies, "polynomial Rödl" theorems) are the current state of the art. The weaker near-polynomial bound $2^{(\log n)^{1-o(1)}}$ is known for all paths, so the gap to be closed is precisely the exponent.

Formalizing the rungs builds the induced-subgraph vocabulary (induced embeddings of paths, cographs, the clique–independent set dichotomy) on top of Mathlib's SimpleGraph. $\mathrm{EH}(4)$ via perfection of cographs is a realistic first project; $\mathrm{EH}(5)$ is a long paper with no machine-checked proof. The goal and $\mathrm{EH}(6)$ are open.

Difficulty

The Erdős–Hajnal argument gives only $\exp(c\sqrt{\log n})$ because each step of its density increment loses a constant factor; the polynomial regime requires structure specific to the forbidden graph. For $P_5$ the proof needs a new "polynomial" version of Rödl's theorem for $P_5$-free graphs together with a delicate analysis of sparse and dense configurations; none of it is known to extend to $P_6$. The naive idea, induction on $r$ by deleting a vertex, loses the forbidden structure.

Formalization scope

Graphs are Mathlib's SimpleGraph V with [Fintype V] and V : Type (the lowest universe); $H$-freeness is ¬ H ⊴ G with Mathlib's induced-subgraph relation ⊴ (an injective graph homomorphism that reflects adjacency). ErdosHajnalConjectureFor H states: there is a real $c>0$ such that every finite $H$-free graph $G$ has a Finset $s$ which is a clique of $G$ or a clique of the complement $G^{c}$, with $|s|\ge |V|^{c}$ as real numbers (real exponentiation). The rung statement_05 r is ErdosHajnalConjectureFor (pathGraph r), with Mathlib's pathGraph r on Fin r. For $r\le 1$ the path embeds in every graph with enough vertices, so the hypothesis is vacuous or nearly so; the content starts at $r=2$. The goal is ∀ r, statement_05 r.

No trivialising reading: $c$ is chosen before $G$, the empty graph on $0$ vertices satisfies the conclusion with $s=\emptyset$ since $0^c=0$, and the clique-or-independent-set alternative is genuine. The Lean definitions are copied verbatim from the Ten Challenges repository. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: an API for $P_r$-freeness (characterisations of $P_3$-free and $P_4$-free graphs), perfection of cographs, the exercises $r\le 3$, decompositions of $\mathrm{EH}(4)$ and $\mathrm{EH}(5)$.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 5).
• P. Erdős, A. Hajnal, Ramsey-type theorems, Discrete Appl. Math. 25 (1989), 37–52. https://doi.org/10.1016/0166-218X(89)90045-0
• M. Chudnovsky, The Erdős–Hajnal conjecture: a survey, J. Graph Theory 75 (2014), 178–190. https://doi.org/10.1002/jgt.21730
• N. Alon, J. Pach, J. Solymosi, Ramsey-type theorems with forbidden subgraphs, Combinatorica 21 (2001), 155–170. https://doi.org/10.1007/s004930100016
• M. Chudnovsky, S. Safra, The Erdős–Hajnal conjecture for bull-free graphs, J. Combin. Theory Ser. B 98 (2008), 1301–1310. https://doi.org/10.1016/j.jctb.2008.02.005
• M. Chudnovsky, A. Scott, P. Seymour, S. Spirkl, Erdős–Hajnal for graphs with no 5-hole, Proc. London Math. Soc. 126 (2023), 997–1014. https://doi.org/10.1112/plms.12504
• M. Bucić, T. Nguyen, A. Scott, P. Seymour, Induced subgraph density. I. A loglog step towards Erdős–Hajnal, 2023. https://arxiv.org/abs/2301.10147
• T. Nguyen, A. Scott, P. Seymour, Induced subgraph density. V. All paths approach Erdős–Hajnal, 2023. https://arxiv.org/abs/2307.15032
• T. Nguyen, A. Scott, P. Seymour, Induced subgraph density. VII. The five-vertex path, Proc. London Math. Soc. (2026). https://arxiv.org/abs/2312.15333

Motivation

The Graph Minor Theorem of Robertson and Seymour states that finite graphs are well-quasi-ordered by the minor relation: in every infinite sequence of finite graphs, some graph is a minor of a later one. It is one of the deepest results of combinatorics, and it implies that every minor-closed class of graphs is characterised by finitely many excluded minors. Nash-Williams introduced the stronger notion of better-quasi-ordering (BQO) in the 1960s, precisely because well-quasi-ordering is not preserved under the natural infinitary constructions (Rado's example): BQO is preserved under taking subsets, sequences and transfinite iterations of these. Whether finite graphs are better-quasi-ordered under minors is a folklore conjecture that has resisted every attempt; the only known route, the Graph Minor Theorem, gives well-quasi-ordering and nothing more (Georgakopoulos 2025).

Timeline.

• 1954 — Rado exhibits a well-quasi-order whose power set is not well-quasi-ordered (Rado 1954).
• 1965/1968 — Nash-Williams introduces better-quasi-orders and proves that they are closed under the operations that break well-quasi-orders; infinite trees are BQO under topological minors (Nash-Williams 1965).
• 1983–2004 — Robertson and Seymour prove the Graph Minor Theorem (Robertson–Seymour 2004).
• 1988 — Thomas shows that infinite graphs are not well-quasi-ordered under minors and conjectures that countable graphs are (Thomas 1988).
• 2025 — Georgakopoulos proves that the BQO conjecture for finite graphs is equivalent to Thomas's conjecture restricted to rayless countable graphs (Georgakopoulos 2025).

Setting

A quasi-order is a reflexive, transitive relation $\le$ on a set $Q$. It is a well-quasi-order (WQO) if for every sequence $q_0,q_1,\dots$ in $Q$ there are $i<j$ with $q_i\le q_j$.

For a set $Q$ and an ordinal $\alpha$ define the cumulative hierarchy $V^*_\alpha(Q)$ by $V^*_0(Q)=Q$, $V^*_{\beta+1}(Q)=\mathcal P^*(V^*_\beta(Q))$ (the nonempty subsets), and $V^*_\lambda(Q)=\dot\bigcup_{\beta<\lambda}V^*_\beta(Q)$ (disjoint union) for limit $\lambda$. Extend $\le$ to a relation $\le^*$ on the hierarchy by a two-player game from a position $(X,Y)$: if both $X$ and $Y$ lie in $Q$, Player II wins if $X\le Y$; otherwise Player I names $X'$, which is $X$ itself if $X\in Q$ and an element of $X$ otherwise, then Player II names $Y'$ in the same way from $Y$, and play continues from $(X',Y')$; an element of a limit level is identified with its underlying element of a lower level. Then $X\le^* Y$ means that Player II has a winning strategy from $(X,Y)$. The quasi-order $(Q,\le)$ is $\alpha$-well-quasi-ordered if $(V^*_\alpha(Q),\le^*)$ is well-quasi-ordered. Thus $0$-WQO is WQO, and $(Q,\le)$ is BQO exactly when it is $\omega_1$-WQO, equivalently $\alpha$-WQO for every ordinal $\alpha$.

Finite graphs are ordered by $G\preceq H$ if $G$ is a minor of $H$: $H$ contains pairwise disjoint connected branch sets $B_v$, one for each vertex $v$ of $G$, with an edge of $H$ between $B_u$ and $B_v$ for every edge $uv$ of $G$. A finite graph is planar if it has neither $K_5$ nor $K_{3,3}$ as a minor (Wagner's criterion). The challenge interleaves planar graphs and all graphs: for an ordinal $r$, write $r=2\cdot\alpha+k$ with $k\in\{0,1\}$ and let