Completed

Algebraic Topology Differential Geometry Mathematical Physics·Captain: Lucas

Gribov Ambiguity: no continuous gauge fixing (Singer 1978)Research Paper

Motivation

In the Feynman path-integral approach to a non-abelian gauge theory one wants to integrate a gauge-invariant weight over the space $\mathfrak{A}$ of vector potentials (connections) of a principal bundle. The integrand is constant on the orbits of the group $\mathcal{G}$ of gauge transformations, so the integral over $\mathfrak{A}$ diverges and one is supposed to integrate instead over the orbit space $\mathfrak{R} = \mathfrak{A}/\mathcal{G}$ . The Faddeev–Popov procedure realizes this by fixing a gauge: choosing, continuously in the orbit, exactly one vector potential on each orbit, and correcting by a Jacobian determinant.

V. N. Gribov (SLAC Translation 176, 1977) observed that for $SU(2)$ potentials on $\mathbb{R}^3$ (or $\mathbb{R}^4$ ) with suitable conditions at infinity, the Coulomb gauge condition does not do this: the Coulomb slice through the zero potential meets the orbit of the zero potential again, far from the origin. These extra intersections are the Gribov copies; R. Jackiw, I. Muzinich and C. Rebbi (Phys. Rev. D 17 (1978) 1576) analyzed them in detail.

I. M. Singer, Some Remarks on the Gribov Ambiguity (Commun. Math. Phys. 60 (1978) 7–12), showed that the phenomenon is not a defect of the Coulomb gauge. If the conditions at infinity are those of Gribov — gauge transformations extending to the one-point compactification with value $I$ at infinity, so that the base manifold is $M = S^3$ or $M = S^4$ — then no continuous gauge fixing exists at all, in any gauge. The obstruction is topological: the space of irreducible connections is weakly contractible, while the gauge group is not, and a weakly contractible principal bundle admits no global continuous section.

Setting

Fix $N \ge 2$ and take the structure group $SU(N)$ , the group of $N \times N$ complex matrices $U$ with $U^\ast U = I$ and $\det U = 1$ , topologized as a subspace of matrices. Let $S^r$ denote the unit sphere of $\mathbb{R}^{r+1}$ , with base point $m$ the north pole.

For the trivial $SU(N)$ -bundle over a space $M$ , a gauge transformation is a map $\varphi : M \to SU(N)$ , and the gauge group is

\mathcal{G}(M,N) \;=\; C\bigl(M, SU(N)\bigr),

continuous maps with pointwise multiplication and the compact-open topology. Two subobjects matter. The based gauge group $\mathcal{G}_m = \{\varphi : \varphi(m) = I\}$ is the subgroup of transformations that are the identity at the base point. The constant transformations with value in the centre $Z_N = \{e^{2\pi i k/N} I\}$ of $SU(N)$ form a normal subgroup, and the reduced gauge group is the quotient

\overline{\mathcal{G}}(M,N) \;=\; \mathcal{G}(M,N)/Z_N

with the quotient topology. The centre acts trivially on vector potentials, so $\overline{\mathcal{G}}$ is the group that acts effectively.

A group $G$ acting continuously on a space $\mathfrak{A}$ has orbit space $\mathfrak{A}/G$ with the quotient topology, and a gauge fixing is a continuous map $s : \mathfrak{A}/G \to \mathfrak{A}$ with $p \circ s = \mathrm{id}$ , where $p : \mathfrak{A} \to \mathfrak{A}/G$ is the projection: a continuous choice of exactly one point on each orbit. The action is principal when it is free and the division map, which sends a pair of points on one orbit to a group element carrying the second to the first, can be chosen continuously; this is the topological content of " $p$ is a principal $G$ -bundle". The space $\mathfrak{A}$ is weakly contractible when it is nonempty and all its homotopy groups vanish.

In the paper, $\mathfrak{A}$ is the affine space of connections, $\mathfrak{R}$ its set of irreducible members, and Theorems 1 and 2 say exactly that $\mathfrak{R}$ is a weakly contractible principal $\overline{\mathcal{G}}$ -space.

Formalization targets

Goal — Corollary 4 (no gauge fixing)

For $r \in \{3,4\}$ , $N \ge 2$ , and every weakly contractible principal $\overline{\mathcal{G}}(S^r,N)$ -space $A$ :

\nexists\, s : A/\overline{\mathcal{G}}(S^r,N) \longrightarrow A \quad\text{continuous with}\quad p \circ s = \mathrm{id}.

By Theorems 1 and 2 of the paper the space of irreducible connections over $S^3$ or $S^4$ is such an $A$ , so the goal contains Singer's Corollary 4 for that space; it leaves the analytic construction of the space of connections unfixed, which is what makes it statable today.

Milestone level — Theorem 3

\exists\, j \ge 1: \quad \pi_j\bigl(\overline{\mathcal{G}}(S^r,N)\bigr) \neq 0, \qquad r \in \{3,4\},\ N \ge 2 .

Milestone level — Theorem 5 and its homotopy inputs

\pi_j\bigl(\mathcal{G}_m(S^r,N)\bigr) \;\cong\; \pi_{j+r}\bigl(SU(N)\bigr), \qquad \pi_3(SU(N)) \cong \mathbb{Z}, \qquad \pi_4(SU(N)) = 0 \ (N\ge 3), \qquad \pi_4(SU(2)) \cong \mathbb{Z}/2 .

Significance

The result rules out the existence of a global gauge in the topological sense: every gauge condition used in practice is at best a local slice, and the Faddeev–Popov construction has to be read as a local statement, patched with a partition of unity over the orbit space (as the last section of the paper proposes). It is the mathematical reason why the Gribov ambiguity cannot be repaired by a cleverer gauge condition, and it is the origin of the Gribov–Zwanziger restriction of the functional integral to a fundamental domain.

Formalizing it adds a machine-checked version of an argument that is quoted far more often than it is checked, and it forces into Lean a piece of infrastructure that Mathlib currently lacks: homotopy groups of mapping spaces, the long exact sequence of a fibration in the form needed for $0 \to \mathcal{G}_m \to \mathcal{G} \to SU(N) \to 0$ , and the classical computations $\pi_3(SU(N)) \cong \mathbb{Z}$ , $\pi_4(SU(N)) = 0$ for $N \ge 3$ , $\pi_4(SU(2)) \cong \mathbb{Z}/2$ . Singer's results are proved mathematics; none of them is formalized, and Mathlib as of the pinned revision contains homotopy groups as a definition together with their group structure, but essentially no computation of them.

Difficulty

The naive approach to the goal — build a section by hand, or average over the group — fails because $\overline{\mathcal{G}}$ is neither compact nor contractible and the obstruction is global: locally, slices do exist (that is the content of the generalized Coulomb gauge), so no local argument can produce a contradiction. The proof has to convert a section into a homotopy-theoretic statement: a section of a principal bundle trivializes it, exhibiting the group as a retract of the total space, so all homotopy groups of the group would vanish; the work is then to show that some homotopy group of the reduced gauge group does not vanish, which needs the identification of the based gauge group with a mapping space, the exact sequences relating $\mathcal{G}_m$ , $\mathcal{G}$ and $\overline{\mathcal{G}}$ , and non-trivial homotopy groups of $SU(N)$ — including $\pi_6(S^3) \cong \mathbb{Z}/12$ for the $SU(2)$ case of Theorem 3.

Formalization scope

The formalization commits to the following conventions, all of them visible in the definitions of this mission.

The bundle is the trivial $SU(N)$ -bundle, so gauge transformations are literally maps $M \to SU(N)$ . This is the case of Gribov's original setting over $S^3$ ; over $S^4$ the paper also treats bundles of nonzero Pontrjagin index, which are out of scope here.
Gauge transformations are continuous, not smooth, with the compact-open topology; Singer's Theorem 5 uses smoothing homotopies to pass between the two, and the homotopy-theoretic content is the same.
$SU(N)$ is the special unitary group of complex $N \times N$ matrices, with its subspace topology; $S^r$ is the unit sphere of $\mathbb{R}^{r+1}$ with its subspace topology.
Homotopy groups are Mathlib's HomotopyGroup, based at the identity element.
The space of connections is not constructed: Mathlib has no space of connections on a principal bundle, and building one is a mission of its own. The goal therefore quantifies over an arbitrary topological space carrying a weakly contractible principal action of the reduced gauge group — exactly the properties Theorems 1 and 2 establish for the irreducible connections.
This quantification is not vacuous: such spaces exist (the total space of a universal $\overline{\mathcal{G}}$ -bundle is one), so the goal is a genuine non-existence statement and not a statement about an empty class. Conversely it is not trivially true: the hypotheses do not mention any homotopy invariant of the gauge group, and refuting a section requires Theorem 3.
The paper's analytic statements — Theorem 1 (openness and density of the irreducible connections, principal bundle structure), Theorem 2 (weak contractibility), Theorem 6 ( $\pi_1$ of the irreducible orbit space), Theorem 7 (no flat connection), Theorem 8 (tangency of orbits to the Coulomb slice) and Theorem 9 (the canonical connection and its curvature) — are out of scope until a space of connections exists in Lean. Contributions that build one, in reusable form, are welcome and would let this mission be extended to them.

Selected references

V. N. Gribov, Instability of non-abelian gauge theories and impossibility of choice of Coulomb gauge, SLAC Translation 176 (1977); Nucl. Phys. B 139 (1978) 1–19, doi:10.1016/0550-3213(78)90175-X.
I. M. Singer, Some Remarks on the Gribov Ambiguity, Commun. Math. Phys. 60 (1978) 7–12, doi:10.1007/BF01609471.
R. Jackiw, I. Muzinich, C. Rebbi, Coulomb gauge description of large Yang-Mills fields, Phys. Rev. D 17 (1978) 1576, doi:10.1103/PhysRevD.17.1576.
H. Toda, Composition methods in homotopy groups of spheres, Annals of Mathematics Studies 49, Princeton University Press (1962).

8 thms2 active usersReviewed

Algebraic Geometry Geometry & Topology·Captain: Lucas

Algebraicity of Weil classes on abelian sixfolds of discriminant -1Research Paper

Motivation

The Hodge conjecture predicts that on a non-singular complex projective variety $X$ every rational cohomology class of type $(p,p)$ is a rational linear combination of the classes of algebraic subvarieties of $X$ . Abelian varieties are the oldest testing ground for the conjecture, and the hardest known classes on them were isolated by A. Weil. A $2n$ -dimensional complex abelian variety $A$ is of Weil type for an imaginary quadratic field $K=\mathbb{Q}(\sqrt{-d})$ if $K$ embeds into $\mathrm{End}_{\mathbb{Q}}(A)$ in such a way that both eigenspaces of $\eta(\sqrt{-d})$ meet $H^{1,0}(A)$ in an $n$ -dimensional subspace. Such an $A$ carries a distinguished two-dimensional space of rational $(n,n)$ -classes, the Weil classes, which for a generic $A$ of Weil type does not lie in the subring generated by divisor classes. Weil classes are therefore the standard obstruction to the Hodge conjecture in low dimension: for abelian fourfolds the conjecture reduces to their algebraicity.

Timeline of the unconditional results on algebraicity of Weil classes:

A. Weil (1977) constructed the classes and showed that the generic abelian variety of Weil type has a three-dimensional space of rational $(n,n)$ -classes, spanned by $h^n$ and the two-dimensional Weil plane.
C. Schoen (Compositio Math. 65 (1988) and its 1998 Addendum, Compositio Math. 114) proved algebraicity for fourfolds of Weil type with $K=\mathbb{Q}(\sqrt{-3})$ and arbitrary discriminant, for sixfolds with $K=\mathbb{Q}(\sqrt{-3})$ and trivial discriminant, and for fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$ ; a second proof of the last case is in B. van Geemen's survey (1994).
K. Koike (Canad. Math. Bull. 47 (2004)) proved algebraicity for sixfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$ , which yields fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and arbitrary discriminant.
E. Markman (JEMS 25 (2023)) proved algebraicity for fourfolds, arbitrary $K$ , and discriminant $1$ .
E. Markman, arXiv:2502.03415, proves algebraicity for sixfolds of discriminant $-1$ and every imaginary quadratic $K$ , and deduces the Hodge conjecture for all abelian fourfolds.

Setting

Fix $g$ and present a $g$ -dimensional complex torus by its first homology: a complex structure $J$ on $H_1(A,\mathbb{R})=\mathbb{R}^{2g}$ with $J^2=-1$ , the lattice being $\mathbb{Z}^{2g}\subset\mathbb{R}^{2g}$ . A polarization is a rational alternating form $E$ on $H_1(A,\mathbb{Q})=\mathbb{Q}^{2g}$ satisfying the Riemann relations $E(Jx,Jy)=E(x,y)$ and $E(x,Jx)>0$ for $x\neq 0$ . Cohomology is $H^k(A,\mathbb{C})=\wedge^k H^1(A,\mathbb{C})$ , realized as the alternating $\mathbb{C}$ -multilinear forms on $H_1(A,\mathbb{C})=\mathbb{C}^{2g}$ ; a class is rational if its values on rational vectors are rational, and it has type $(p,q)$ if it is multiplied by $z^p\bar z^{q}$ under the scaling action $v\mapsto (\mathrm{Re}\,z)v+(\mathrm{Im}\,z)Jv$ of $z\in\mathbb{C}$ . A Hodge class of degree $2p$ is a rational class of type $(p,p)$ .

Let $g=2n$ and $K=\mathbb{Q}(\sqrt{-d})$ with $d>0$ . A polarized abelian $2n$ -fold of Weil type is such an $(A,E)$ together with a rational endomorphism $M=\eta(\sqrt{-d})$ of $H_1(A,\mathbb{Q})$ with

M^2=-d,\qquad MJ=JM,\qquad E(Mx,My)=d\,E(x,y),

the last condition saying that $\eta(k)$ multiplies the polarization class by the norm $\mathrm{Nm}(k)$ , and such that each of the two eigenspaces $W,\overline{W}\subset H_1(A,\mathbb{C})$ of $M$ meets the $i$ -eigenspace of $J$ in an $n$ -dimensional subspace. The Hodge–Weil classes are the rational classes in

\widehat{HW}\;=\;\big(\wedge^{2n}W\;\oplus\;\wedge^{2n}\overline{W}\big)\cap H^{2n}(A,\mathbb{Q}),

equivalently the rational degree- $2n$ classes that vanish on every tuple of vectors containing both a vector of $W$ and a vector of $\overline{W}$ .

The form $H(x,y)=E(Mx,y)+\sqrt{-d}\,E(x,y)$ is $K$ -valued and hermitian on $H_1(A,\mathbb{Q})$ , viewed as a $K$ -vector space through $\eta$ . The determinant of its Gram matrix in a $K$ -basis lies in $\mathbb{Q}^{\times}$ , and its class in $\mathbb{Q}^{\times}/\mathrm{Nm}(K^{\times})$ is the discriminant $\det H$ of $(A,\eta,h)$ . Discriminant $-1$ means that this determinant equals $-(a^2+dc^2)$ for some rationals $a,c$ not both zero.

Algebraicity is not modelled abstractly. An abelian variety is tied to a genuine non-singular projective variety $X\subseteq\mathbb{P}^N$ by a projective realization: a smooth, $\mathbb{Z}^{2g}$ -periodic immersion $u:\mathbb{R}^{2g}\to X$ , surjective onto $X$ and injective modulo the lattice, whose differential intertwines $J$ with the complex structure of $\mathbb{P}^N$ . A class $w\in H^{2p}(A,\mathbb{C})$ is algebraic when some de Rham class of $X$ whose periods over the $2p$ -cycles swept out by rational vectors $\lambda_1,\dots,\lambda_{2p}$ equal $w(\lambda_1,\dots,\lambda_{2p})$ is a rational combination of cycle classes $\mathrm{cl}(Z)$ of irreducible subvarieties $Z\subseteq X$ of dimension $g-p$ . Cycle classes, de Rham cohomology of a projective variety, $(p,q)$ -types and Hodge classes are taken from the platform's HodgeConjecture bundle, which formalizes §1 of Deligne's Clay problem description.

Formalization targets

Goal — Theorem 1.5.1 of arXiv:2502.03415

\text{For every } d>0:\ \text{the Hodge–Weil classes of a polarized abelian sixfold of Weil type with CM by }\mathbb{Q}(\sqrt{-d})\text{ and discriminant }-1\text{ are algebraic.}

The statement fixes neither the field $K$ nor the sixfold: it quantifies over every $d>0$ , every polarized abelian sixfold of Weil type of discriminant $-1$ , and every projective realization of it.

Milestone — Weil's plane of Hodge–Weil classes (§1.1)

\widehat{HW}\ \text{is a two-dimensional }\mathbb{Q}\text{-space, and each of its elements has type }(n,n).

Milestone — Schoen's degeneration step (§1.6)

\text{Goal for all sixfolds of discriminant }-1\ \Longrightarrow\ \text{Hodge–Weil classes of every abelian fourfold of Weil type are algebraic,}

for every imaginary quadratic $K$ and every discriminant; this is the use made of Schoen's Proposition 10 (Compositio Math. 114 (1998)) in the paper.

Milestone — Corollary 1.6.1

\text{The Hodge conjecture holds for abelian fourfolds.}

Milestone — Lefschetz $(1,1)$

Divisor classes: every Hodge class in $H^2$ of a non-singular projective variety is algebraic. This is an already published platform statement, imported here as a reference, since the reduction in Corollary 1.6.1 uses the algebraicity of divisor classes.

Significance

Weil classes are, by the results of Moonen–Zarhin (Duke Math. J. 77 (1995), Math. Ann. 315 (1999)), the only obstruction left in dimension four: for a simple abelian fourfold $H^{2,2}(A,\mathbb{Q})$ is spanned by quadratic expressions in divisor classes and by Weil classes, and the non-simple cases reduce to products treated by Ramón Marí (Collect. Math. 59 (2008)) and Moonen–Zarhin. The goal theorem therefore closes the Hodge conjecture for abelian fourfolds, the first dimension in which the conjecture for abelian varieties was open.

Formalizing it produces, first, a reusable Lean model of polarized abelian varieties, of complex multiplication of Weil type, of the Hodge–Weil plane and of the discriminant, tied to an honest notion of algebraic cohomology class through projective realizations. None of these objects exists in Mathlib today. The result itself is proved in the source preprint and has no machine-checked proof; the milestones below are equally unformalized, including the classical statements of Weil and Schoen that the paper's Corollary depends on.

Difficulty

The naive attack — write down subvarieties whose classes span $\widehat{HW}$ — fails because Weil classes are not expressible through divisors: for a generic abelian variety of Weil type the Néron–Severi group is cyclic while $H^{n,n}(A,\mathbb{Q})$ is three-dimensional, so no product of divisor classes reaches the Weil plane. The source constructs instead a reflexive sheaf $\mathcal{E}$ on $X\times\hat X$ , for $X$ the Jacobian of a genus- $3$ curve, whose characteristic class $\kappa(\mathcal{E})$ remains of Hodge type along all deformations of $(X\times\hat X,\eta,h)$ as a polarized abelian sixfold of Weil type, and deforms the pair over that moduli space using a semiregularity theorem for twisted sheaves. Each of these steps — Orlov's derived equivalence, spinor geometry of the Mukai lattice, semiregularity — is itself missing from Mathlib, which is why the milestone list stays on the Hodge-theoretic side of the argument rather than transcribing the sheaf-theoretic core.

Formalization scope

Conventions the Lean development commits to:

Complex tori are presented by $(J,E)$ on $\mathbb{R}^{2g}$ with the lattice $\mathbb{Z}^{2g}$ ; the polarization form is rational rather than integral, which is the isogeny-invariant form of the Riemann relations.
Cohomology is the space of alternating multilinear forms on $H_1(A,\mathbb{C})$ , i.e. invariant forms on the torus; a period over a lattice cube is used to compare it with the de Rham cohomology of a projective realization.
The Weil condition is imposed symmetrically on both eigenspaces of $\eta(\sqrt{-d})$ , so it does not depend on the choice of convention for $H^{1,0}$ versus $H^{0,1}$ .
Discriminant $-1$ is stated as the existence of a $K$ -basis in which the Gram determinant of $H$ is $-\mathrm{Nm}(k)$ ; changing the basis multiplies the determinant by a norm, so the condition is basis-independent.
Algebraicity always refers to cycle classes of subvarieties of an actual projective variety, in the sense of Deligne's formulation, never to an abstract subspace of "algebraic" classes; in particular the goal cannot be satisfied by exhibiting a formal object, and the hypotheses are satisfiable — abelian varieties of Weil type of discriminant $-1$ exist for every $K$ , and abelian varieties admit projective realizations.

A complete development needs, beyond what is drafted here: the spin representation of the Mukai lattice of an abelian $n$ -fold, pure spinors and $K$ -secant lines, Orlov's equivalence, Atiyah classes and semiregularity for twisted sheaves. Contributions establishing any of these, or proving the Hodge-theoretic milestones, are welcome.

Selected references

E. Markman, Cycles on abelian $2n$ -folds of Weil type from secant sheaves on abelian $n$ -folds, arXiv:2502.03415. https://arxiv.org/abs/2502.03415
A. Weil, Abelian varieties and the Hodge ring, Collected Papers III, Springer 1980, 421–429.
C. Schoen, Hodge classes on self-products of a variety with an automorphism, Compositio Math. 65 (1988), 3–32; Addendum, Compositio Math. 114 (1998), 329–336. https://eudml.org/doc/89880
B. van Geemen, An introduction to the Hodge conjecture for abelian varieties, Lecture Notes in Math. 1594, Springer 1994, 233–252. https://doi.org/10.1007/BFb0094425
K. Koike, Algebraicity of some Weil Hodge classes, Canad. Math. Bull. 47 (2004), 566–572. https://doi.org/10.4153/CMB-2004-055-3
B. Moonen, Y. Zarhin, Hodge classes and Tate classes on simple abelian fourfolds, Duke Math. J. 77 (1995), 553–581. https://doi.org/10.1215/S0012-7094-95-07717-5
B. Moonen, Y. Zarhin, Hodge classes on abelian varieties of low dimension, Math. Ann. 315 (1999), 711–733. https://doi.org/10.1007/s002080050333
J. Ramón Marí, On the Hodge conjecture for products of certain surfaces, Collect. Math. 59 (2008), 1–26. https://doi.org/10.1007/BF03191179
E. Markman, The monodromy of generalized Kummer varieties and algebraic cycles on their intermediate Jacobians, J. Eur. Math. Soc. 25 (2023), 231–321. https://doi.org/10.4171/JEMS/1199
P. Deligne, The Hodge conjecture, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/hodge.pdf

7 thms2 active usersReviewed

Number Theory Pure Mathematics·Captain: Lucas

Schinzel's Hypothesis HOpen Problem

Motivation

Almost every classical question about prime values of polynomials is a special case of one statement. Are there infinitely many twin primes? Infinitely many primes of the form $n^2+1$ ? Infinitely many Sophie Germain primes $p$ with $2p+1$ prime? Each asks whether a fixed finite list of integer polynomials takes prime values simultaneously infinitely often. Schinzel's Hypothesis H (A. Schinzel and W. Sierpiński, 1958) is the single conjecture that predicts "yes" in all these cases, subject to the two obvious obstructions: a polynomial that factors cannot be prime infinitely often, and neither can a family whose product is always divisible by some fixed prime.

Timeline.

1837 — Dirichlet proves the degree-one, single-polynomial case: if $\gcd(a,b)=1$ and $a>0$ , then $an+b$ is prime for infinitely many $n$ .
1857 — Bunyakovsky states the single-polynomial case for arbitrary degree. It is open for every fixed polynomial of degree $\ge 2$ ; not one instance, not even $n^2+1$ , is known.
1904 — Dickson states the case of arbitrarily many linear polynomials.
1958 — Schinzel and Sierpiński state Hypothesis H in the generality used here (Acta Arith. 4 (1958), 185–208).
1962 — Bateman and Horn give the conjectural asymptotic count of such $n \le N$ , refining Hypothesis H to a quantitative form (Math. Comp. 16 (1962), 363–367).
1978 — Iwaniec proves that $n^2+1$ has at most two prime factors infinitely often; the sieve barrier that blocks "exactly one" has not been broken.
2004 — Green and Tao prove the analogous simultaneous-prime statement for systems of linear forms of finite complexity, which yields arbitrarily long arithmetic progressions of primes but does not cover Dickson's conjecture in full (the pair $n$ , $n+2$ has infinite complexity).
2013 — Zhang, and then Maynard and Tao, establish bounded gaps between primes, i.e. that some admissible pair $\{n+h_1, n+h_2\}$ is simultaneously prime infinitely often — but the method does not identify which pair.

Hypothesis H itself remains open in every case that is not covered by Dirichlet's theorem.

Setting

Work in the ring $\mathbb{Z}[X]$ of polynomials with integer coefficients. Fix a finite set $\mathcal{F} \subseteq \mathbb{Z}[X]$ of polynomials $f$ , each subject to the Bunyakovsky condition:

$\deg f \ge 1$ ;
the leading coefficient of $f$ is positive;
$f$ is irreducible in $\mathbb{Z}[X]$ .

Irreducibility in $\mathbb{Z}[X]$ is strictly stronger than irreducibility in $\mathbb{Q}[X]$ : it also forces the content of $f$ to be $1$ , ruling out $2X^2+2$ .

Even an irreducible family can be blocked by congruences. The polynomial $X^2+X+2$ is irreducible with positive leading coefficient, yet $n^2+n+2$ is even for every integer $n$ , so it is prime only when it equals $2$ . The family $\mathcal{F}$ therefore also has to satisfy the Schinzel condition: for every prime $p$ there exists an integer $n$ with

p \nmid \prod_{f \in \mathcal{F}} f(n).

Equivalently, no prime is a fixed divisor of the product $\prod_{f\in\mathcal{F}} f$ . A family satisfying both conditions is called admissible.

Target

For an admissible family $\mathcal{F}$ , write

S(\mathcal{F}) \;=\; \{\, n \in \mathbb{N} \;:\; |f(n)| \text{ is prime for every } f \in \mathcal{F} \,\}.

The goal of the mission is Hypothesis H:

\mathcal{F} \text{ admissible} \;\Longrightarrow\; S(\mathcal{F}) \text{ is infinite.}

The milestones are, in order: the linear one-polynomial case (Dirichlet); the reduction of the Schinzel condition to the finitely many primes $p \le \sum_{f\in\mathcal F}\deg f$ ; the necessity of the Schinzel condition; and three specializations of the goal — Bunyakovsky's conjecture, the twin prime conjecture, and Landau's problem on $n^2+1$ — each stated as an implication from the goal statement, so that they can be proved before the goal itself is.

Significance

The result itself. Hypothesis H implies the twin prime conjecture, the Sophie Germain prime conjecture, Landau's conjecture that $n^2+1$ is prime infinitely often, the infinitude of primes in every admissible constellation, and Dickson's conjecture; with Bateman–Horn it also predicts the density of such $n$ . Nothing beyond the degree-one case is known, and the conjecture is the standard yardstick against which sieve-theoretic progress on prime values of polynomials is measured.

Formalizing it. The goal is open, so the mission's deliverable is not a proof of it but a formal, audited statement of it together with a supporting environment: the admissibility predicates, the classical reductions, and machine-checked derivations of the famous corollaries from the goal. Dirichlet's theorem on primes in arithmetic progressions is already formalized in Mathlib, so the linear milestone is a matter of connecting that result to this mission's formulation rather than of new mathematics. The three "H implies …" milestones are provable now, unconditionally, because they are implications; they are also the sharpest available check that the goal statement has been formalized faithfully, since a mis-stated goal will usually fail to yield twin primes.

Difficulty

The obvious first idea — sieve the values $\prod_{f} f(n)$ for $n \le N$ and count survivors — is exactly the idea that fails. Sieve methods lose a constant factor (the parity problem): they can show that $\prod_f f(n)$ has few prime factors infinitely often, but they cannot distinguish "one prime factor" from "two", which is why Iwaniec's $n^2+1$ result stops at $P_2$ . The analytic input that works for degree one — the nonvanishing of Dirichlet $L$ -functions on $\Re s = 1$ — has no known analogue for a polynomial of degree $\ge 2$ , because the relevant counting problem is not governed by characters of a finite abelian group. Milestones 1–3 are elementary or already available in Mathlib; the goal itself is not expected to be resolved here.

Formalization scope

Conventions fixed by the Lean development, and deliberately so:

The family is a finite set of polynomials, so repeated polynomials collapse, and it is allowed to be empty (the goal is then a statement about all of $\mathbb{N}$ , and true).
Primality is asserted of the absolute value $|f(n)|$ as a natural number. Since the leading coefficient is positive and $\deg f \ge 1$ , the values are eventually positive, so this is equivalent to asking for a positive prime value at all large $n$ .
The variable $n$ ranges over $\mathbb{N}$ , not $\mathbb{Z}$ , and "infinitely often" means that the set of such $n$ is infinite.
Irreducibility is irreducibility in $\mathbb{Z}[X]$ (so primitivity is included), and the degree hypothesis is $\deg f \ge 1$ in the sense of the natural-number degree.
The Schinzel condition is stated as a condition on the product over the family, quantified over all primes $p$ — not over $p$ up to a bound; milestone 2 is what reduces it to a finite check.

The statement admits no trivializing reading: the hypotheses are satisfiable (for example $\{X, X+2\}$ and $\{X^2+1\}$ are admissible, as milestones 5 and 6 require one to verify), so the goal is not vacuous, and the conclusion asserts infinitude rather than the existence of a single $n$ .

A complete development needs the admissibility predicates (supplied as the mission's definition bundle), Mathlib's polynomial and modular-arithmetic APIs for the fixed-divisor arguments, and Mathlib's Dirichlet theorem for milestone 1. The definition bundle and milestones 2–3 are reusable for any future mission on Bateman–Horn, Dickson's conjecture, or prime constellations. Contributions of further conditional consequences of the goal (Sophie Germain primes, prime $k$ -tuples, cousin primes) are welcome as additions to the tree.

Selected references

A. Schinzel and W. Sierpiński, Sur certaines hypothèses concernant les nombres premiers, Acta Arithmetica 4 (1958), 185–208. DOI
P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Mathematics of Computation 16 (1962), 363–367. DOI
H. Iwaniec, Almost-primes represented by quadratic polynomials, Inventiones Mathematicae 47 (1978), 171–188. DOI
B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Annals of Mathematics 167 (2008), 481–547. arXiv:math/0404188
J. Maynard, Small gaps between primes, Annals of Mathematics 181 (2015), 383–413. arXiv:1311.4600

8 thms2 active usersReviewed

Completed

Analysis Topology·Captain: Lucas

Rudin PMA IV: ContinuityTextbook

Motivation

Continuity is the hypothesis under which limits may be moved inside a function, and Chapter 4 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) is about what continuity gives once the domain is compact or connected. Three of its theorems are used in nearly every later argument of the book: a continuous function on a compact set has compact image (Theorem 4.14), hence attains its bounds (4.16); a continuous function on a connected set has connected image (4.22), hence takes intermediate values (4.23); and a continuous function on a compact metric space is uniformly continuous (Theorem 4.19) — the $\delta$ can be chosen independently of the point.

The last of these is the chapter's capstone. Uniform continuity is exactly what is needed to prove that continuous functions are Riemann-integrable (Chapter 6), and it is the first place where compactness upgrades a pointwise hypothesis into a global one with a quantitative conclusion.

This mission is the fourth in a series formalizing Rudin Chapters 1–11; it uses the metric topology of Mission II and is a prerequisite for Missions V–VII.

Setting

Let $X, Y$ be metric spaces, $E \subseteq X$ , $f : E \to Y$ , and let $p$ be a limit point of $E$ . Rudin writes $\lim_{x \to p} f(x) = q$ when for every $\varepsilon > 0$ there is $\delta > 0$ with $d_Y(f(x), q) < \varepsilon$ for all $x \in E$ satisfying $0 < d_X(x,p) < \delta$ ; the exclusion of $x = p$ is deliberate, and it is what makes the notion agree with continuity only when $f(p) = q$ (Theorem 4.6). $f$ is continuous at $p$ if the same holds with the condition $0 < d_X(x,p)$ dropped, and continuous if it is continuous at every point.

$f$ is uniformly continuous on $X$ if for every $\varepsilon > 0$ there is a single $\delta > 0$ such that $d_Y(f(p), f(q)) < \varepsilon$ for all $p, q \in X$ with $d_X(p,q) < \delta$ . A real function on $(a,b)$ is monotonically increasing if $x < y$ implies $f(x) \le f(y)$ ; its one-sided limits are written $f(x-)$ and $f(x+)$ , and it has a discontinuity of the first kind at $x$ when both exist but do not agree with $f(x)$ .

Formalization targets

Goal — uniform continuity on compacta (Theorem 4.19)

X \text{ compact metric space},\ f : X \to Y \text{ continuous} \;\Longrightarrow\; \forall \varepsilon > 0\ \exists \delta > 0\ \forall p, q \in X,\ d(p,q) < \delta \Rightarrow d(f(p), f(q)) < \varepsilon .

Milestones

f \text{ continuous at } p \iff \lim_{x \to p} f(x) = f(p) \qquad (4.6)

f \text{ continuous} \iff f^{-1}(V) \text{ open for every open } V \qquad (4.8)

K \text{ compact} \Rightarrow f(K) \text{ compact} \qquad (4.14)

\text{a continuous real } f \text{ on a compact } X \text{ attains } \sup f \text{ and } \inf f \qquad (4.16)

f : X \to Y \text{ continuous bijection, } X \text{ compact} \Rightarrow f^{-1} \text{ continuous} \qquad (4.17)

E \text{ connected} \Rightarrow f(E) \text{ connected} \qquad (4.22)

f(a) < c < f(b) \Rightarrow f(x) = c \text{ for some } x \in (a,b) \qquad (4.23)

f \text{ monotone} \Rightarrow f(x-),\, f(x+) \text{ exist and } f(x-) \le f(x) \le f(x+) \qquad (4.29)

\text{the discontinuity set of a monotone function is at most countable} \qquad (4.30)

Significance

Uniform continuity is the hypothesis that converts local approximation into global approximation with a uniform error bound. In Chapter 6 it is what makes the upper and lower Riemann–Stieltjes sums of a continuous function come together; in Chapter 7 it underlies the equicontinuity of Arzelà–Ascoli; in Chapter 9 it appears again in the estimate of a $C'$ mapping on a compact ball. The extreme value theorem and the intermediate value theorem are the two existence theorems of elementary analysis, and both come from this chapter by combining Chapter 2's compactness and connectedness with continuity.

Theorem 4.30 — a monotone function has at most countably many discontinuities — is the result that makes monotone integrators well behaved in Chapter 6, and it is the first place in the book where a countability argument (Chapter 2) pays off analytically.

Mathlib has continuity, compactness and connectedness in general topological spaces, and most of the milestones can be matched to library results after the statements are put in Rudin's metric form. The formalization value is again in the dictionary: Rudin's punctured-limit definition versus ContinuousWithinAt, and his $\varepsilon$ – $\delta$ uniform continuity versus the library's uniformity-filter definition.

Difficulty

There is no single hard step; the difficulty is in the hypotheses being weaker than they look. In Theorem 4.6 the limit is taken through $E \setminus \{p\}$ , so the equivalence with continuity genuinely needs $p \in E$ and $p$ a limit point; dropping the second hypothesis makes the statement false at isolated points. In Theorem 4.19 the naive proof — pick $\delta_p$ at each point by continuity and take the infimum — fails because the infimum over infinitely many points can be $0$ ; compactness is used to reduce to finitely many, and the factor of two in the radii of the covering balls is essential. Theorem 4.30 requires an injection from the discontinuity set into $\mathbb{Q}$ , built from the gap between $f(x-)$ and $f(x+)$ .

Formalization scope

Conventions fixed by this mission:

Continuity is Mathlib's Continuous, ContinuousOn, ContinuousWithinAt; Rudin's $\lim_{x\to p} f(x) = q$ along $E$ is Filter.Tendsto f (𝓝[E \ {p}] p) (𝓝 q).
Uniform continuity is Rudin.UniformlyContinuous, stated with explicit $\varepsilon$ and $\delta$ as in Definition 4.18, rather than through the uniformity filter.
Limit points are Rudin.IsLimitPoint from the Chapter 2 mission, so the two missions share one notion.
Compactness of the domain in 4.16, 4.17 and 4.19 is the typeclass [CompactSpace X], matching Rudin's phrase "compact metric space"; 4.14 is stated for a compact subset instead, which is the form later missions use.
Monotone functions are MonotoneOn f (Set.Ioo a b); one-sided limits are 𝓝[<] x and 𝓝[>] x filters, and 4.29 also identifies them with the supremum and infimum of the corresponding one-sided images, as Rudin does.

The goal is not vacuous and does not follow by unfolding: uniform continuity fails for continuous functions on non-compact domains (e.g. $x \mapsto x^2$ on $\mathbb{R}$ , or $x \mapsto 1/x$ on $(0,1)$ ), so compactness is doing the work.

Selected references

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 4 (pp. 83–101).

11 thms2 active usersReviewed

Completed

Dynamical Systems Group Theory Topology·Captain: dbenbenn

Brin–Squier: the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints has no free subgroup of rank greater than oneResearch Paper

Motivation

Von Neumann introduced amenability in 1929 in response to the Banach–Tarski paradox: a group is amenable when it carries a finitely additive, translation-invariant probability measure on its subsets, and no amenable group contains a free subgroup of rank $2$ — which is exactly what the paradox needs. The converse is the von Neumann conjecture, and it is false: Ol'shanskii in 1980 and Adyan in 1982 produced finitely generated counterexamples. A finitely presented counterexample was harder, and one candidate stood out — Richard Thompson's group $F$ , finitely presented, with nobody able to decide whether it was amenable.

Brin and Squier attacked it and in 1985 got what they called "half a success": they proved that $F$ , and more generally the group $\mathrm{PLF}(\mathbb{R})$ of piecewise-linear homeomorphisms of the line with finitely many breakpoints, contains no free subgroup of rank greater than $1$ . Whether $F$ is amenable they could not determine, and it is still open today; claimed proofs have appeared in both directions and none has been accepted. Finitely presented counterexamples were eventually found by other routes (Ol'shanskii–Sapir 2002; Lodha–Moore 2016), so $F$ is no longer needed as a candidate. This mission formalizes the half that was settled.

Setting

Let $\mathrm{Homeo}_+(\mathbb{R})$ be the group of orientation-preserving homeomorphisms of the line: the strictly increasing bijections $\mathbb{R}\to\mathbb{R}$ under composition. The support of $f$ is the set of points it moves, $\operatorname{supp} f = \{\,t : f(t)\neq t\,\}$ , an open subset of $\mathbb{R}$ .

A continuous $f$ is piecewise linear when there is a discrete set $B$ of breakpoints with $f$ differentiable off $B$ and $f'$ constant on each component of $\mathbb{R}\setminus B$ ; for finite $B$ this is the same as $f$ being affine on a neighbourhood of every point outside $B$ . Nothing is required at the points of $B$ , so the two affine pieces meeting at a breakpoint may disagree — that is what makes such an $f$ more than an affine map. Write $\mathrm{PL}(\mathbb{R})$ for the piecewise-linear elements of $\mathrm{Homeo}_+(\mathbb{R})$ and

\mathrm{PLF}(\mathbb{R}) = \{\, f \in \mathrm{PL}(\mathbb{R}) : f \text{ has a finite breakpoint set} \,\}

for the subgroup this mission is about. The distinction matters: the goal below holds in $\mathrm{PLF}(\mathbb{R})$ and fails in $\mathrm{PL}(\mathbb{R})$ , where Brin and Squier build free subgroups of rank $2$ by lifting them from the circle. Write $\mathrm{PLF}'(\mathbb{R})$ for the commutator subgroup, which Brin and Squier identify as the elements whose slope at each end is $1$ — an element has slope $a$ at an end when it agrees with a single affine map of slope $a$ on a ray out to that end. Thompson's group $F$ — the piecewise-linear homeomorphisms of $[0,1]$ with dyadic breakpoints and power-of-two slopes — is realized inside $\mathrm{PLF}(\mathbb{R})$ .

Formalization targets

Goal — no two elements generate freely

\text{for } f,g \in \mathrm{PLF}(\mathbb{R}), \quad F_2 \to \mathrm{PLF}(\mathbb{R}),\ a \mapsto f,\ b \mapsto g \quad\text{is never injective.}

Since a free group of rank greater than $1$ contains one of rank $2$ , this is Brin and Squier's Theorem (3.1).

The dichotomy it rests on

G \le \mathrm{PLF}'(\mathbb{R}) \implies G \text{ abelian, or } G \text{ contains a free abelian subgroup of rank } 2.

Their Theorem (3.2), with the conclusion weakened to what the goal consumes. What they prove is infinite rank, which needs the general form of their Lemma (1.2); that general Lemma and the full-strength (3.2) are milestones of their own here. The goal itself only ever uses the rank-two form.

The twenty-four milestones

Thirteen are numbered results of theirs: the support observations (1.1a), (1.1b); Lemma (1.2) in its rank-two case and in its general form; Lemmas (3.4) and (3.5), already formalized and published, entering as references; the commutator facts (2.14a), (2.14b), (2.14c); Theorem (3.2) both as the rank-two dichotomy the goal consumes and at full strength; and Corollary (3.3), likewise in both strengths. Five are piecewise-linear infrastructure the source treats as routine: closure of $\mathrm{PLF}(\mathbb{R})$ under composition and under inverse, the same two for slope $1$ at each end, and finiteness of the number of components of a support. Five more are steps the source asserts without proof — that the line carries no non-fixed periodic points, that a map fixing a set's complement preserves its components, that the iterated images of a pushed-forward interval are pairwise disjoint, that the closure of a commutator's moved set stays inside the union of the two supports (p. 495), and that the derived subgroup of a free group of rank two is non-abelian (p. 494). The last is not from the source at all — that an abelian subgroup of a free group is cyclic, which is what lets the goal finish through Nielsen–Schreier.

Significance

The theorem closes the standard route to proving a group non-amenable. To show a group amenable the classical routes are elementary amenability and subexponential growth, and $F$ is neither elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) nor of subexponential growth, having exponential growth (their Corollary 4.7). To show a group non-amenable the standard route is to exhibit a free subgroup of rank $2$ — the route this theorem closes. $F$ sits in the gap, which is why its status has survived sustained attention.

The result reaches past $F$ . Monod's groups of piecewise projective homeomorphisms are counterexamples to von Neumann's conjecture, and Monod's theorem that they contain no non-abelian free subgroup is, in Monod's words, "a sequacious generalization of the corresponding theorem of Brin–Squier about piecewise affine transformations"; of its own proof that paper says it will "largely follow [Brin–Squier, § 3]".

What formalizing it adds. Mathlib has no piecewise-linear maps and no amenability predicate for groups. This mission builds the piecewise-linear layer: a workable $\mathrm{PLF}(\mathbb{R})$ , its closure properties, and the structure of supports.

Difficulty

The obstruction is bookkeeping across two finiteness facts of different kinds. Finiteness of the breakpoint set is what gives an element slopes at $\pm\infty$ at all, and what makes two elements affine on each side of a common fixed point. Compactness is the other — throughout, $[f,g] = fgf^{-1}g^{-1}$ — and it splits: that the closure of $\operatorname{supp}[f,g]$ is compact needs only slope $1$ at each end, with no piecewise linearity at all, which is why (2.14b) is formalized under a weaker hypothesis than the source's; that the closure stays inside $\operatorname{supp} f \cup \operatorname{supp} g$ is what reaches back to finiteness. Keeping straight which fact does which job is most of the work.

The first idea a newcomer has about (3.2) is the wrong one. Its proof produces a family of commuting elements, and it is not disjointness of supports that makes them commute: only their intersections with one chosen component are disjoint, and commutation is deduced instead from a minimality argument. A proof routed through disjoint supports will not close.

Formalization scope

What the Lean fixes. Elements are order isomorphisms of $\mathbb{R}$ — strictly increasing bijections, automatically homeomorphisms — rather than a homeomorphism type. Composition follows Mathlib's convention $(f\cdot g)(x) = f(g(x))$ , the opposite of the source's right action, so the conjugation identity reads $\operatorname{supp}(fgf^{-1}) = f(\operatorname{supp} g)$ here; getting this backwards states a different theorem that still compiles. A support is the bare moved set, with no closure taken. Piecewise linearity is a finite breakpoint set together with local affineness off it — the set need not be minimal and may be empty. A copy of $\mathbb{Z}^2$ is an injectivity statement about $(m,n)\mapsto u^m v^n$ , not a subgroup isomorphism, and the goal is about a single pair $f,g$ rather than a subgroup. The dichotomy hypothesises slope $1$ at both ends directly, not membership in a derived subgroup — that these coincide is the source's result, and both inclusions are formalized here: (2.14a) gives one, and the identification asserted on p. 493 gives the other. Beyond a workable $\mathrm{PLF}(\mathbb{R})$ , the development needs Nielsen–Schreier, already in Mathlib as subgroupIsFreeOfIsFree: it is what lets an abelian subgroup of a free group be cyclic, and so lets the goal finish without the source's metabelian ending. That ending is formalized too, as Corollary (3.3) together with the p. 494 remark that the derived subgroup of a free group of rank two is non-abelian; the goal simply does not route through it.

One trivializing reading is ruled out. Slope $1$ at both ends is not a compact-support condition — every translation satisfies it — so (3.2) is not secretly a statement about compactly supported maps.

Nothing is built for $F$ specifically, and amenability is not touched. That is the one piece deliberately omitted, and contributions are welcome on it: modelling $F$ and embedding it in $\mathrm{PLF}(\mathbb{R})$ . The piecewise-linear layer is reusable beyond this theorem — Thompson's groups $T$ and $V$ , and piecewise-linear topology generally, need exactly it.

Selected references

M. G. Brin and C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. math. 79 (1985), 485–498, doi:10.1007/BF01388519. Theorem (3.1) is the goal.
J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique 42 (1996), 215–256. Theorem 4.10 and Corollary 4.7.
N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013), 4524–4527, arXiv:1209.5229.
A. Yu. Ol'shanskii and M. V. Sapir, Non-amenable finitely presented torsion-by-cyclic groups, Publ. Math. IHÉS 96 (2002), 43–169, doi:10.1007/s10240-002-0006-7.
Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016), 177–200, doi:10.4171/ggd/347.
V. Guba, Amenability problem for Thompson's group $F$ : state of the art, J. Groups Complex. Cryptol. 15 (2023), arXiv:2305.07113.

32 thms2 active usersReviewed

Analysis Partial Differential Equations Probability·Captain: Lucas

Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper

Motivation

Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical $\Phi^4_3$ model $\partial_t u = \Delta u - u^3 + \xi$ on the three-dimensional torus, the KPZ equation $\partial_t h = \partial_x^2 h + (\partial_x h)^2 - \infty + \xi$ , and the parabolic Anderson model $\partial_t u = \Delta u + u\,\xi$ all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's A theory of regularity structures (Invent. Math. 198 (2014) 269–504, arXiv:1303.5113) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.

The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on $\mathbb{R}^d$ with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.

Setting

Fix a dimension $d$ and a scaling $s = (s_1,\dots,s_d)$ of positive integers, with $|s| = \sum_i s_i$ , and put $\|x\|_s = \max_i |x_i|^{1/s_i}$ . For $\delta > 0$ , a point $x \in \mathbb{R}^d$ and a test function $\varphi$ , the rescaled test function is

(S^{\delta}_{s,x}\varphi)(y) = \delta^{-|s|}\,\varphi\!\left(\frac{y_1-x_1}{\delta^{s_1}},\dots,\frac{y_d-x_d}{\delta^{s_d}}\right).

Write $\mathcal{B}^r_{s,0}$ for the set of test functions supported in $\{\|y\|_s \le 1\}$ whose derivatives up to order $r$ are bounded by $1$ . For $\alpha<0$ , a distribution $\xi$ belongs to the Hölder–Besov space $\mathcal{C}^\alpha_s$ if, on every compact set $K$ , $|\langle \xi, S^{\delta}_{s,x}\eta\rangle| \le C\delta^{\alpha}$ uniformly over $x\in K$ , $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ with $r=-\lfloor\alpha\rfloor$ .

A regularity structure $(A,T,G)$ consists of an index set $A \subseteq \mathbb{R}$ containing $0$ , bounded below and locally finite; a graded vector space $T = \bigoplus_{\alpha\in A} T_\alpha$ with $T_0 \cong \mathbb{R}$ spanned by a unit $\mathbf{1}$ ; and a group $G$ of linear operators on $T$ with $\Gamma a - a \in \bigoplus_{\beta<\alpha}T_\beta$ for $a \in T_\alpha$ , and $\Gamma\mathbf{1} = \mathbf{1}$ . Elements of $T_\alpha$ are "homogeneous of order $\alpha$ ": they are placeholders for objects whose size at scale $\varepsilon$ is $\varepsilon^{\alpha}$ .

A model $(\Pi,\Gamma)$ assigns to each point $x$ a linear map $\Pi_x : T \to \mathcal{D}'(\mathbb{R}^d)$ and to each pair $(x,y)$ an element $\Gamma_{xy}\in G$ , subject to $\Gamma_{xx}=\mathrm{id}$ , $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$ , $\Pi_y = \Pi_x\circ\Gamma_{xy}$ and, locally uniformly, the analytic bounds

|(\Pi_x a)(S^{\delta}_{s,x}\varphi)| \lesssim \|a\|_\ell\,\delta^{\ell}, \qquad \|\Gamma_{xy}a\|_m \lesssim \|a\|_\ell\,\|x-y\|_s^{\ell-m}, \qquad a \in T_\ell,\; m<\ell.

A modelled distribution of order $\gamma$ is a function $f : \mathbb{R}^d \to T_{<\gamma}$ such that on every compact $K$

|||f|||_{\gamma;K} = \sup_{x\in K,\ \beta<\gamma}\|f(x)\|_\beta + \sup_{\substack{x,y \in K,\ \|x-y\|_s\le 1 \\ \beta<\gamma}} \frac{\|f(x)-\Gamma_{xy}f(y)\|_\beta}{\|x-y\|_s^{\gamma-\beta}} < \infty;

the space of these is $\mathcal{D}^\gamma$ , and $\mathcal{D}^\gamma(V)$ if $f$ takes values in a sector $V$ , that is, a graded $G$ -invariant subspace vanishing in degrees below its regularity.

Formalization targets

Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$

With $\alpha = \min A < 0$ and $r$ the order attached to $A$ , for every $f \in \mathcal{D}^\gamma$ with $\gamma>0$ there is a unique distribution $\mathcal{R}f \in \mathcal{C}^\alpha_s$ with

\big|(\mathcal{R}f - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \lesssim \delta^{\gamma} \qquad (x \in K,\ \delta\in(0,1],\ \eta\in\mathcal{B}^r_{s,0}).

The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.

Milestone level — the calculus around the reconstruction operator

The uniqueness clause of Theorem 3.10 in isolation; the existence of a linear reconstruction operator for arbitrary $\gamma \in \mathbb{R}$ (for $\gamma\le 0$ the bound no longer pins it down); Corollary 3.16, improving the regularity of $\mathcal{R}f$ to $\mathcal{C}^\beta_s$ when $f$ takes values in a sector of regularity $\beta$ ; Proposition 3.31, that for $\nu>0$ the action of $\Pi$ on $T_\nu$ is determined by $\Gamma$ and by $\Pi$ in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of $f_1 \in \mathcal{D}^{\gamma_1}(V)$ and $f_2\in\mathcal{D}^{\gamma_2}(W)$ lies in $\mathcal{D}^{\gamma}$ with $\gamma = (\gamma_1+\alpha_2)\wedge(\gamma_2+\alpha_1)$ .

Significance

The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces $\mathcal{D}^\gamma$ carry no information about actual distributions.

Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces $\mathcal{C}^\alpha_s$ that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the $\Phi^4_3$ and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.

Difficulty

The naive construction fails: setting $\mathcal{R}f := \Pi_x f(x)$ for a fixed $x$ is wrong away from $x$ , and the pointwise limit $\lim_{\delta\to0}$ of localisations of $\Pi_x f(x)$ around each $x$ does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling $s$ : one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the $\mathcal{D}^\gamma$ bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for $\gamma>0$ is by contrast short, and is listed as a separate milestone.

Formalization scope

The development commits to the following conventions, fixed in the mission's definition files. Points of $\mathbb{R}^d$ are Fin d → ℝ. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by $0$ to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's $\mathcal{B}^r_{s,0}$ consists of $C^r$ functions; here it consists of smooth ones, which defines the same spaces $\mathcal{C}^\alpha_s$ . The model space is the algebraic direct sum $\bigoplus_{a\in A} T_a$ over the index set, each $T_a$ a real normed space, with $Q_a$ the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces $V_a \subseteq T_a$ ; Hairer's requirement that each $V_a$ admit a complement is automatic in this algebraic setting. The integer $r$ appearing in the model bounds is the smallest one with $\ell > -r$ for all $\ell \in A$ , which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in $\mathcal{C}^\alpha_s$ , and uniqueness simultaneously.

Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on $\mathbb{R}^d$ , the elementary theory of $\mathcal{C}^\alpha_s$ (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.

Selected references

M. Hairer, A theory of regularity structures, Inventiones Mathematicae 198 (2014) 269–504. arXiv:1303.5113, DOI:10.1007/s00222-014-0505-4
T. Lyons, Differential equations driven by rough signals, Revista Matemática Iberoamericana 14 (1998) 215–310. DOI:10.4171/RMI/240
M. Gubinelli, Controlling rough paths, Journal of Functional Analysis 216 (2004) 86–140. arXiv:math/0306433
M. Gubinelli, P. Imkeller, N. Perkowski, Paracontrolled distributions and singular PDEs, Forum of Mathematics Pi 3 (2015) e6. arXiv:1210.2684
Y. Bruned, M. Hairer, L. Zambotti, Algebraic renormalisation of regularity structures, Inventiones Mathematicae 215 (2019) 1039–1156. arXiv:1610.08468

13 thms2 active usersReviewed

Completed

Analysis·Captain: Lucas

Rudin PMA III: Numerical Sequences and SeriesTextbook

Motivation

Chapter 3 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) develops the theory of convergence for sequences and series of numbers: subsequential limits and upper limits, the Cauchy criterion, the comparison, root and ratio tests, power series, summation by parts, and products of series. Its final section answers a question that distinguishes analysis from algebra: an infinite sum is not a sum. For a series that converges only conditionally, the value of the sum depends on the order of the terms, and Riemann's rearrangement theorem (Theorem 3.54) makes the dependence total — by reordering the terms one can prescribe any pair of limit inferior and limit superior for the partial sums, including divergence to $\pm\infty$ .

This mission is the third in a series formalizing Rudin Chapters 1–11. It uses the real and complex number systems of Mission I and the compactness results of Mission II, and it supplies the convergence machinery used by Missions VII and VIII.

Setting

A series $\sum a_n$ is the sequence of partial sums $s_n = a_0 + a_1 + \dots + a_{n-1}$ ; the series converges to $s$ when $s_n \to s$ , and converges absolutely when $\sum \|a_n\|$ converges. The upper limit of a real sequence is $s^{*} = \limsup_{n} s_n$ , taken in the extended real number system $[-\infty, +\infty]$ , and a subsequential limit is a limit of a subsequence there. A rearrangement of $\sum a_n$ is a series $\sum a_{\sigma(n)}$ with $\sigma$ a bijection of the index set onto itself.

The distinction that drives the chapter: for real or complex terms, absolute convergence is equivalent to convergence of $\sum a_{\sigma(n)}$ for every $\sigma$ , to the same sum (Theorem 3.55), whereas mere convergence is not.

Formalization targets

Goal — Riemann's rearrangement theorem (Theorem 3.54)

Let $\sum a_n$ be a series of real numbers which converges but not absolutely, and let $-\infty \le \alpha \le \beta \le +\infty$ . Then there is a rearrangement $\sum a_{\sigma(n)}$ with partial sums $s_n'$ such that

\liminf_{n \to \infty} s_n' = \alpha, \qquad \limsup_{n \to \infty} s_n' = \beta .

Milestones

s^{*} \text{ is a subsequential limit, and } x > s^{*} \Rightarrow s_n < x \text{ eventually; } s^{*} \text{ is unique with these properties} \qquad (3.17)

\textstyle\sum a_n \text{ converges} \iff \forall \varepsilon>0\ \exists N\ \forall m \ge n \ge N,\ \big|\sum_{k=n}^{m} a_k\big| \le \varepsilon \qquad (3.22)

\textstyle\sum_{n\ge 0} x^n = \tfrac{1}{1-x}\ (0 \le x < 1), \text{ divergence for } x \ge 1 \qquad (3.26)

\textstyle\sum n^{-p} \text{ converges} \iff p > 1 \qquad (3.28)

e = \textstyle\sum 1/n! = \lim_n (1 + 1/n)^n \qquad (3.30,\ 3.31)

\alpha = \limsup \|a_n\|^{1/n} < 1 \Rightarrow \text{convergence}, \ \alpha > 1 \Rightarrow \text{divergence} \qquad (3.33)

\text{ratio test} \qquad (3.34)

\text{radius of convergence of } \textstyle\sum c_n z^n \qquad (3.39)

\text{bounded partial sums} + b_n \downarrow 0 \Rightarrow \textstyle\sum a_n b_n \text{ converges} \qquad (3.42)

\text{absolute convergence} \Rightarrow \text{convergence} \qquad (3.45)

\text{Cauchy product: } \textstyle\sum c_n = AB \text{ when } \sum a_n \text{ converges absolutely} \qquad (3.50)

Significance

The rearrangement theorem is the precise statement of why conditional convergence must be handled with care, and it is the reason later chapters insist on uniform or absolute hypotheses before interchanging limit operations: Theorem 3.50 (Mertens) needs absolute convergence of one factor, and the Fourier and Lebesgue theories of Chapters 8 and 11 are built on $L^2$ and $L^1$ convergence rather than pointwise summation. The supporting milestones are the standard convergence tests, which are used constantly in the rest of the book, and the characterization of $\limsup$ , which is the tool that makes the root test and the radius of convergence formula precise.

Mathlib's Summable/HasSum express unconditional summability, which over $\mathbb{R}$ and $\mathbb{C}$ is equivalent to absolute convergence. The conditionally convergent series that this chapter is about are therefore invisible to that API, and the mission works with partial sums directly. Some of the classical tests exist in Mathlib in Summable form and will need restating; the rearrangement theorem itself has to be built.

Difficulty

The goal theorem is a construction, not an estimate: one splits $a_n$ into its positive and negative parts $p_n, q_n$ , observes that $\sum p_n$ and $\sum q_n$ both diverge while $p_n, q_n \to 0$ , and then alternately draws blocks of positive and negative terms to overshoot targets $\beta_m \to \beta$ and undershoot targets $\alpha_m \to \alpha$ . Formalizing the alternating greedy construction requires defining the permutation recursively together with the invariant that every index is eventually used — the bookkeeping, not the analysis, is the hard part. The endpoint cases $\alpha = -\infty$ or $\beta = +\infty$ must be carried through the same construction rather than treated separately.

Formalization scope

Conventions fixed by this mission:

Series convergence is Rudin.SeriesConvergesTo / Rudin.SeriesConverges, defined through Rudin.partialSum a n = ∑_{i<n} a i. Absolute convergence is Rudin.SeriesConvergesAbsolutely. Mathlib's Summable is deliberately not used, since it would collapse the distinction the chapter is about.
Upper and lower limits are taken in EReal via Filter.limsup/Filter.liminf, so $\pm\infty$ are allowed as values of $\alpha$ and $\beta$ in the goal.
Rearrangements are Equiv.Perm ℕ, and the rearranged series is fun k => a (σ k).
Series with complex terms are used where Rudin allows complex terms (3.22, 3.33, 3.34, 3.39, 3.42, 3.45, 3.50); the goal is about real series, as in the book.
The radius-of-convergence milestone is stated as α‖z‖ < 1 and α‖z‖ > 1 rather than ‖z‖ < 1/α, to avoid inversion in EReal.

The goal is not vacuous: conditionally convergent series exist (the alternating harmonic series), so the hypotheses are satisfiable, and the conclusion fixes both limit points exactly rather than merely bounding them.

Selected references

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 3 (pp. 47–78).
Bernhard Riemann, Über die Darstellbarkeit einer Function durch eine trigonometrische Reihe, Abhandlungen der Königlichen Gesellschaft der Wissenschaften zu Göttingen 13 (1867), Section 3.

13 thms2 active usersReviewed

Completed

Analysis Topology·Captain: Lucas

Rudin PMA II: Basic TopologyTextbook

Motivation

Convergence, continuity and integration are all statements about nearness, and Chapter 2 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) isolates the amount of structure needed to talk about nearness: a metric. The chapter's payoff is a single theorem, Heine–Borel (Theorem 2.41), which says that in $\mathbb{R}^k$ — and, as the chapter's examples show, only in spaces resembling it — three very different-looking finiteness conditions coincide: being closed and bounded, admitting finite subcovers, and forcing every infinite subset to accumulate. Nearly every existence theorem in the rest of the book (a continuous function on $[a,b]$ attains its maximum, is uniformly continuous, is Riemann-integrable) is an application of that equivalence.

This mission is the second in a series formalizing Rudin Chapters 1–11. It builds on the number systems of Mission I and supplies the topological input for Missions III–VII.

Setting

A metric space is a set $X$ with a distance $d : X \times X \to \mathbb{R}$ that is positive for distinct points, symmetric, and satisfies the triangle inequality. The neighbourhood $N_r(p)$ is the set of $q$ with $d(p,q) < r$ . A point $p$ is a limit point of $E \subseteq X$ if every neighbourhood of $p$ contains a point of $E$ different from $p$ ; $E$ is closed if it contains all its limit points, open if each of its points has a neighbourhood inside $E$ , and its closure $\bar E$ is $E$ together with its limit points. $E$ is perfect if it is closed and every point of $E$ is a limit point of $E$ , and bounded if it is contained in some neighbourhood.

An open cover of $E$ is a family of open sets whose union contains $E$ ; $K$ is compact if every open cover of $K$ has a finite subcover. A $k$ -cell is a product $\{x \in \mathbb{R}^k : a_j \le x_j \le b_j \text{ for all } j\}$ . Two sets $A, B$ are separated if $\bar A \cap B = A \cap \bar B = \varnothing$ , and $E$ is connected if it is not the union of two nonempty separated sets.

Formalization targets

Goal — Heine–Borel (Theorem 2.41)

For $E \subseteq \mathbb{R}^k$ , the following are equivalent:

\text{(a) } E \text{ closed and bounded} \quad\Longleftrightarrow\quad \text{(b) } E \text{ compact} \quad\Longleftrightarrow\quad \text{(c) every infinite } S \subseteq E \text{ has a limit point in } E .

Milestones

\textstyle\bigcup_n E_n \text{ countable when each } E_n \text{ is} \qquad (2.12)

\{0,1\}^{\mathbb{N}} \text{ is uncountable} \qquad (2.14)

\text{arbitrary unions of open sets, finite intersections of open sets, and the closed duals} \qquad (2.24)

\bar E = E \cup E', \quad \bar E \text{ closed}, \quad \bar E = E \Leftrightarrow E \text{ closed}, \quad E \subseteq F \text{ closed} \Rightarrow \bar E \subseteq F \qquad (2.27)

\sup E \in \bar E \qquad (2.28)

\text{open-cover compactness} \Leftrightarrow \text{compactness} \qquad (2.32)

F \subseteq K,\ F \text{ closed},\ K \text{ compact} \Rightarrow F \text{ compact} \qquad (2.35)

\text{finite intersection property for compact sets} \qquad (2.36)

\text{infinite } E \subseteq K \text{ compact} \Rightarrow E \text{ has a limit point in } K \qquad (2.37)

\text{nested } k\text{-cells have a common point} \qquad (2.39)

\text{every } k\text{-cell is compact} \qquad (2.40)

\text{nonempty perfect } P \subseteq \mathbb{R}^k \text{ is uncountable} \qquad (2.43)

E \subseteq \mathbb{R} \text{ connected} \Leftrightarrow (x,y \in E,\ x<z<y \Rightarrow z \in E) \qquad (2.47)

Significance

Heine–Borel is the bridge between the order completeness of $\mathbb{R}$ established in Chapter 1 and the analytic theorems of Chapters 3–7: the bisection argument that proves $k$ -cells compact is the same argument that produces convergent subsequences (Bolzano–Weierstrass, Theorem 2.42), and compactness is what converts local information into global statements. Theorem 2.43 supplies the standard source of uncountable sets of measure zero — the Cantor set is the running example — which matters again in Chapter 11. Theorem 2.47, characterizing the connected subsets of the line as the order-convex ones, is the topological content of the intermediate value theorem proved in Chapter 4.

Mathlib has an extensive metric-space and compactness library, so much of this chapter exists there in some form. What this mission adds is the explicit correspondence with Rudin's formulations: his open-cover definition of compactness against the library's filter-based IsCompact (a milestone in its own right), his $\varepsilon$ -style limit points against closure, and his $k$ -cells against the library's boxes. The resulting dictionary is what the remaining missions in the series use when they need a compactness argument.

Difficulty

The mathematics is standard, and the difficulty is almost entirely in the translation layer. Two places bite. First, Rudin's compactness quantifies over arbitrary open covers, so the statement is a $\Pi$ -type over families of sets, while Mathlib's IsCompact is a statement about filters; the equivalence is available in the library but only after the cover is presented in the right indexed form. Second, "limit point" in Rudin's sense is not p ∈ closure E: the point must be approached by points of $E$ other than $p$ , so isolated points of $E$ are excluded, and statements such as 2.27(a) and 2.41(c) are false if the two notions are conflated.

Formalization scope

Conventions fixed by this mission:

Metric spaces are Mathlib's [MetricSpace X]; IsOpen, IsClosed, closure, Perfect, IsCompact, Bornology.IsBounded and IsPreconnected are used for Rudin's corresponding notions.
Rudin's limit points are Rudin.IsLimitPoint p E, defined with the explicit $\varepsilon$ and the condition $q \ne p$ , and his open-cover compactness is Rudin.IsCoverCompact.
$k$ -cells are Rudin.kCell k a b inside EuclideanSpace ℝ (Fin k); the case where some $a_j > b_j$ gives the empty set, which is why the nested-cell milestone assumes each cell is nonempty, exactly as Rudin's construction does.
Connectedness is IsPreconnected, which admits the empty set, matching Rudin's convention that a set is connected unless it splits into two nonempty separated pieces.
The Heine–Borel goal is stated as a TFAE list in Rudin's order (a), (b), (c).

The equivalence is not vacuous: all three conditions are satisfied by any $k$ -cell and all three fail for $\mathbb{R}^k$ itself when $k \ge 1$ .

Selected references

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 2 (pp. 24–55).
The mathlib Community, The Lean Mathematical Library, CPP 2020. https://doi.org/10.1145/3372885.3373824

15 thms2 active usersReviewed

Completed

Analysis·Captain: Lucas

Rudin PMA I: The Real and Complex Number SystemsTextbook

Motivation

Every course in analysis begins by fixing what a real number is, because the theorems that follow — the intermediate value theorem, the convergence of monotone bounded sequences, the compactness of closed bounded intervals — are false over the rationals and true over the reals for exactly one reason: the least-upper-bound property. Walter Rudin opens Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) with this point. His Example 1.1 exhibits the gap concretely: the set of rationals $p$ with $p^2 < 2$ has no least upper bound in $\mathbb{Q}$ . Chapter 1 then constructs an ordered field in which no such gap occurs, and derives from that single axiom the archimedean property, the density of $\mathbb{Q}$ , and the existence of $n$ -th roots.

This mission is the first in a series formalizing Rudin Chapters 1–11. It covers the chapter's number-system foundations: the ordering axioms, the real field, the complex field, and euclidean space $\mathbb{R}^k$ .

Setting

An ordered set is a set $S$ with a transitive relation $<$ such that for $x, y \in S$ exactly one of $x < y$ , $x = y$ , $y < x$ holds. If $E \subseteq S$ and there is $\beta \in S$ with $x \le \beta$ for all $x \in E$ , then $E$ is bounded above and $\beta$ is an upper bound. A least upper bound (supremum) of $E$ is an upper bound $\alpha$ such that no $\gamma < \alpha$ is an upper bound. The ordered set $S$ has the least-upper-bound property if every nonempty $E \subseteq S$ that is bounded above has a least upper bound in $S$ .

An ordered field is a field $F$ carrying an order such that $x + y < x + z$ whenever $y < z$ , and $xy > 0$ whenever $x > 0$ and $y > 0$ . Rudin's Theorem 1.19 asserts that an ordered field $\mathbb{R}$ with the least-upper-bound property exists and contains $\mathbb{Q}$ as a subfield; the members of $\mathbb{R}$ are the real numbers. The complex field $\mathbb{C}$ is the set of ordered pairs $(a,b)$ of reals with the usual operations, written $a + bi$ , with $|z| = (z\bar z)^{1/2}$ ; euclidean $k$ -space $\mathbb{R}^k$ is the set of $k$ -tuples with the inner product $x \cdot y = \sum_{j} x_j y_j$ and norm $|x| = (x\cdot x)^{1/2}$ .

Formalization targets

Goal — the real field is the unique complete ordered field (Theorem 1.19)

\text{$K$ an ordered field with the least-upper-bound property} \;\Longrightarrow\; \exists!\, e : K \xrightarrow{\ \sim\ } \mathbb{R} \text{ an order-preserving field isomorphism.}

Existence of such a field is witnessed in Lean by $\mathbb{R}$ itself; what carries the content of Rudin's theorem, and what the goal asks for, is that the least-upper-bound property pins the field down up to a unique isomorphism of ordered fields. Uniqueness of $e$ also gives Rudin's second assertion for free: any embedding of $\mathbb{Q}$ is the canonical one, so $K$ contains $\mathbb{Q}$ as an ordered subfield.

Milestones

\neg\,\exists p \in \mathbb{Q},\ p^2 = 2 \qquad (\text{Example } 1.1)

\text{LUB property} \Rightarrow \text{GLB property, with } \inf B = \sup(\text{lower bounds of } B) \qquad (1.11)

x>0 \Rightarrow \exists n \in \mathbb{N},\ nx > y; \qquad x<y \Rightarrow \exists p \in \mathbb{Q},\ x<p<y \qquad (1.20)

x>0,\ n>0 \Rightarrow \exists!\, y>0,\ y^n = x \qquad (1.21)

|\bar z| = |z|,\quad |zw| = |z||w|,\quad |\operatorname{Re} z| \le |z|,\quad |z+w| \le |z|+|w| \qquad (1.33)

\Big|\sum_{j} a_j \overline{b_j}\Big|^2 \le \sum_j |a_j|^2 \sum_j |b_j|^2 \qquad (1.35)

|x \cdot y| \le |x|\,|y|, \quad |x+y| \le |x|+|y|, \quad |x-z| \le |x-y|+|y-z| \qquad (1.37)

Significance

The least-upper-bound property is the only non-algebraic input to the whole of single-variable analysis, and the chapter shows how much follows from it alone: the archimedean property, which rules out infinitesimals; the density of $\mathbb{Q}$ , which makes approximation arguments possible; and the existence of $n$ -th roots, which repairs precisely the defect exhibited by $\sqrt{2}$ . The uniqueness statement is what licenses the common practice of treating "the" real numbers as a single object regardless of the construction used (Dedekind cuts, as in Rudin's appendix, or Cauchy sequences).

Mathlib already contains $\mathbb{R}$ , $\mathbb{C}$ , and a uniqueness theorem for conditionally complete linearly ordered fields, and several of the milestones are available there in some form. The work this mission asks for is therefore bridging work: stating Rudin's hypotheses in his own terms — an order with the least-upper-bound property as a hypothesis on a set, not as a typeclass whose data includes a chosen supremum operator — and deriving the standard library form from them. That bridge is what later missions in the series reuse.

Difficulty

The individual statements are elementary, and the mathematical difficulty is genuinely low; what makes the chapter non-mechanical in a proof assistant is the mismatch between hypothesis and structure. Mathlib's completeness is packaged as ConditionallyCompleteLinearOrder, a structure carrying sSup and sInf as data; Rudin's is a proposition about an arbitrary ordered field. Turning the proposition into the structure (in order to invoke the library's uniqueness theorem) is the one step where the obvious "just apply the Mathlib lemma" move does not typecheck.

Formalization scope

Conventions fixed by this mission:

Rudin's least-upper-bound property is the predicate Rudin.HasLeastUpperBoundProperty, using Mathlib's IsLUB, BddAbove, lowerBounds; no completeness typeclass is assumed of K.
Ordered fields are [Field K] [LinearOrder K] [IsStrictOrderedRing K], which is exactly Rudin's Definition 1.17.
Order-field isomorphisms are Mathlib's ≃+*o (OrderRingIso), so "unique isomorphism" is stated as ∃ e, ∀ e', e' = e.
$\mathbb{C}$ is Mathlib's ℂ and $|z|$ is the norm ‖z‖; euclidean $k$ -space is EuclideanSpace ℝ (Fin k) with the inner product inner ℝ x y, so Rudin's $\mathbb{R}^k$ facts are norm and inner-product inequalities.
Statements bundling several of Rudin's conclusions (1.33, 1.37) are stated as a single conjunction, in the order the book lists them.

Nothing here is vacuous: the goal quantifies over an arbitrary ordered field satisfying the property, and ℝ itself is such a field, so the hypothesis is satisfiable and the conclusion is not automatic.

Selected references

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 1 (pp. 1–21) and its Appendix.
The mathlib Community, The Lean Mathematical Library, CPP 2020. https://doi.org/10.1145/3372885.3373824

10 thms2 active usersReviewed

Combinatorics Discrete Geometry·Captain: mysticflounder

Superlinear or exact bounds for planar distinct distancesOpen Problem

Superlinear or exact bounds for planar distinct distances

Motivation

This mission asks how restrictions on collinear and cocircular points limit the reuse of distances in the plane. Its central question is Erdős Problem 98: must the minimum number of distances grow faster than the number of points?

Setting

For each positive integer n, let h(n) be the minimum number of distinct positive Euclidean distances determined by an n-point set in the plane with no three collinear points and no four cocircular points. Write D(P) for the number of distinct positive Euclidean distances determined by P.

Target

The mission is to establish a superlinear lower bound, or determine this extremal function exactly. The superlinear target is Erdős Problem 98:

\lim_{n\to\infty} h(n)/n=\infty.

Concretely, for every real A > 0, prove that there is an integer n_A such that every general-position configuration P with |P| = n >= n_A satisfies D(P) > A n. A fixed improvement of the coefficient 1/3, or an additive sublinear improvement above n/3, does not complete this objective.

The alternative completion target is an exact determination of h(n), proved by a universal lower bound and general-position constructions attaining that bound. State the range of n explicitly. An asymptotic estimate or a counterexample to superlinearity alone must be labeled with its actual scope; neither is an exact determination of h(n).

Known bounds and supporting results

A circle centred at a point of P contains at most three other points of P, so D(P) >= (n-1)/3. The following improvements are kernel-checked in Lean 4:

An additive bound: $D(P)\ge n/3+c\,n^{1/4}$ for some absolute c > 0 and all sufficiently large n, the Proved record in this mission. The proof constructs an algebraic curve from a small distinct-distance count, proves pair separation, and constructs intrinsic curve cells to obtain the curve bound D(S) >= c d^(-4/3) |S|^(4/3) for finite samples S on noncircular, irreducible and absolutely irreducible, maximally circular curves of degree d, under |S|^2 >= T d^5 for absolute constants c, T > 0.
$D(P) > (1/3 + 1/130)\,n$ for $n \ge 10^4$ : the Proved record Esgk.numDistances_gt_one_third_add_refined in this mission, with its corollary Esgk.eventually_numDistances_gt_linear_of_le_refined.
$D(P) > (1/3 + 1/40)\,n$ for $n \ge 10^4$ : A. McKenna, Distinct distances in general position: an explicit improvement of the bound n/3 (aiXiv 2610.02806; Zenodo 10.5281/zenodo.23706854). The whole proof, with an exact-rational certificate of 60 cases, is checked in Lean 4 with core axioms only in the public repository as Esgk.numDistances_gt_one_third_add_kappa_image_gap. It is not yet a record on this platform.

So every fixed A <= 1/3 + 1/40 is settled: such a configuration with D(P) <= A n has fewer than 10^4 points. These are supporting results, not the mission's terminal goal. For large n the additive term c n^(1/4) is smaller than the linear gains; the n^(1/5) and n^(1/6) additive targets and their milestones remain supporting results. Resolving the superlinear target would establish a lower bound above every fixed linear coefficient. Determining h(n) exactly would settle the corresponding extremal problem with matching constructions.

Research priorities

Develop an argument that excludes D(P) <= A n for every fixed A > 0. A fixed-coefficient distance-energy gap is one sufficient route.
Improve the linear coefficient further, or find a route whose gain grows with n. Larger constants count as intermediate progress; they must not be reported as a superlinear lower bound.
Investigate constructions and universal lower bounds together when pursuing an exact extremal determination.
Preserve and formalize useful intermediate theorems while keeping their statements and remaining premises explicit.

Formalization scope

Configurations are finite subsets of the Euclidean plane. In the indexed formalization, a configuration is an injective map p : Fin n → ℝ²; write P = image(p) before using D(P). Both general-position hypotheses apply to the image. D(P) counts distinct positive distance values, not pairs or ordered multiplicities. The superlinear quantifier ranges over every real A > 0 and every sufficiently large general-position configuration.

The superlinear target and exact-determination target remain open here. Distinguish conjectures, conditional reductions, audited prose proofs, and kernel-checked Lean results. A completed supporting formalization does not by itself complete this mission.

Selected references

Erdős Problem 98 — extremal question and bibliography.
A. McKenna, Distinct distances in general position: an explicit improvement of the bound n/3, aiXiv 2610.02806, 2026; Lean sources and certificate: mysticflounder/distinct-distances-general-position.
Proof of a fourth-root additive bound for planar distinct distances (dated 2026-09-13; revision 2026-09-14 UTC; Git revision 9e63c1648017becfc717d7e0e4f2877925ace28d; file SHA-256 8ceaca7bad8c07ce3d56f8bf726a0d273ddc41fd300b777fae1eb6525e087d29), manuscript, revised 2026-09-14.
Independent audit of the fourth-root additive bound (dated 2026-09-14 UTC; Git revision 9e63c1648017becfc717d7e0e4f2877925ace28d; file SHA-256 911a06495542d5b4b6cf9f6a41418e4baf4ecd8800b80001b3cc3748f82b0e7b; target SHA-256 8ceaca7bad8c07ce3d56f8bf726a0d273ddc41fd300b777fae1eb6525e087d29), 2026-09-14.
L. Guth, N. H. Katz, On the Erdős distinct distances problem in the plane, Ann. of Math. (2) 181 (2015), 155–190; arXiv:1011.4105.

141 thms2 active users

Completed

Mechanism Design Theoretical Computer Science·Captain: Shuze Chen

Algorithmic Game Theory III: Arrow and Gibbard–SatterthwaiteTextbook

Algorithmic Game Theory III: Arrow and Gibbard–Satterthwaite

Motivation

Before a mechanism can pay anyone, it must decide something — and the impossibility theorems of social choice say that deciding honestly is already hard. Arrow's theorem (1951) showed that any method of aggregating individual rankings into a social ranking that respects unanimity and independence of irrelevant alternatives must be a dictatorship; Gibbard (1973) and Satterthwaite (1975) showed the voting analogue: any non-dictatorial voting rule onto three or more candidates can be strategically manipulated. These two results frame all of mechanism design — they are the reason Chapter 9 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), this mission's source, introduces money and quasilinear utilities immediately after proving them: without transfers, incentive compatibility is an impossibility, not a design constraint.

A timeline: Arrow proved the aggregation impossibility in his 1951 monograph Social Choice and Individual Values; Gibbard (1973) established the manipulability of non-dictatorial voting schemes via game forms, Satterthwaite (1975) independently via a direct argument; the derivation of Gibbard–Satterthwaite as a corollary of Arrow's theorem, which the book follows and this mission adopts as its attack path, is standard since the 1970s.

Setting

Fix a finite set $A$ of alternatives (candidates) and a finite set $\iota$ of voters. A preference is a strict total order on $A$ ; we write the relation as $r(a,b)$ , read " $a$ is strictly preferred to $b$ " (the book writes $b \prec a$ ). A preference profile assigns a preference to each voter. A social welfare function $F$ maps profiles to a social preference; a social choice function $f$ maps profiles to a single chosen alternative (Definition 9.1).

The properties at stake (Definitions 9.2, 9.4, 9.5, 9.7):

$F$ satisfies unanimity if on every profile where all voters hold the identical preference $r$ , the social preference is $r$ .
$F$ satisfies independence of irrelevant alternatives (IIA) if the social preference between $a$ and $b$ depends only on the voters' preferences between $a$ and $b$ .
Voter $i$ is a dictator in $F$ if the social preference always equals $i$ 's; in $f$ , if $f$ always elects $i$ 's top alternative.
$f$ is incentive compatible if no voter, by misreporting, can obtain an outcome they strictly prefer (under their true preference) to the truthful outcome; $f$ is monotone if whenever a single voter's change of vote moves the outcome from $a$ to $a' \ne a$ , that voter ranked $a$ above $a'$ before and $a'$ above $a$ after.
$f$ is onto if every alternative is elected on some profile.

Formalization targets

Goal (capstone) — Theorem 9.8, Gibbard–Satterthwaite

|A| \ge 3,\ f \text{ incentive compatible and onto } A \implies f \text{ is a dictatorship.}

Theorem 9.3 — Arrow

|A| \ge 3,\ F \text{ a social welfare function satisfying unanimity and IIA} \implies F \text{ is a dictatorship.}

Proposition 9.6 — incentive compatibility = monotonicity

f \text{ is incentive compatible} \iff f \text{ is monotone},

with no cardinality or finiteness assumptions: the two properties are quantifier-for-quantifier the same data viewed twice.

Significance

These are the two foundational impossibility theorems of social choice, and the pivot of the whole mechanism-design part of this series: the VCG mission that follows exists because Gibbard–Satterthwaite closes the door on non-trivial strategyproof choice without money. The chapter derives Gibbard–Satterthwaite from Arrow through the top-set extension (Definition 9.9, Lemmas 9.10–9.11), so a solver of the capstone gets Arrow as a stepping stone, not a detour.

Formalizing them produces the platform's first social-choice library: preference profiles as strict total orders, the aggregation vocabulary, and the impossibility pair. Arrow's theorem has been formalized before in other proof assistants (Nipkow's Isabelle formalization, 2009; a Mizar formalization by Wiedijk), which is evidence the statement shapes here are the standard ones — but no Lean 4/mathlib formalization exists, and none on this platform.

Difficulty

The proofs are short on paper and famously slippery in the details. Arrow's proof (the book gives Geanakoplos's pairwise-neutrality route) is a sequence of profile surgeries: each step swaps one voter's ranking of a pair and tracks the social outcome through IIA; the formal cost is constructing the intermediate profiles and proving they remain strict total orders — pure bookkeeping, but a lot of it. The hybrid-profile argument needs, over three or more alternatives, custom orders placing chosen pairs at chosen positions; building these on an abstract finite type is where most of the work lies. For the capstone, the book's route through the top-set extension $\prec^S$ (move $S$ to the top, Definition 9.9) requires proving the extension is again a strict total order (Lemma 9.10) and inherits unanimity, IIA, and non-dictatorship (Lemma 9.11); a solver may equally take any direct proof of Gibbard–Satterthwaite — the statement fixes no route. Proposition 9.6 is a genuine warm-up: unfolding both definitions and rearranging quantifiers.

Formalization scope

Preferences are relations A → A → Prop carrying IsStrictTotalOrder; r a b means " $a$ is strictly preferred to $b$ ", the reverse of the book's $\prec$ — every definition's docstring states this orientation. Aggregators are total functions on all relation-valued profiles; every property quantifies only over genuine preference profiles, so behavior on invalid inputs is irrelevant, and nothing can be smuggled through junk inputs. Unanimity is the book's identical-profile form (Definition 9.2), which together with IIA yields the pairwise form used in proofs. Both alternatives and voters are finite types; |A| ≥ 3 enters as 2 < Fintype.card A. Arrow's theorem carries Nonempty ι, matching the book's setting of $n \ge 1$ voters; it is not needed for truth — with zero voters the identical-profile unanimity is already unsatisfiable over three or more alternatives, so that case is vacuous either way. Gibbard–Satterthwaite deliberately omits it: with zero voters ontoness onto three alternatives is unsatisfiable, and the statement holds vacuously. Dictatorship for choice functions is Definition 9.7 exactly: whenever some alternative is the dictator's unique maximum, it is elected.

Selected references

K. J. Arrow, Social Choice and Individual Values, Wiley, 1951 (2nd ed. 1963). Link
A. Gibbard, Manipulation of voting schemes: a general result, Econometrica 41 (1973), 587–601. DOI
M. A. Satterthwaite, Strategy-proofness and Arrow's conditions, Journal of Economic Theory 10 (1975), 187–217. DOI
J. Geanakoplos, Three brief proofs of Arrow's impossibility theorem, Economic Theory 26 (2005), 211–215. DOI
T. Nipkow, Social choice theory in HOL: Arrow and Gibbard–Satterthwaite, J. Automated Reasoning 43 (2009), 289–304. DOI
N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 9, §9.2. DOI

4 thms2 active usersReviewed

Completed

Algorithmic Game Theory Theoretical Computer Science·Captain: Shuze Chen

Algorithmic Game Theory II: No-Regret Learning and Correlated EquilibriaTextbook

Motivation

Equilibrium concepts are static; play is dynamic. The bridge between the two is regret minimization: simple adaptive rules that, against arbitrary — even adversarial — opponents, perform nearly as well as the best fixed alternative in hindsight. The subject begins with Hannan (1957) and Blackwell (1956), whose consistency theorems predate most of computational learning theory; the modern multiplicative-weights style bounds are due to Littlestone–Warmuth (1994) and Freund–Schapire (1997); the reduction from external to swap regret, and with it the algorithmic route to correlated equilibria, is Blum–Mansour (2005), following Foster–Vohra (1997) and Hart–Mas-Colell (2000). Chapter 4 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Blum and Mansour, is the source text of this mission.

The punchline of the chapter, and of this mission, is that a computationally trivial form of rationality — each player privately running a no-swap-regret algorithm — drives the empirical play of any finite game into an approximate correlated equilibrium (Aumann, 1974). No coordination, no knowledge of the game, no fixed-point computation: the equilibrium concept that Chapter 1 of the series defines through a correlating device is reached by decentralized learning.

Setting

The online model (§4.2): there are $N$ actions. At each time $t$ an online algorithm selects a distribution $p^t$ over actions, as a function of the loss vectors observed so far; then the adversary reveals a loss vector $\ell^t \in [0,1]^N$ and the algorithm suffers $\sum_i p^t_i \ell^t_i$ . Cumulatively, $L_H^T = \sum_{t \le T} \sum_i p^t_i \ell^t_i$ and $L_k^T = \sum_{t \le T} \ell^t_k$ for a fixed action $k$ . The external regret of $H$ is $L_H^T - \min_k L_k^T$ . A modification rule $F : \{1,\dots,N\} \to \{1,\dots,N\}$ rewires the algorithm's play, giving the modified loss $L_{H,F}^T = \sum_t \sum_i p^t_i\, \ell^t_{F(i)}$ ; the swap regret is $L_H^T - \min_F L_{H,F}^T$ over all $N^N$ rules.

A finite game (the vocabulary of Mission I of this series, in loss form): players $\iota$ , finite action sets $S_i$ , cost functions $c_i : \prod_j S_j \to \mathbb{R}$ . A joint distribution $Q$ on action vectors is an $\varepsilon$ -correlated equilibrium (Definition 4.11) if for every player $i$ and every switching rule $F : S_i \to S_i$ ,

\mathbb{E}_{s \sim Q}\big[c_i(s)\big] \;\le\; \mathbb{E}_{s \sim Q}\big[c_i(F(s_i), s_{-i})\big] + \varepsilon.

Formalization targets

Goal (capstone) — Corollary 4.16, explicit form

\forall N, T\ \exists H:\quad \text{swap regret of } H \text{ on every } [0,1]\text{-loss sequence} \;\le\; 2N\sqrt{T \ln N}.

An online algorithm with vanishing per-round swap regret, with the constant the chapter's own route produces.

Theorem 4.6 — Polynomial Weights

L_{PW}^T \;\le\; L_k^T + \eta\, Q_k^T + \frac{\ln N}{\eta}, \qquad Q_k^T = \sum_{t\le T} (\ell^t_k)^2, \quad 0 < \eta \le \tfrac12.

Theorem 4.9 — external regret in constant-sum games

A player with external regret $R$ over $T$ rounds has average loss at most $v_i + R/T$ , where $v_i$ is the game value — no-regret play guarantees the minimax value against any opponent.

Theorem 4.15 — external-to-swap reduction

Any algorithm with external regret $\le R$ on all $[0,1]$ -loss sequences yields one with swap regret $\le N R$ .

Theorem 4.12 — swap regret bounds distance from correlated equilibrium

If every player's swap regret over $T$ steps of mixed play is at most $R$ , the empirical joint distribution is an $(R/T)$ -correlated equilibrium.

Theorem 4.3 — deterministic algorithms fail

Every deterministic algorithm has a $\{0,1\}$ -loss sequence forcing loss $T$ while some action loses at most $\lfloor T/N \rfloor$ : randomization is necessary, not a convenience.

Significance

Correlated equilibrium is the equilibrium concept with a defensible dynamic foundation: Nash equilibria are PPAD-hard to find, but the capstone plus Theorem 4.12 exhibit polynomial-time decentralized dynamics whose empirical play is an $\varepsilon$ -correlated equilibrium after $T = O(N^2 \ln N / \varepsilon^2)$ rounds. Later missions in this series lean on this machinery: the price-of-anarchy chapters bound the cost of no-regret play (not just of exact equilibria), and the routing-game chapter uses precisely the convergence result formalized here.

Formalizing it produces the platform's first online-learning library: the adversarial protocol, regret in both external and swap forms, the multiplicative-weights analysis, and correlated equilibria. The regret vocabulary is directly reusable for the bandit-flavored missions already on the platform. All results are classical, with textbook proofs; the work requested is machine-checked proof, not new mathematics.

Difficulty

The Polynomial Weights bound is a potential-function argument: the total weight $W^t$ falls geometrically with the algorithm's loss and is bounded below by the weight of action $k$ ; the formal work is inequalities for $\ln(1-x)$ on $[0, 1/2]$ and careful bookkeeping of the recursion. The reduction (Theorem 4.15) is the structurally interesting step: the master algorithm runs $N$ copies of the external-regret procedure, feeds copy $i$ the true losses scaled by the master's own probability $p^t_i$ , and — the crux — plays the stationary distribution $p^t = p^t Q^t$ of the column-stochastic matrix assembled from the copies' outputs. Existence of that fixed point is exactly the existence of a stationary distribution of a finite Markov chain, available on this platform as the goal of Markov Chains and Mixing Times I — or provable directly. Theorem 4.12 is an averaging argument, deliberately easy; Theorem 4.3 is an adversary construction; Theorem 4.9 combines the regret bound with the security level the minimax theorem of Mission I supplies, through the opponent's empirical mixture. The capstone is the composition of 4.6 (tuned at $\eta = \min\{\sqrt{\ln N / T}, 1/2\}$ ) with 4.15, plus the arithmetic that turns $N \cdot 2\sqrt{T \ln N}$ into the stated bound.

Formalization scope

An online algorithm is a deterministic function from the observed history (the list of past loss vectors) to the mixed action played next — the standard formal reading of the full-information model; randomization lives in the mixed action, and losses are expected losses. Boundedness of losses ( $[0,1]$ ) is a hypothesis on theorems, never part of a definition. The Polynomial Weights algorithm is defined concretely by its weight recursion, and its learning rate carries the hypothesis $0 < \eta \le 1/2$ : the book writes only $\eta \le 1/2$ , but at $\eta = 0$ the bound's $\ln N / \eta$ term degenerates and the claim is false, so positivity is explicit. Action sets are Fin (n+1), keeping them nonempty. The number of steps $T$ is a known parameter (the book's convention; guess-and-double is out of scope). Correlated equilibria use the switching-rule form of Definition 4.11, over the game vocabulary (IsLottery, IsMixedProfile, profileProb) published with Mission I of this series. In Theorem 4.12 the empirical distribution is the average of product distributions of the played profiles, $T \ge 1$ is required (at $T = 0$ there is no empirical distribution), and costs are not assumed bounded — the averaging is scale-free.

Trivializing readings are ruled out: the existential algorithms in Theorem 4.15 and the capstone are quantified before the loss sequence and the modification rule, so a witness must work uniformly against every adversary — nothing may be chosen with hindsight.

Selected references

A. Blum, Y. Mansour, From external to internal regret, JMLR 8 (2007), 1307–1324. Link
N. Littlestone, M. K. Warmuth, The weighted majority algorithm, Information and Computation 108 (1994), 212–261. DOI
D. P. Foster, R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. DOI
S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000), 1127–1150. DOI
N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 4. DOI

7 thms2 active usersReviewed

Number Theory·Captain: alexcarter

The Erdős–Straus Conjecture (Erdős Problem 242)Open Problem

Egyptian fractions and the Erdős–Straus question

A unit fraction is the reciprocal of a positive integer. The Erdős–Straus conjecture asks whether the particularly simple rational number $4/n$ always admits an expansion with three such terms. Its difficulty lies in obtaining a fixed number of terms for every denominator: general algorithms for Egyptian fractions do not give this three-term guarantee.

The conjecture is open. This mission adopts the exact statement maintained as Erdős Problem 242. It aims to formalize established reductions and provide a precise frontier for further work; it does not present a proof of the universal conjecture.

The historical formulations vary. Erdős’s 1950 paper, pp. 193–195, discusses distinct unit fractions and attributes the conjecture jointly to himself and Straus. His 1961 problem I.32, p. 238, allows positive denominators without specifying distinctness, while the 1979 statement, problem 9, p. 70, explicitly orders distinct denominators. The earliest published discussion may be Obláth’s 1950 paper, submitted in 1948; it attributes the question to Erdős, as explained by Bloom–Elsholtz, pp. 238–239.

The main developments relevant here are:

1950: Obláth’s sufficient condition using a prime divisor of $n+1$ congruent to $3$ modulo $4$ .
1965–1969: Yamamoto’s congruence analysis and Mordell’s exposition reduce the remaining prime cases to six classes modulo $840$ .
1970–1971: Vaughan bounds the density of possible exceptions; Terzi develops a stronger congruence sieve modulo $120120$ .
2013–2022: Elsholtz–Tao analyze representation counts and soluble polynomial congruences; Bloom–Elsholtz give an explicit equivalent covering formulation.
2025: Computational verification is reported through $10^{18}$ . Pomerance–Weingartner study the more general Erdős–Straus–Schinzel problem, including quantitative dependence on a variable numerator.

The exact property

For a natural number $n$ , write $\mathrm{IsErdosStraus}(n)$ for the following literal property:

\exists x,y,z\in\mathbb N,\qquad 1\le x<y<z,\qquad \frac4n=\frac1x+\frac1y+\frac1z.

Every fraction is evaluated in $\mathbb Q$ . The predicate contains only these witnesses, inequalities, and equality. The required range of the conjecture is $n>2$ ; distinctness is part of the mathematical target. In particular, the prime $2$ cannot simply be imported from a formulation permitting repeated denominators. The boundary value $n=3$ is included, with denominators $1,4,12$ .

Formalization targets

The unresolved root goal is

\forall n\in\mathbb N,\quad n>2\Longrightarrow\mathrm{IsErdosStraus}(n).

The supporting milestones concern established mathematics. Denominator clearing relates the rational equation to $4xyz=n(yz+xz+xy)$ under strict positivity. Positive scaling transports a solution for $n$ to one for $kn$ while preserving the strict order. An explicit even-number family supplies the case needed for the prime reduction.

The elementary families cover $3\mid n$ , $n\equiv2\pmod3$ , $n\equiv3\pmod4$ , and $n\equiv5\pmod8$ , with the displayed witnesses and their integrality and strict ordering recorded in separate statements. Together with the even case, they solve every $n>2$ outside $1\pmod{24}$ . The useful reduction is an equivalence between the root goal and its restriction to primes $p\equiv1\pmod{24}$ ; the ordinary prime reduction is also stated separately. The classical scaling and residue observations are discussed in Bloom–Elsholtz, p. 239.

Obláth’s milestone says that $\mathrm{IsErdosStraus}(n)$ holds for $n>2$ whenever $n+1$ has a prime divisor $q\equiv3\pmod4$ . This condition is explicitly recorded in the introduction of Pomerance–Weingartner, which identifies the original Obláth reference. The exact distinctness requirement is retained in this mission.

The Mordell–Yamamoto milestone asks for a decomposition for every prime $p>2$ satisfying

p\bmod840\notin\{1,121,169,289,361,529\}.

The actual existence claim is the theorem to prove. It has no hypothesis asserting that these classes are covered. Yamamoto’s original paper, §§3–4, pp. 42–46, supplies the congruence framework and prints this residual list. The same list appears in the current Erdős Problems record. The list printed on p. 239 of Bloom–Elsholtz instead contains $49$ and omits $529$ ; that discrepant list is not used here. The historical papers often permit repeated denominators, so producing distinct ordered witnesses is an explicit part of the formalization obligation.

What these results provide

The elementary infrastructure gives reusable certificates and transports for exact rational decompositions. The reductions identify a mathematically meaningful remaining domain without assuming the conjecture. Completion of the modulo- $840$ milestone would leave the prime cases in its six residual classes as the classical research frontier; those classes are not asserted to consist of counterexamples.

Later targets include Terzi’s 1971 sieve, whose publisher abstract reports 198 residual classes modulo $120120$ , and Vaughan’s density theorem, bounding the exceptional count by $X\exp(-c(\log X)^{2/3})$ for a positive constant $c$ . Neither is a core Lean statement in this draft. No unaudited list of 198 classes is supplied.

Elsholtz–Tao provide counting results and a classification of polynomially soluble congruences. Bloom–Elsholtz, Theorem 1, pp. 239–240, characterize their conjecture by coverage of all primes by classes

-a/c\pmod{4acd-1}\quad(a,c,d\ge1),

or

-(4c^2d+1)/k\pmod{4cd}\quad(c,d,k\ge1,\ k\mid4c^2d+1).

Here division by $c$ denotes a modular inverse; division by $k$ is exact integer division. The authors are Bloom and Elsholtz, not Bradford and Elsholtz. This is a later formalization target: an initial core theorem is not included until the translation between that paper’s denominator convention and the present strict convention is separately formalized. Pomerance–Weingartner address growing numerators in the generalized problem; their exceptions are not counterexamples to the fixed numerator $4$ conjecture.

The remaining difficulty

Congruence identities prove infinite families only when the identities and their arithmetic hypotheses are established for arbitrary parameters. Checking finitely many representatives with a search program does not prove that all future values in an arithmetic progression work. Density estimates also allow an exceptional set and therefore do not settle the universal statement.

The current record cites Mihnea–Bogdan (2025) for computational verification through $10^{18}$ . This is reported computational evidence, not a Lean-certified theorem in this mission. No universal conclusion or periodicity assertion is inferred from it.

Formalization scope

The development uses natural-number denominators, exact rational arithmetic, integer polynomial identities, divisibility, primality, and natural-number remainders. Definitions are transparent. The root is not hidden in a typeclass, structure field, certificate, or extra assumption, and its quantifier is not bounded. The existing Google DeepMind transcription is a statement reference, not an imported proof.

The draft targets Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 with Lean 4.33.1. Every proposed statement has been locally elaborated and supplied with an independent read-back. Statement elaboration with sorry is not proof verification. The accompanying local proof audit distinguishes the proved supporting results from the open root and the remaining modulo- $840$ formalization task.

Selected references

Erdős, Az … egyenlet egész számú megoldásairól, Mat. Lapok 1 (1950), 192–210; original scan.
Erdős–Graham, Old and New Problems and Results in Combinatorial Number Theory (1980), chapter IV; author’s institutional scan.
Obláth, Sur l’équation diophantienne $4/n=1/x_1+1/x_2+1/x_3$ , Mathesis 59 (1950), 308–316; bibliographic record, also cited in Pomerance–Weingartner.
Yamamoto, On the Diophantine Equation $4/n=1/x+1/y+1/z$ , Mem. Fac. Sci. Kyushu Univ. A 19 (1965), 37–47; original paper.
Mordell, Diophantine Equations, Academic Press (1969), chapter 30, pp. 287–290; publisher record.
Terzi (1971), Vaughan (1970), Elsholtz–Tao (2013), Bloom–Elsholtz (2022), Mihnea–Bogdan (2025), and Pomerance–Weingartner (2025/2026): primary sources linked at their statements above.

15 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Probability·Captain: burkh4rt

The Bunkbed Conjecture is FalseResearch Paper

Motivation

Let $G=(V,E)$ be a finite connected graph. In Bernoulli bond percolation each edge is independently retained with probability $P$ and deleted otherwise, and one writes $\mathbb{P}_P[u \leftrightarrow v]$ for the probability that vertices $u$ and $v$ lie in the same component of the resulting random subgraph. Comparing such connection probabilities is a basic and genuinely hard problem: computing them exactly is $\#\mathsf{P}$ -hard.

The bunkbed graph is built from two copies of $G$ , joined by vertical edges called posts above a chosen set $T \subseteq V$ of transversal vertices. Percolation is performed on the two copies while every post is retained. Writing $v$ for a vertex in the lower copy and $v'$ for its counterpart upstairs, Kasteleyn conjectured in 1985 that being connected within a level is always at least as likely as crossing between levels.

The conjecture is intuitively compelling — crossing levels appears to require "using up" a post — and it resisted proof for forty years. A short timeline:

1985 — Kasteleyn formulates the conjecture; it is recorded as Remark 5 of van den Berg–Kahn (2001), which is how the source cites it.
Positive results accumulate for special cases: wheels, complete graphs, complete bipartite graphs, graphs symmetric with respect to an automorphism exchanging $u$ and $v$ , one or two transversal vertices, and in the $P \uparrow 1$ limit.
2024 — Hollom refutes the $3$ -uniform hypergraph analogue. This alone does not settle the graph case: it is impossible to simulate a single $3$ -hyperedge by bond percolation on a gadget graph.
2025 — Gladkov, Pak and Zimin disprove the conjecture outright, with an explicit counterexample and without computer assistance.

Section 7 of the source is a candid account of a large-scale machine-learning-guided search that failed to find a counterexample, and of why the problem is unusually ill-suited to experimental testing.

Setting

Fix a finite graph with vertex set $V$ and edge set $E$ , and a retention function $w : E \to [0,1]$ (the uniform case is $w \equiv P$ ). A configuration is a subset $S \subseteq E$ of open edges, occurring with probability

\mathbb{P}(S) \;=\; \prod_{e \in S} w(e) \prod_{e \in E \setminus S} \bigl(1 - w(e)\bigr),

and $\mathbb{P}[u \leftrightarrow v]$ is the total probability of those $S$ for which $u$ and $v$ are connected in $(V, S)$ .

Given $T \subseteq V$ , the bunkbed graph has vertex set $V \times \{0,1\}$ . Its edges are a copy of $E$ in each level together with a post $\{(t,0),(t,1)\}$ for every $t \in T$ . In bunkbed percolation the two level-copies are percolated independently while all posts are retained; $\mathbb{P}^{\mathrm{bb}}$ denotes the resulting connection probabilities.

Formalization targets

Goal — the bunkbed conjecture is false

\neg\;\Bigl(\forall\,G \text{ connected},\ \forall\,T \subseteq V,\ \forall\,0<P<1,\ \forall\,u,v \in V:\quad \mathbb{P}^{\mathrm{bb}}_P[u \leftrightarrow v] \;\ge\; \mathbb{P}^{\mathrm{bb}}_P[u \leftrightarrow v'] \Bigr)

Supporting target — the explicit counterexample (Theorem 1.2)

\exists\, G,\ |V| = 7{,}222,\ |E| = 14{,}442,\ |T| = 3,\ \exists\, u,v:\qquad \mathbb{P}^{\mathrm{bb}}_{1/2}[u \leftrightarrow v] \;<\; \mathbb{P}^{\mathrm{bb}}_{1/2}[u \leftrightarrow v']

Supporting target — hyperedge simulation (Lemma 4.1)

For the gadget $G_n$ on $n+1$ vertices,

P_{abc}\,P_{a|b|c} \;-\; P_{ab|c}\,P_{ac|b} \;>\; \Bigl(n\tfrac{1-P}{1+P} - 1\Bigr) P_{a|bc}.

Significance

The result itself. A forty-year-old conjecture in percolation theory is false, and prior positive results are thereby sharpened rather than superseded: it becomes interesting to delimit exactly which families of graphs do satisfy the inequality. The refutation also settles the Counting, Weighted, Alternative and Computational variants listed in §8.1, and shows the random-cluster analogue cannot be pushed from $q=2$ down to $q=1$ .

Formalizing it. Nothing here is open; the mission produces machine-checked versions of published results, and as a by-product the first percolation theory in Lean. Mathlib currently contains no percolation of any kind — no connection probabilities, no bunkbed graph, no hypergraph percolation. That infrastructure is reusable far beyond this mission. The source itself notes (§8.2) that its central combinatorial lemma was independently verified by computer; a formal proof would replace that check with a certificate.

Difficulty

The obvious approach — exhibit a small graph and compute both probabilities — is hopeless, and the source explains why at length. A graph with $m$ edges has $2^m$ configurations; for the counterexample here the probability gap is on the order of $10^{-4331}$ , so no sampling argument can detect it, and exact enumeration is out of reach. Section 7 records a substantial computational search that found nothing and, in hindsight, could not have.

The proof is instead structural, and its difficulty is concentrated in one place. Hollom's refutation of the hypergraph version cannot be transferred directly, because a single $3$ -hyperedge cannot be simulated by bond percolation on any gadget graph. The source's answer is to prove a robust version of Hollom's lemma (Lemma 3.3) which survives the inexact simulation that gadget graphs do provide, and this robustness is what Lemma 4.1's inequality quantifies. Lemma 3.3 is proved by constructing a weight-preserving involution on a refined configuration space — the technical heart, and the milestone a solver should expect to spend the most effort on.

Formalization scope

The development commits to the following conventions.

Everything is finite and rational-valued, hence computable: connection probabilities are ℚ and evaluate by #eval, and small instances close by decide.
A graph is given by an explicit edge Finset and realised through SimpleGraph.fromEdgeSet; connectivity is Mathlib's SimpleGraph.Reachable.
Percolation is a sum over the powerset of the edge set, weighted as displayed above, of a reachability indicator. Edge weights are per-edge (Sym2 V → ℚ), since the gadget $G_n$ genuinely needs two different weights: its spokes are retained with probability $1-P$ and its path edges with probability $P$ .
In the bunkbed, level 0 is the lower copy; posts over T are unconditionally present and are not percolated. The two levels are percolated independently.
⚠️ Planarity is omitted from the goal. Theorem 1.2 asserts the counterexample is planar, and Mathlib has no notion of a planar graph — no IsPlanar, no Euler formula, no Kuratowski. Building one is a larger project than this mission. The formalized statement of Theorem 1.2 is therefore strictly weaker than the published one, and the goal is instead the negation of the conjecture, which is exactly the source's own "In particular, the BBC is false." Contributions adding planarity are welcome and would strengthen the milestone.
Ruling out a trivializing reading: the conjecture must be negated as stated, over all connected graphs, transversal sets and $0<P<1$ . Weakening it to a fixed graph, or to $P \in \{0,1\}$ , or dropping connectivity, would make the refutation vacuous.

Infrastructure. Mathlib supplies SimpleGraph, boxProd, Reachable with a DecidableRel instance, fromEdgeSet, edgeFinset and Finset.powerset. It supplies no percolation, so this mission ships two definition files: Bernoulli bond percolation with the bunkbed construction and the five triple-partition probabilities, and hypergraph percolation with Hollom's hypergraph and the Wierman–Ziff five-state model. One known gap: Mathlib's Reachable decision procedure enumerates walks and is far too slow to evaluate the $64$ -configuration check of Lemma 3.1 by decide. A solver will want a linear-time reachability procedure together with a proof that it agrees with Reachable; that is itself a worthwhile reusable contribution.

Selected references

J. van den Berg and J. Kahn, A correlation inequality for connection events in percolation, Ann. Probab. 29 (2001), 123–126 — Kasteleyn's conjecture appears as Remark 5.
T. Hollom, A new proof of the bunkbed conjecture in the $p \uparrow 1$ limit, Discrete Math. 347 (2024), 113711.
T. Hollom, The bunkbed conjecture is not robust to generalisation, arXiv:2406.01790 (2024).
T. Hutchcroft, P. Nizić-Nikolac, A. Kent, The bunkbed conjecture holds in the $p \uparrow 1$ limit, Comb. Probab. Comput. 32 (2023), 363–369.
N. Gladkov, I. Pak, A. Zimin, The bunkbed conjecture is false, Proc. Natl. Acad. Sci. USA 122 (2025), no. 24, e2420725122. doi:10.1073/pnas.2420725122; preprint arXiv:2410.02545.
J. C. Wierman and R. M. Ziff, Self-dual planar hypergraphs and exact bond percolation thresholds, Electron. J. Combin. 18 (2011).
G. R. Grimmett, Percolation, 2nd ed., Springer, 1999.

38 thms2 active usersReviewed

Completed

Algebraic Topology Quantum Error Correction Quantum Information·Captain: Rui Chao

Counterexamples to the Zeng–Pryadko Homological-Distance ConjectureResearch Paper

Background and main question

The tensor product of chain complexes is a basic construction in homological algebra and in the theory of quantum CSS codes. If $A$ and $B$ are finite based chain complexes over a finite field, their tensor product is graded by total degree,

(A\otimes B)_j=\bigoplus_{i=0}^{j} A_i\otimes B_{j-i}.

Each complex carries a basis-dependent homological distance: $d_j(A)$ is the least Hamming weight of a degree- $j$ cycle that is not a boundary, with $d_j(A)=\infty$ when the degree- $j$ homology vanishes. A natural candidate for the distance of the tensor product is therefore

m_j(A,B)=\min_{0\le i\le j} d_i(A)d_{j-i}(B).

Every nonzero pair of homology classes in complementary degrees gives a pure-tensor class of the corresponding product weight, so one always has $d_j(A\otimes B)\le m_j(A,B)$ . The substantive question is whether this upper bound is always sharp.

In the preprint Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates, posted in 2018 and subsequently published in Physical Review Letters, Zeng and Pryadko proved that the bound is sharp when one factor is a binary one-complex. Their exact formula is Eq. (13) of the arXiv version and is the capstone theorem of the Prove2Me mission Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates. The present formalization is a direct sequel: it retains the same definitions and degree conventions while examining what happens when the one-complex restriction is removed.

Zeng and Pryadko later considered arbitrary finite chain complexes over arbitrary finite fields in Minimal distances for certain quantum product codes and tensor products of chain complexes, published in 2020. In the corresponding arXiv preprint, Conjecture 18 asserts the unrestricted equality

d_j(A\otimes B)=m_j(A,B).

The conjecture is appealing because it would make tensor-product distance completely compositional: the degreewise distances of the two factors would determine the distance of their product. The obstruction is that a homology class in $A\otimes B$ need not have a minimum-weight representative supported in a single bidegree. A representative spread across several summands of the total complex can be lighter than every pure-tensor representative. The purpose of this formalization is to turn that observation into a concrete, machine-checked counterexample to Conjecture 18 while preserving the valid one-complex theorem as a sharply delimited special case.

The counterexample mechanism

The common foundation is recorded in the Prove2Me entry Based binary chain complexes and homological distance. In particular, the boundary in degree $j$ is a map $\partial_j:A_j\to A_{j-1}$ , and

d_j(A)=\inf\{\operatorname{wt}(x):x\in\ker\partial_j,\ x\notin\operatorname{im}\partial_{j+1}\}.

The one-complex result is separately available as Eq. (13) — Exact distance with a one-complex. The construction below uses exactly the same notion of distance, but both tensor factors are genuine three-term complexes.

Begin with binary CSS check maps

H_X:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_X}, \qquad H_Z:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_Z},

assumed surjective and satisfying $H_XH_Z^T=H_ZH_X^T=0$ . Suppose there are logical vectors $x,z\in\mathbb F_2^n$ such that

H_Zx=0,\qquad H_Xz=0,\qquad x\cdot z=1.

The check maps determine two dual three-term complexes

A:\quad \mathbb F_2^{r_X}\xleftarrow{H_X}\mathbb F_2^n \xleftarrow{H_Z^T}\mathbb F_2^{r_Z}, \qquad B:\quad \mathbb F_2^{r_Z}\xleftarrow{H_Z}\mathbb F_2^n \xleftarrow{H_X^T}\mathbb F_2^{r_X}.

Their degree-two tensor space has three bidegree summands, corresponding to $(2,0)$ , $(1,1)$ , and $(0,2)$ . Under the natural matrix identifications, consider the element whose three blocks are

(I_{r_Z},I_n,I_{r_X}).

The CSS orthogonality relations make this element a cycle. Its pairing with the chosen logical vectors certifies that it is not a boundary. Its Hamming weight is exactly $r_Z+n+r_X$ , whereas the componentwise candidate in degree two reduces to

m_2(A,B)=d_1(A)d_1(B).

Consequently, any CSS datum satisfying

r_Z+n+r_X<d_1(A)d_1(B)

produces the strict inequality $d_2(A\otimes B)<m_2(A,B)$ . For orientation, a binary quantum Golay CSS presentation with parameters $[[23,1,7]]$ has $r_X=r_Z=11$ , giving the numerical comparison $45<49$ . The formal proof must supply an explicit CSS instance and verify its algebraic and distance properties, rather than relying on the parameter notation alone.

Formalization objectives

The first milestone proves the general certificate: for every CSS datum satisfying the hypotheses above, the element $(I_{r_Z},I_n,I_{r_X})$ is a nontrivial degree-two cycle of weight $r_Z+n+r_X$ , and the componentwise minimum is $d_1(A)d_1(B)$ .

The second milestone constructs and verifies one explicit CSS datum for which $r_Z+n+r_X<d_1(A)d_1(B)$ . This is the step that turns the general mechanism into an actual counterexample.

The capstone packages the construction as the direct existential statement

\exists\,A,B\qquad d_2(A\otimes B)<\min_{0\le i\le 2}d_i(A)d_{2-i}(B).

Thus the final theorem is not conditional on the existence of suitable code data: it exhibits finite based binary chain complexes for which the equality proposed in Conjecture 18 fails.

Relation to prior work

The counterexample concerns only the unrestricted passage from a one-complex factor to two arbitrary bounded complexes. It does not conflict with Zeng and Pryadko's Eq. (13), whose one-complex hypothesis rules out the three-bidegree interaction used here.

The broader literature also indicates why additional structure matters. Bravyi and Hastings introduced homological-product codes and analyzed logical representatives in product constructions; Audoux and Couvreur developed tensor products of CSS codes through chain-complex methods. More recently, Akhmechet et al. discussed the Zeng–Pryadko conjecture in the structured setting of complexes derived from Khovanov homology, while Berthusen et al. restated it as Conjecture 5.1 in their study of automorphism gadgets. Golowich and Guruswami obtained strong distance guarantees for iterated homological products under expansion and local-testability hypotheses. These results are compatible with the proposed counterexample: they concern special families or impose hypotheses that are absent from Conjecture 18.

Besides settling the unrestricted statement, the formalization isolates a reusable obstruction. It shows precisely how a low-weight class assembled across several bidegrees can evade a formula based only on the degreewise distances of the factors. This distinction should help guide corrected formulations in which an exact product formula, or a useful lower bound, is recovered from additional geometric, expansion, or local-testability assumptions.

The main formal issues are mathematically substantive rather than presentational: the proof must respect the endpoint conventions for the boundary maps, distinguish a cycle from a non-boundary, compare finite weights with $\infty$ -valued distances, and verify a concrete strict-gap instance. Making each of these points explicit is especially important here, because an indexing shift or a merely conditional existence statement would no longer constitute a refutation of the conjecture as stated.

References

W. Zeng and L. P. Pryadko, Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates, Physical Review Letters 122, 230501 (2019); arXiv:1810.01519 (2018), Eq. (13).
W. Zeng and L. P. Pryadko, Minimal distances for certain quantum product codes and tensor products of chain complexes, Physical Review A 102, 062402 (2020); arXiv:2007.12152, Conjecture 18.
S. Bravyi and M. B. Hastings, Homological Product Codes, STOC 2014; arXiv:1311.0885.
B. Audoux and A. Couvreur, On tensor products of CSS codes, Annales de l'Institut Henri Poincaré D 6 (2019); arXiv:1512.07081.
R. Akhmechet et al., Khovanov homology and quantum error-correcting codes, arXiv:2410.11252 (2024).
N. Berthusen et al., Automorphism gadgets in homological product codes, arXiv:2508.04794 (2025).
L. Golowich and V. Guruswami, Quantum LDPC Codes of Almost Linear Distance via Iterated Homological Products, CCC 2025; full version.

6 thms2 active usersReviewed

Completed

Complexity Theory Quantum Information·Captain: Goku

Shallow Quantum Circuits and Causal ConesTextbook

Motivation

A quantum circuit of depth $d$ built from gates of fan-in at most two cannot let an output wire depend on more than $2^d$ input wires. The argument is folklore and takes a paragraph on paper: the causal cone of the measured wire grows by at most a factor of two per layer. Formalizing it exposes a subtlety that the paper argument hides, and that is what this mission is about.

The subtlety

Define the backward cone step of a wire set $S$ through a layer $l$ by adjoining the support of every gate of $l$ that meets $S$ . There is a choice here: test each gate against the incoming set $S$ , or against the partially accumulated cone. Testing against the accumulator over-approximates, and the doubling bound fails. Testing against the incoming set gives the bound — but is only correct when the gates within a layer act on pairwise disjoint wires.

Without that hypothesis (LayerOk) the semantic statement is false, and the counterexample is small: on three wires, the single layer [cnot 2 1, cnot 1 0] has cone $\{0,1\}$ around wire $0$ , yet wire $0$ ends up holding $x_0 \oplus x_1 \oplus x_2$ . So the cone under-approximates the true dependence. This mission's development carries LayerOk throughout, and the counterexample is recorded in the source.

What is formalized

Layered circuits over $\{H, S, T, \mathrm{CNOT}\}$ on $n$ wires, with states as amplitude functions on bit-strings and no tensor products anywhere. On top of that:

the combinatorial half — one layer at most doubles the cone, hence $|\mathrm{cone}| \le 2^{d}\,|S|$ ;
norm preservation, so that acceptProb is a genuine probability in $[0,1]$ ;
the semantic half — inputs agreeing on the causal cone of the output wire are accepted with equal probability.

The semantic half is proved in the Heisenberg picture. The measurement observable is conjugated backwards through the circuit and its support tracked: a gate meeting the support enlarges it by that gate's own wires, and a gate missing it commutes with the observable and cancels against its own adjoint. That cancellation is the reason the non-cascading cone step is correct, and it is why unitarity of the gate set is needed at the $2^n$ -dimensional level rather than gate by gate. Supporting this is a small reusable algebra of local operators: locality is monotone, closed under adjoint and product, and disjointly supported operators commute.

The frontier

The published depth bound assumes each input wire lies in the syntactic cone of the output. That is weaker than saying the wire matters. Milestone 1 asks for the semantically honest version, stated in terms of genuine functional dependence; the bridge is the semantic cone theorem already in the development.

Beyond that, the natural continuations are the same argument for fan-in- $k$ gates ( $|\mathrm{cone}| \le k^{d}$ ), for geometrically local circuits where cone growth is linear rather than exponential, and ultimately the Bravyi–Gosset–König separation $\mathrm{QNC}^{0} \not\subset \mathrm{NC}^{0}$ — which needs machinery (non-local games, magic squares) that this development deliberately does not build.

9 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: Shuze Chen

Dynamic Programming and Optimal Control VI: Lookahead and RolloutTextbook

Motivation

When exact dynamic programming is intractable, practice runs on approximations: one-step and multistep lookahead with a cost-to-go surrogate, open-loop feedback control, and rollout — the algorithm that improved backgammon programs and became a conceptual ancestor of Monte-Carlo tree search and modern policy improvement schemes. Chapter 6 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) gives the basic guarantees: performance bounds for limited lookahead (Props. 6.3.1–6.3.2), superiority of open-loop feedback control over open-loop control (Prop. 6.2.1), and the cost-improvement theory of rollout on discrete deterministic problems (Props. 6.4.1–6.4.3). These are the theorems that make "approximate DP" more than a heuristic.

Setting

Two frameworks. For the stochastic bounds (§6.2–6.3): the basic finite-horizon model of Mission I of this series (BertsekasDPModel), its policy cost recursion, and the open-loop cost of a fixed control sequence (BertsekasDPOpenLoopCost). For rollout (§6.4.1): a graph search problem — a finite digraph with destination set and terminal costs $g(i)$ on destinations (BertsekasGraphSearch); a base heuristic $\mathcal{H}$ producing from every node a path to a destination (BertsekasBaseHeuristic), with projection $p(i)$ and heuristic cost $H(i) = g(p(i))$ ; the rollout algorithm $R\mathcal{H}$ repeatedly moves to a neighbor $j$ minimizing $H(j)$ (BertsekasIsRolloutRun). $\mathcal{H}$ is sequentially consistent if its paths have the tail property (Def. 6.4.1), sequentially improving if $\min_{j \in N(i)} H(j) \le H(i)$ (Def. 6.4.2).

Target

For sequentially improving $\mathcal{H}$ and any terminating rollout run $(i_1, \dots, i_{\bar m})$ :

g(i_{\bar m}) \;\le\; H(i_1), \qquad g(i_{\bar m}) \;=\; \min\Big\{ H(i_1),\ \min_{j \in N(i_1)} H(j),\ \dots,\ \min_{j \in N(i_{\bar m - 1})} H(j) \Big\},

— BertsekasDP.rollout_sequential_improvement (goal, Prop. 6.4.2). Milestones: Props. 6.4.1 (termination under sequential consistency with the book's tie-breaking), 6.4.3 (exact cost identity via the defects $\delta_i$ ), 6.3.1, 6.3.2 (lookahead bounds), 6.2.1 (OLFC).

Significance

Prop. 6.4.2 is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, with Prop. 6.3.1 its stochastic counterpart (via Example 6.3.1 the rollout of any policy improves that policy). Prop. 6.3.2 is the robustness version that quantifies the cost of inexact minimization, used for CEC bounds. Formalizing the chapter yields a reusable graph-search + base-heuristic vocabulary and connects it to the Mission I stochastic model. Everything here is proved in the book; the formal versions are new.

Difficulty

The rollout proofs are elementary but exact: the min formula (6.37) requires tracking the running minimum along the run, and the IsLeast membership half forces identifying which neighbor value is attained. Termination under sequential consistency (6.4.1) is the delicate one — it fails without the tie-breaking convention (the book gives a cycling counterexample), so the formal statement carries the convention explicitly and the proof must extract a termination measure from "strict decreases are finitely many, plateaus shorten the heuristic path". The stochastic bounds are clean backward inductions over the Mission I recursion.

Formalization scope

Graph search: finite node type, arcs as ordered pairs, vertex costs only (no arc costs — the book's reduction absorbs them into destination costs); heuristic paths as lists; rollout runs as lists (finite, complete runs) except 6.4.1, where the run is an infinite sequence absorbed at destinations so that termination is a genuine claim. Ties in neighbor selection are allowed everywhere except where 6.4.1's convention pins them. Stochastic side: state-independent constraint sets for OLFC (as in §6.2); restricted lookahead sets $\bar U_k(x) \subseteq U_k(x)$ per Eq. (6.19); all statements at the level of the Mission I model.

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§6.2–6.4.) http://www.athenasc.com/dpbook.html
G. Tesauro, G. R. Galperin, On-line policy improvement using Monte-Carlo search, NIPS 1996. https://papers.nips.cc/paper/1302
D. P. Bertsekas, J. N. Tsitsiklis, C. Wu, Rollout algorithms for combinatorial optimization, J. Heuristics 3 (1997), 245–262. https://doi.org/10.1023/A:1009635226865

9 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: naimengye

Speculative Actions: Cost-Latency Analysis for Agentic SpeculationResearch Paper

Motivation

An LLM agent acting in an environment spends most of its wall-clock time waiting. Each step — a model call, a tool or MCP request, a browser action, sometimes a human reply — must complete before the next can be issued, and the round trips dominate end-to-end latency: a chess game between two reasoning agents runs for hours, and an operating-system tuning task for tens of minutes. When a training or prompt-optimization loop repeats such a run thousands of times, the waiting is the cost.

Speculative actions (Ye, Ahuja, Liargkovas, Lu, Kaffes, Peng, ICLR 2026) transplants a classical systems idea — speculative execution in microprocessors, and speculative decoding for LLM inference — to the agent's environment loop. A cheap, fast speculator guesses the action a slow, authoritative actor is about to produce, the guess is used to launch the next environment call early, and the work is committed only when the actor's real action confirms the guess. The interface stays sequential and lossless; the internals run in parallel.

What makes this a formalization target rather than an engineering report is the paper's §5 cost–latency analysis. Speculating more branches buys hit probability but costs tokens, and the paper derives closed-form expressions for both sides of that trade — a self-contained piece of applied probability sitting underneath a systems paper. This mission asks for those expressions, machine-checked.

Setting

Fix a horizon $T$ and index steps $t = 0, 1, \dots, T-1$ . At each step a policy maps the state to an API call; the actor executes it with latency $\mathrm{Exp}(\beta)$ , while the speculator proposes candidate actions with latency $\mathrm{Exp}(\alpha)$ , where $\beta < \alpha$ (the speculator is faster in expectation). A speculative branch hits when the action it guesses implies the same next call the actor's true action would have implied; branches hit independently across steps with probability $p$ .

Two knobs define the two regimes analyzed. Breadth $k$ : at each step, launch $k$ independent one-step speculations in parallel, each immediately followed by a real call. At least one of the $k$ succeeds with probability

p(k) \;=\; 1 - (1-p)^k .

Depth: follow a single branch, extending it whenever a speculative or real call returns and pruning subtrees the actor contradicts.

The quantity driving both results is $S_n$ , the expected number of hits by round $n$ . A hit consumes the following step's speculation window — after a correct guess the next call is already cached, so no new speculation is launched there — which yields the two-term recursion

S_0 = 0, \qquad S_1 = p, \qquad S_n = p\,(1 + S_{n-2}) + (1-p)\,S_{n-1}.

Write $T_{\mathrm{seq}}, M_{\mathrm{seq}}$ for the latency and token cost of strictly sequential execution, and $T_{\mathrm{spec}}, M_{\mathrm{spec}}$ for their speculative counterparts. In the depth regime latencies are taken deterministic: $a$ for a real call, $b < a$ for a speculative one.

Target

The goal theorem is the finite-horizon latency ratio for breadth-focused speculation (Proposition 1), with $p(k)$ abbreviated $p_k$ :

\frac{\mathbb{E}[T_{\mathrm{spec}}]}{\mathbb{E}[T_{\mathrm{seq}}]} = 1 - \frac{1}{T}\,\frac{\alpha}{\alpha+\beta} \left[\frac{(T-1)p_k}{1+p_k} + \frac{p_k^2}{(1+p_k)^2} - \frac{p_k^2}{(1+p_k)^2}(-p_k)^{T-1}\right].

The supporting targets, ordered as the analysis builds them:

the closed form $S_n = \frac{p}{1+p}n + \frac{p^2}{(1+p)^2}\bigl(1 - (-p)^n\bigr)$ solving the recursion;
the per-hit saving $\mathbb{E}[(B-A)^+] = \frac{\alpha}{\beta(\alpha+\beta)}$ for independent $A \sim \mathrm{Exp}(\alpha)$ , $B \sim \mathrm{Exp}(\beta)$ ;
the $T \to \infty$ limit $1 - \frac{p_k}{1+p_k}\cdot\frac{\alpha}{\alpha+\beta}$ , and the resulting 50% ceiling: the latency reduction is strictly below $\tfrac12$ for every $p_k \le 1$ ;
the cost counterpart (Theorem 4), finite-horizon and in the limit, with $\tilde k$ the number of distinct actions across the $k$ branches;
the depth-focused time and cost identities (Theorem 6), whose latency coefficient is $p$ rather than $\frac{p}{1+p}$ — raising the speedup ceiling from $\tfrac12$ to $1$ ;
the structure of confidence-aware selective speculation (Theorem 3 and Corollary 5): with sorted per-branch confidences, the marginal hit-probability gain is non-increasing, so the optimal breadth is the greedy threshold rule "add a branch while $\Delta^\star \delta q(m) \ge c$ ".

Significance

The analysis is what turns speculation from a trick into a tunable system. Proposition 1 and Theorem 4 are governed by the same quantity $p_k$ , so a practitioner who can estimate hit probability can choose $k$ offline against a latency/cost budget rather than by trial. The 50% ceiling is a genuine negative result — it says breadth alone cannot do better, and motivates the depth regime, where the ceiling becomes 1. Theorem 3 explains why confidence-based branch selection is cheap in practice: the whole dynamic program collapses to one scalar continuation value, so a runtime system sorts confidences and adds branches greedily in $O(k)$ per step.

The paper's proofs are pen-and-paper and, as far as we are aware, none of these results has a machine-checked proof. Three parts reward formalization specifically. The recursion's closed form is derived by a characteristic-equation argument with a particular solution that collides with the homogeneous part — routine but error-prone. The per-hit saving is an honest two-dimensional integral over independent exponentials. And Theorem 6's cost expression is stated in the paper with a floor function and then immediately replaced by an approximation, so formalizing it forces a decision about which claim is actually being asserted (see Formalization scope).

Difficulty

The obvious first move on the recursion — guess a constant particular solution — fails, because $r = 1$ is a root of the characteristic polynomial $r^2 - (1-p)r - p$ and a constant trial collides with the homogeneous family; the particular solution is linear in $n$ , and the $\frac{p^2}{(1+p)^2}$ coefficient comes out of matching both initial conditions, not one.

The interesting hypothesis is the one the recursion's shape encodes and the prose states only in passing: a hit at round $t$ removes the speculation window at round $t+1$ . Drop it and the recursion becomes one-term and the answer changes.

For the per-hit saving, the difficulty is analytic rather than algebraic: the inner antiderivative of $(b-a)\alpha e^{-\alpha a}$ must be handled, and the outer integral runs over an unbounded interval, so integrability has to be established rather than assumed.

The asymptotic statements need the oscillating term $(-p_k)^{T-1}$ controlled uniformly — it is bounded, not vanishing termwise in an obvious way — before the $\tfrac1T$ prefactor can be taken to zero.

Formalization scope

Everything is over $\mathbb{R}$ . The model lives in one definition bundle, Def_SpecActions_model, in namespace SpecActions; the mission's Lean names match the prose symbols ( $S_n$ is hits, $p(k)$ is phit, $\tilde k$ is kt).

The model is formalized at the level the paper's own proofs use: $\mathbb{E}[T]$ and $\mathbb{E}[M]$ are defined by the expressions Appendix A derives for them (specTime, specCost, and their depth analogues), and the theorems assert the algebraic and asymptotic identities relating those quantities. Deriving those expressions from a measure-theoretic model of the execution trace is deliberately not in scope — with one exception: milestone 2 states the per-hit saving as a genuine iterated integral against the exponential densities, so the one probabilistic step the paper actually computes is formalized as an integral rather than assumed.

Conventions a solver should know before starting:

Statements are quantified over $\alpha, \beta > 0$ and $0 \le p_k \le 1$ ; the standing assumption $\beta < \alpha$ is not imposed, since none of the identities need it.
Finite-horizon statements carry $1 \le T$ , and $T-1$ is natural-number subtraction — the $T = 0$ case is excluded rather than silently truncated.
hits takes $p_k$ (the per-step hit probability $p(k)$ ), not the per-branch $p$ ; phit relates the two, and Thm_SpecActions_phit_bounds supplies the $0 \le p(k) \le 1$ range facts the other statements assume.
Theorem 6's cost is stated as the exact identity, not the paper's approximation. The paper gives an exact expression involving $\lfloor a/b \rfloor$ and then an $\approx$ form with $\frac{a}{2b} - \frac12$ ; these coincide only when $a/b$ is an integer. The milestone asserts the exact floor version, which is what the proof establishes.
The 50% ceiling is stated as the strict bound $\frac{p_k}{1+p_k}\cdot\frac{\alpha}{\alpha+\beta} < \frac12$ , which holds for all admissible parameters; the paper's "upper bound of 50%, occurring when $p=1$ and $\alpha = \infty$ " describes an unattained supremum.
Theorem 3's dynamic program is formalized as the two facts that carry its content — diminishing marginal returns, and optimality of the greedy threshold breadth — rather than as a Bellman recursion over a mode process, which would require a full MDP development.

Reusable beyond this mission: the two-term linear recursion solved in milestone 1, and the $\mathbb{E}[(B-A)^+]$ computation for independent exponentials, which is a standard fact absent from Mathlib. Contributions extending the model toward an actual measure on execution traces — deriving specTime rather than defining it — are welcome as follow-on work.

Selected references

Naimeng Ye, Arnav Ahuja, Georgios Liargkovas, Yunan Lu, Kostis Kaffes, Tianyi Peng. Speculative Actions: A Lossless Framework for Faster Agentic Systems. ICLR 2026. arXiv:2510.04371 — Proposition 1 (p. 4), Appendix A (pp. 13–14), Theorem 3 (p. 10), Theorem 4 (p. 19), Corollary 5 (p. 22), Theorem 6 (p. 23).
Yaniv Leviathan, Matan Kalman, Yossi Matias. Fast Inference from Transformers via Speculative Decoding. ICML 2023. arXiv:2211.17192 — the speculate-verify pattern at token level.
Wenyue Hua, Mengting Wan, Shashank Vadrevu, Ryan Nadel, Yongfeng Zhang, Chi Wang. Interactive Speculative Planning. 2024. arXiv:2410.00079 — depth-oriented speculation on a single planning branch.
Yilin Guan et al. Dynamic Speculative Agent Planning. 2025. arXiv:2509.01920 — online RL for choosing speculation depth under a cost-latency trade-off.
Robert M. Tomasulo. An Efficient Algorithm for Exploiting Multiple Arithmetic Units. IBM Journal of Research and Development, 1967. DOI:10.1147/rd.111.0025 — speculative execution in hardware.

13 thms2 active usersReviewed

Completed

Algebra Combinatorics Information Theory·Captain: Rui Chao

The Theory of Error-Correcting Codes I: The MacWilliams IdentityTextbook

Motivation

Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code $C$ over a finite field has a dual code $C^\perp$ consisting of the words orthogonal to all words of $C$ under the standard coordinatewise bilinear form.

The MacWilliams identity states that the full Hamming-weight distribution of $C^\perp$ is determined by that of $C$ through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's The Theory of Error-Correcting Codes. The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.

This development isolates the arbitrary- $q$ Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.

Setting

Let $F$ be a finite field of cardinality $q$ , let $\iota$ be a finite coordinate type, and let a word be a function $c:\iota\to F$ . A linear code $C$ is an $F$ -linear subspace of the word space. The standard bilinear form is

\langle c,v\rangle=\sum_{i\in\iota}c_i v_i,

and the dual code is

C^\perp=\{v:\iota\to F:\langle c,v\rangle=0\text{ for every }c\in C\}.

The Hamming weight $\operatorname{wt}(c)$ is the number of coordinates at which $c$ is nonzero. Writing $n=|\iota|$ , the homogeneous Hamming weight enumerator of $C$ is the integer-coefficient polynomial

W_C(X,Y)=\sum_{c\in C}X^{n-\operatorname{wt}(c)}Y^{\operatorname{wt}(c)}.

Thus the coefficient of $X^{n-j}Y^j$ is the number of codewords of weight $j$ . The Lean development represents this object symbolically in MvPolynomial (Fin 2) ℤ; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.

Formalization targets

Character orthogonality over a code

For a primitive complex additive character $\psi$ of $F$ , define

S_C(v)=\sum_{c\in C}\psi(\langle c,v\rangle).

The first milestone states that $S_C(v)=|C|$ when $v\in C^\perp$ and $S_C(v)=0$ otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.

Coordinatewise Hamming transform

For every word $c$ and all $X,Y\in\mathbb C$ , the second milestone records the full character-weighted transform of the Hamming monomial:

\sum_{v\in F^\iota} X^{n-\operatorname{wt}(v)}Y^{\operatorname{wt}(v)} \psi(\langle c,v\rangle) = \bigl(X+(q-1)Y\bigr)^{n-\operatorname{wt}(c)} (X-Y)^{\operatorname{wt}(c)}.

This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.

MacWilliams identity

The capstone is the following equality of integer polynomials:

|C|\,W_{C^\perp}(X,Y) = W_C\bigl(X+(q-1)Y,\,X-Y\bigr).

This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula

W_{C^\perp}(X,Y) = \frac{1}{|C|}W_C\bigl(X+(q-1)Y,\,X-Y\bigr).

Significance

The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.

The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.

Difficulty

The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in $\mathbb C$ ; and the final result is most reusable as an equality of symbolic polynomials over $\mathbb Z$ . The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.

The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.

Formalization scope

The coordinate type is an arbitrary finite type rather than only Fin n; its cardinality plays the role of the code length. A word is CodingTheory.Word F ι := ι → F, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.

The polynomial CodingTheory.hammingWeightEnumeratorPolynomial has coefficients in $\mathbb Z$ and variables indexed by Fin 2. Variable $0$ records zero coordinates and variable $1$ records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.

The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to $1=1$ . The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.

Selected references

F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland, 1977, Chapter 5, pp. 125--154; especially Problem 13 (p. 134), Lemmas 9 and 11 (pp. 143--145), and Theorem 13 (p. 146). Publisher chapter record.
Violetta Weger, Coding Theory, Technical University of Munich lecture notes, 2025, Theorem 11.2 and Lemma 11.8, pp. 154--159.
F. J. MacWilliams, “A Theorem on the Distribution of Weights in a Systematic Code”, Bell System Technical Journal 42 (1963), 79--94.

4 thms2 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: xbgxjack

Gross–Yellen Graph Theory I: Cayley's Tree FormulaTextbook

Motivation

Counting the trees on a fixed, labeled vertex set is one of the oldest enumeration problems in graph theory. Cayley stated the count in 1889 while enumerating isomers of saturated hydrocarbons — each tree corresponds to a possible carbon skeleton — and the same number reappears throughout combinatorics as the number of spanning trees of the complete graph $K_n$ , a special case of Kirchhoff's Matrix–Tree Theorem, and as the base case against which more refined tree-counting results (trees with a prescribed degree sequence, forests, spanning trees of general graphs) are measured.

Several independent proofs of the count are known — a direct recursive argument, a determinant computation via the Matrix–Tree Theorem, a double-counting argument on increasing trees — and each exposes a different piece of structure. This mission formalizes the proof via Prüfer sequences, due to Prüfer (1918): an explicit, computable bijection between labeled trees and certain finite sequences, presented here following Gross and Yellen, Graph Theory and Its Applications, 3rd ed. (CRC Press, 2018), Section 3.7, pp. 157–162.

Setting

Fix $n \geq 2$ and take the vertex set to be $\{1, \dots, n\}$ (formalized as Fin n). A labeled tree on $n$ vertices is a simple graph $T$ on this vertex set that is connected and acyclic (Mathlib's SimpleGraph.IsTree). Two labeled trees are the same exactly when their edge sets coincide — the two 4-vertex trees in Figure 3.7.1 of the source are both paths but are different labeled trees, since the labels sit on different vertices.

A Prüfer sequence of length $n - 2$ is any sequence $(s_1, \dots, s_{n-2})$ of labels drawn from $\{1, \dots, n\}$ , repetitions allowed (so there are $n^{n-2}$ of them, by the rule of product).

The encoding of a tree $T$ (Algorithm 3.7.1, p. 157) builds its Prüfer sequence by repeating, $n-2$ times: find the leaf (degree-one vertex) with the smallest label among those not yet removed, record the label of its neighbor, then delete that leaf. The decoding of a sequence (Algorithm 3.7.3, p. 159) reverses this: it rebuilds the tree edge by edge, at each step joining the smallest label not yet used and not appearing later in the sequence to the next label in the sequence, finishing by joining the two labels left over.

Formalization targets

Goal — Cayley's Tree Formula (Theorem 3.7.5, p. 162)

\operatorname{Nat.card}\, \{T : \text{SimpleGraph}(\text{Fin } n) \mid T.\text{IsTree}\} = n^{\,n-2}, \qquad n \geq 2.

This is the weakest stable statement: it is exactly the count Cayley identified, phrased without reference to any particular proof method, so it is not tied to properties of Prüfer sequences beyond what is needed to establish the count.

Significance

The identity itself is foundational: it is the base case of Kirchhoff's Matrix–Tree Theorem (which computes the analogous count for spanning trees of an arbitrary graph as a cofactor of its Laplacian) and it appears as an ingredient in random graph theory (counting spanning trees of $K_n$ bounds the number of ways a random graph process can build a tree) and in the analysis of algorithms on trees, where the Prüfer encoding itself is used as a compact serialization of a labeled tree.

The result has been proved by hand for over a century, and its most classical proof (the one formalized here) has not, to this project's knowledge, appeared as a machine-checked Lean proof; Mathlib's Combinatorics.SimpleGraph library has the tree and acyclicity infrastructure this mission builds on, but not the Prüfer bijection or the count itself. Formalizing it here means constructing the encoding and decoding maps explicitly as computable, total recursive functions, and proving they are mutually inverse — the mission's four milestones below are exactly the four supporting results the source uses for this.

Difficulty

The obvious first attempt is to define the encoding by structural recursion, peeling one leaf per step, but this immediately runs into a dependent-typing obstacle: after deleting a vertex, the "remaining graph" naturally lives on a smaller vertex type, so a naive recursive definition changes type at every step and the final sequence's type (length $n-2$ ) is not visible to the recursion by construction. The formalization here sidesteps this by keeping the ambient vertex type fixed at Fin n throughout and tracking the shrinking set of "active" vertices as an ordinary Finset (Fin n) parameter, so the recursion is on a natural number step-counter rather than on the type itself; the price is that every step's "leaf" and "neighbor" must be picked out by an explicit Finset.filter/Finset.min computation whose well-definedness (there is always a smallest active leaf, and it always has a unique active neighbor) is exactly the content of Propositions 3.7.1 and 3.7.3 below, rather than something the type system gives for free. The inverse direction has the dual issue in reverse: decoding recurses structurally on the sequence while tracking a shrinking label set, and showing the two recursions undo each other (Proposition 3.7.4) requires the same induction run in both directions simultaneously.

Formalization scope

Trees are SimpleGraph (Fin n) satisfying Mathlib's SimpleGraph.IsTree; no alternate, weaker notion of "tree" is used. Prüfer sequences are functions Fin (n - 2) → Fin n (equivalently, by Fintype.card_fun, exactly the $n^{n-2}$ count needed) rather than List or Vector, so that the final counting step is immediate once the bijection is established. The encoding and decoding functions (pruferEncode, pruferDecode) are supplied as noncomputable definitions in Definitions.Def_GYGraphTheory — noncomputable only because Prop-level decidability of a general SimpleGraph.Adj is classical, not because the algorithm is non-constructive; every step is the literal Prüfer procedure, junk-valued (defaulting to label 0) outside its intended domain in exactly the way a hand proof would say "this step is meaningless once fewer than two active vertices remain." The four milestones give the precise faithful statements of the source's Propositions 3.7.1, Corollary 3.7.2, Proposition 3.7.3, and Proposition 3.7.4; the goal theorem is the immediate corollary once all four are in hand, via Fintype.card_congr and Fintype.card_fun. A trivializing formalization is not available here: IsTree is Mathlib's standard, non-vacuous notion, and the milestones pin down pruferEncode and pruferDecode to the source's specific algorithm rather than leaving the bijection's existence as a free black box. Beyond the four milestones, a full development needs: basic Finset/List manipulation lemmas relating pruferPeel's step-indexed recursion to pruferDecodeAux's list-indexed recursion (reusable in any future mission touching Prüfer-style encodings); and the final cardinality argument tying the bijection to n ^ (n - 2). Contributions connecting this formula to Mathlib's general Matrix–Tree machinery (if and when it exists) would be a natural, welcome extension but are out of scope for this mission.

Selected references

A. Cayley, A theorem on trees, Quart. J. Math. 23 (1889), 376–378.
H. Prüfer, Neuer Beweis eines Satzes über Permutationen, Archiv der Mathematischen Physik 27 (1918), 742–744.
J.L. Gross and J. Yellen, Graph Theory and Its Applications, 3rd ed., CRC Press, 2018, Section 3.7 "Counting Labeled Trees: Prüfer Encoding", pp. 157–162.

8 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: hao jia

Weak Pentagon Colorings of Triangle-Free Cubic Graphs (OPG-434)Open Problem

Motivation

The weak pentagon problem asks for a five-label structure on the edges of every triangle-free cubic graph. Although its wording resembles proper edge coloring, properness is not part of the conjecture. Instead, each individual color class must meet enough odd cycles that deleting that class leaves a bipartite spanning graph. The problem connects odd-cycle transversals, cut structure, and homomorphisms to a fixed sixteen-vertex graph.

Robert Šámal recorded the conjecture on the Open Problem Garden in 2007. DeVos and Šámal proved that sufficiently high-girth subcubic graphs map to the Clebsch graph, with an explicit girth threshold in their theorem; that does not cover all triangle-free cubic graphs. The mission separates the general existence question from two exact reformulations that can be verified independently.

Setting

Let $G$ be a finite simple triangle-free cubic graph. A five-edge coloring here is any symmetric assignment

c:E(G)\longrightarrow\{1,2,3,4,5\}.

It need not be proper or surjective. For a color $i$ , delete all edges with label $i$ while retaining every vertex. The coloring is a weak-pentagon coloring when each of the five resulting spanning graphs is bipartite.

Equivalently, each color class is an odd-cycle edge transversal: it meets the edge set of every simple odd cycle. The cycles are not required to be induced. This last distinction matters because an odd cycle may have a chord in the original graph and still survive in a deleted-edge spanning subgraph.

A second representation uses the sixteen four-bit vectors. Two vectors are adjacent when their Hamming distance is three or four. This graph is a model of the Clebsch graph. A graph homomorphism sends every edge of $G$ to an adjacent pair in this target.

Formalization targets

Weak pentagon conjecture

The root target is

\forall G\text{ finite, simple, triangle-free, and cubic}, \qquad \exists c:E(G)\to[5]\ \forall i\in[5], \quad G-c^{-1}(i)\text{ is bipartite}.

No condition is imposed on adjacent edges receiving different labels.

Odd-cycle equivalence

For every fixed graph and fixed five-edge labeling,

\bigl(\forall i,\ G-c^{-1}(i)\text{ is bipartite}\bigr) \quad\Longleftrightarrow\quad \bigl(\forall i,\ c^{-1}(i)\text{ meets every odd cycle of }G\bigr).

This theorem is graph-general: triangle-freeness and cubicity delimit the root but are not needed for the equivalence.

Sixteen-vertex homomorphism formulation

For every finite simple graph $G$ ,

G\text{ has a weak-pentagon coloring} \quad\Longleftrightarrow\quad G\longrightarrow H_{16},

where $H_{16}$ has vertex set $\{0,1\}^4$ and edges at Hamming distance three or four. The statement concerns existence of some coloring and some homomorphism; it does not preserve an arbitrarily prescribed coloring.

Significance

The root theorem would establish a uniform parity decomposition for all triangle-free cubic graphs. The transversal form makes every odd cycle use all five colors. The homomorphism form replaces edge labels and five separate bipartitions by one bounded vertex certificate, allowing structural and computational methods to share an exact target.

Formalization prevents several nearby but inequivalent conjectures from being conflated. A weak-pentagon coloring can be improper. Checking only induced odd cycles of the original graph is insufficient. Mapping to a five-cycle is stronger and fails even for familiar positive examples. The explicit four-bit model also avoids relying on the name “Clebsch graph” without fixing its adjacency convention.

Difficulty

The equivalences reorganize the problem but do not create the required object. Five odd-cycle transversals must be pairwise compatible as color fibers; finding one small transversal is not enough. Local deletion and gluing methods must preserve existence of a whole homomorphism, not one chosen boundary assignment.

High-girth results leave finitely many short-cycle configurations only when the girth hypothesis is present. Triangle-free graphs may still contain overlapping five- and seven-cycles, and naive local recoloring can repair one odd cycle while breaking another color complement. Minimum-counterexample arguments also require care because deleting vertices preserves subcubicity but not cubicity.

Formalization scope

Colors are Fin 5. The coloring stores a symmetric value on ordered endpoint pairs, with nonedge values ignored. Cubic means every neighbor set has extended cardinality exactly three. A simple odd cycle is a cyclic list of at least three distinct vertices of odd length; it need not be induced. Bipartiteness is witnessed by a Boolean side assignment after one color is deleted.

The sixteen-vertex relation is defined directly on four-bit functions by Hamming distance, so its cardinality and adjacency are not hidden behind an imported graph name. The repository's transversal proof, normalization, and local homomorphism studies are candidate_only; the mission publishes their clean statements as proof obligations. Contributions may close either equivalence, formalize known high-girth results, prove restricted graph classes, or attack the root. A finite benchmark or a failure of one extension strategy is not a counterexample to the conjecture.

Selected references

R. Šámal, Weak pentagon problem, Open Problem Garden, 2007. https://www.openproblemgarden.org/op/weak_pentagon_problem
M. DeVos and R. Šámal, High-girth cubic graphs are homomorphic to the Clebsch graph, Journal of Graph Theory 66 (2011), 241–259. https://arxiv.org/abs/math/0602580
P. Kolman, B. Lidický, and J.-S. Sereni, On Minimum Fair Odd Cycle Transversal, 2010. https://kam.mff.cuni.cz/kamserie/clanky/2010/s956.pdf
Open Problem Garden / UnsolvedMath, OPG-434. https://www.unsolvedmath.com/problems/OPG-434

4 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: hao jia

Two Acyclic Colors for Planar Orientations (OPG-169)Open Problem

Motivation

The dichromatic number of a digraph is the directed analogue of chromatic number: vertices of one color may be adjacent, but each color class must induce an acyclic digraph. The Two Color Conjecture asks whether every orientation of a planar graph has dichromatic number at most two. It is a natural directed-coloring counterpart to planar graph coloring, with the key difference that forbidden monochromatic objects are directed cycles rather than undirected edges.

Critical-digraph theory gives general degree restrictions on minimal counterexamples, and Li and Mohar proved two-colorability under the additional hypothesis that the directed girth is at least four. The unrestricted planar-orientation problem permits directed triangles, so that theorem is a genuine partial result rather than a solution. The project candidate develops the elementary least-order-counterexample consequences needed before any planar structural argument.

Setting

Let $G$ be a finite simple planar graph. An orientation $D$ assigns exactly one direction to every edge of $G$ , with no loops, parallel arcs, or pair of opposite arcs. For $X\subseteq V(D)$ , the induced digraph $D[X]$ retains every arc whose two endpoints lie in $X$ .

A two-coloring is a map

c:V(D)\longrightarrow\{0,1\}.

It is valid when both induced digraphs $D[c^{-1}(0)]$ and $D[c^{-1}(1)]$ contain no directed cycle. The color classes need not be independent and either color may be unused.

Planarity belongs to the underlying undirected graph. Lean represents it by an injective straight-line embedding with noncrossing nonincident edges. Directed reachability is reflexive, so a singleton orientation is strongly connected under the usual length-zero convention, although it is also acyclic and hence cannot be a counterexample.

Formalization targets

Two Color Conjecture

The goal is

\forall D\text{ an orientation of a finite simple planar graph}, \qquad \exists c:V(D)\to\{0,1\}, \quad D[c^{-1}(0)]\text{ and }D[c^{-1}(1)]\text{ are acyclic}.

Disconnected graphs and empty color classes are included.

Least-order counterexample structure

A supporting theorem states that every counterexample of minimum vertex order is nonempty and strongly connected, and its underlying graph has minimum degree at least three:

D\text{ least-order counterexample} \quad\Longrightarrow\quad D\text{ strongly connected and }\delta(U(D))\ge3.

The minimum is taken over the full class of finite planar orientations, not over one embedding or an arc-minimal subclass.

Semidegree candidate

A stronger open milestone asks whether every vertex of such a least-order counterexample has at least two incoming and at least two outgoing neighbors. This is recorded separately because it is stronger than the degree-three conclusion and its repository proof remains candidate_only.

Significance

The root theorem would establish a universal two-color bound for planar orientations while allowing directed triangles and arbitrary local degree. A counterexample would demonstrate a sharp obstruction specific to directed cycles, not visible to ordinary planar coloring.

The formalized minimal-counterexample package is reusable regardless of the ultimate answer. Strong connectivity permits arguments inside one component, while the degree and semidegree restrictions narrow discharging configurations and finite searches. Encoding the full induced color classes prevents an invalid shortcut in which only a selected acyclic spanning subdigraph is checked.

Difficulty

Deleting a low-degree vertex is safe only if a valid coloring of the smaller graph can be extended without creating a monochromatic directed cycle through the restored vertex. For a chosen color, obstruction depends on both an incoming and an outgoing neighbor of that color together with a directed return path in the old color class. Merely seeing same-colored in- and out-neighbors is not sufficient.

Strongly connected components can be colored separately because their condensation is acyclic, but that observation only reduces a minimal counterexample to one component. Planarity alone does not eliminate directed triangles or the return paths that block both colors. Results assuming directed girth at least four therefore leave the central case untouched.

Formalization scope

A directed graph is a binary relation, coupled to a SimpleGraph by an orientation predicate that requires exactly one direction on every edge and forbids arcs on nonedges. A directed cycle is a cyclic list of at least three distinct vertices. A color class is acyclic when no such list lies entirely in that class. Strong connectivity is nonempty mutual reflexive-transitive reachability.

The least-order predicate quantifies over every smaller finite planar orientation in the same universe. It does not assert that a counterexample exists. Consequently, its structural theorems may be true vacuously if the root conjecture is true; the read-back must expose that conditional form.

Repository arguments, finite tables, and transport receipts are not machine-checked proofs. Contributions may formalize component gluing, exact vertex-extension criteria, degree or semidegree restrictions, planar reducible configurations, or the root. Any stronger minimum-degree claim must remain distinct from the admitted degree-three target until proved.

Selected references

Open Problem Garden / UnsolvedMath, OPG-169: The Two Color Conjecture. https://www.unsolvedmath.com/problems/OPG-169
B. Mohar, Eigenvalues and colorings of digraphs, Linear Algebra and its Applications, 2010. https://www.sfu.ca/~mohar/Reprints/Inprint/BM09_LAA09_Mohar_EigenvaluesandColorings.pdf
Z. Li and B. Mohar, Planar digraphs of digirth four are 2-colourable, Journal of Combinatorial Theory, Series B, 2017. https://arxiv.org/abs/1606.06114

4 thms2 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: Goku

The Aaronson-Ambainis ConjectureOpen Problem

Motivation

Quantum query algorithms are known to beat classical ones on problems with algebraic structure -- period finding, hidden subgroups, forrelation. No such speedup is known for a problem with no structure at all. Aaronson and Ambainis proposed making that observation into a theorem, and reduced it to a question with no quantum content: a statement about bounded low-degree polynomials on the Boolean cube (Aaronson--Ambainis 2009).

The question has resisted since. A timeline of what is actually established:

2009. Aaronson and Ambainis state the conjecture and prove that it implies almost-everywhere classical simulation of quantum query algorithms.
2012. Montanaro settles the case of block-multilinear forms whose coefficients all have the same magnitude.
2016. O'Donnell and Zhao reduce the general conjecture to a restricted class, the one-block decoupled polynomials.
2019. Aaronson surveys a decade of partial progress (retrospective).
2022. Bansal, Sinha and de Wolf prove the conjecture for completely bounded degree- $d$ block-multilinear forms, obtaining influence $1/\mathrm{poly}(d)$ at constant variance (arXiv:2203.00212).
2024. The conjecture is established for a non-negligible fraction of random restrictions (arXiv:2402.13952).

The cases that are settled are settled under structural hypotheses -- block-multilinearity, complete boundedness, symmetry, Boolean range. The general statement is open.

Setting

Let $N$ be a positive integer. The Boolean cube is $\{0,1\}^N$ , carrying the uniform distribution; a point $x$ is identified with the $0/1$ real vector it names, so a real multivariate polynomial $p$ in $N$ variables has a value $p(x)$ at each cube point. For a function $f$ on the cube write

\mathbb{E}[f]=2^{-N}\sum_{x\in\{0,1\}^N}f(x).

The variance of $p$ is $\operatorname{Var}[p]=\mathbb{E}\big[(p-\mathbb{E}[p])^2\big]$ . Writing $x^{\oplus i}$ for $x$ with its $i$ -th bit flipped, the influence of coordinate $i$ on $p$ is

\operatorname{Inf}_i[p]=\mathbb{E}\big[(p(x)-p(x^{\oplus i}))^2\big].

These are the combinatorial forms of both quantities, as used in the source; no Fourier--Walsh expansion is required to state anything below. The degree of $p$ is its total degree as a polynomial. Call $p$ bounded when $0\le p(x)\le 1$ at every cube point -- a condition imposed only on the cube, not on all of $\mathbb{R}^N$ .

Target

The goal is the conjecture in the shape stated by its authors: there is an absolute constant $C$ such that for all $N$ , all $d$ , every polynomial $p$ of degree at most $d$ that is bounded on the cube, and every $\varepsilon>0$ with $\operatorname{Var}[p]\ge\varepsilon$ , some coordinate $i$ satisfies

\operatorname{Inf}_i[p]\;\ge\;\Big(\frac{\varepsilon}{d}\Big)^{C}.

The constant $C$ is quantified outermost and may depend on nothing. That uniformity is the entire content: bounds that degrade exponentially in $d$ are already known, and a goal naming a specific exponent would be superseded by the next improvement.

Significance

The result itself. Aaronson and Ambainis prove that the conjecture implies that the acceptance probability of any bounded-error $T$ -query quantum algorithm on a Boolean input can be approximated, to small error on all but a small fraction of inputs, by a classical algorithm making $\mathrm{poly}(T)$ queries. Quantum speedups would then require structure in a precise sense. The conjecture also has purely classical content, asserting that boundedness plus low degree forces variance to concentrate on some single coordinate rather than spread across all $N$ . Without it, no such concentration is known at any rate polynomial in $1/d$ .

Formalizing it. The conjecture is open, so this mission does not formalize a known proof of the goal. What it produces is a machine-checked statement of the conjecture together with formalizations of the partial results above, each currently existing only on paper. The milestone chain also yields reusable infrastructure for analysis of Boolean functions, of which Mathlib currently contains none: no Fourier--Walsh expansion, no influence, no variance on the cube.

Difficulty

The elementary bound is the Poincare inequality on the cube, $4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$ , which yields a coordinate with influence at least $4\varepsilon/N$ . This is tight for the dictator $p(x)=x_1$ and depends on $N$ , so it says nothing: the conjecture demands a bound free of $N$ entirely.

The natural repair is the route available when $p$ takes only the values $0$ and $1$ . A Boolean-valued polynomial of degree $d$ depends on boundedly many coordinates, which immediately produces an influential one. That argument does not survive relaxing the range to the interval $[0,1]$ : a bounded real-valued polynomial of low degree need not depend on boundedly many coordinates, and every known substitute loses a factor exponential in $d$ . Closing the gap between exponential and polynomial dependence on $d$ is the difficulty, and it is where all of the partial results stop.

Formalization scope

Polynomials are MvPolynomial (Fin N) ℝ and degree is Mathlib's totalDegree, so the statement needs no bespoke notion of degree. Expectation is a finite sum scaled by $2^{-N}$ rather than a measure-theoretic integral, keeping every definition elementary. Bit flipping is Function.update x i (!x i). Boundedness is asserted at cube points only. Variance and influence are the combinatorial definitions above, published as the definition AaronsonAmbainis.

Three points close off degenerate readings. The exponent $O(1)$ of the source is rendered as an existentially quantified natural number with no leading multiplicative constant, since admitting one weakens the claim. Taking that exponent to be $0$ would demand influence at least $1$ and is therefore not a trivializing choice, while larger exponents only weaken the bound; the content is that some fixed exponent suffices for all $N$ and $d$ at once. The hypothesis $\deg p\le d$ is universally quantified over $d$ , which is equivalent to the source's exact-degree form because the smallest admissible $d$ gives the strongest conclusion. The cases $N=0$ and $d=0$ are vacuous, since $0<\varepsilon\le\operatorname{Var}[p]$ fails for a constant polynomial.

A complete development needs, beyond the published definitions, a Fourier--Walsh layer with Parseval's identity, the level- $k$ machinery used by the partial results, and -- for the completely bounded case -- operator-space norms on multilinear forms. All of the Boolean-analysis material is reusable well beyond this mission. Contributions of any milestone are welcome, as are alternative formalizations of the definitions in function-level rather than polynomial-level form.

Out of scope: the quantum simulation consequence is not formalized here. Stating it requires a formal quantum query model, which no Lean library currently provides.

Selected references

S. Aaronson, A. Ambainis, The Need for Structure in Quantum Speedups, Theory of Computing 10 (2014) 133--166; arXiv:0911.0996. Conjecture 6.
N. Bansal, M. Sinha, R. de Wolf, Influence in Completely Bounded Block-multilinear Forms and Classical Simulation of Quantum Algorithms, CCC 2022; arXiv:2203.00212.
Aaronson--Ambainis Conjecture Is True For Random Restrictions, 2024; arXiv:2402.13952.
S. Aaronson, The Aaronson-Ambainis Conjecture (2008-2019), blog retrospective.
S. Arunachalam, J. Briet, C. Palazuelos, Quantum query algorithms are completely bounded forms, SIAM J. Comput. 48 (2019); arXiv:1711.07285.
AIM problem list, Analysis on the hypercube with applications to quantum computing, aimpl.org/hypercubequantum.

4 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: hao jia

Monochromatic Reachability in Three-Colored Tournaments (OPG-1808)Open Problem

Motivation

Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.

The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly candidate_only: it is bounded search evidence, not a proof of the unrestricted theorem.

Setting

A tournament is an orientation of a finite complete simple graph. For each pair of distinct vertices $u,v$ , exactly one of $u\to v$ and $v\to u$ is present. Every directed arc receives one of three labeled colors.

A rainbow directed triangle is a cyclically oriented triangle

a\to b\to c\to a

whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.

A vertex $s$ is a monochromatic source when, for every vertex $t$ , there is some color $k$ and a directed $s$ -to- $t$ path all of whose arcs have color $k$ . The chosen color may depend on $t$ ; the theorem does not demand one common color for all targets. Length-zero reachability handles $t=s$ .

The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.

Formalization targets

Root theorem

For every nonempty finite tournament $T$ with a three-coloring of its arcs,

T\text{ has a rainbow directed triangle} \quad\lor\quad \exists s\in V(T)\ \forall t\in V(T),\ \text{$s$ reaches $t$ monochromatically}.

No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.

Finite order milestone

The first milestone freezes the exact bounded claim supported by the replay package:

1\le |V(T)|\le 11\text{ and no rainbow directed triangle} \quad\Longrightarrow\quad T\text{ has a monochromatic source}.

The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.

Significance

The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.

The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc $u\to_F v$ may encode that $v$ cannot reach $u$ ; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.

Difficulty

The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.

The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.

Formalization scope

Lean represents the tournament as a binary relation D with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.

The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.

Selected references

Open Problem Garden, Monochromatic reachability versus rainbow triangles, posted 2008. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles
B. Sands, N. Sauer, and R. Woodrow, On monochromatic paths in edge-coloured digraphs, Journal of Combinatorial Theory, Series B 33 (1982), 271–275.
A. Georgakopoulos and P. Sprüssel, On 3-coloured tournaments, 2009. https://arxiv.org/abs/0904.1967
A. Trygub, Full Characterization of Color Degree Sequences in Complete Graphs Without Tricolored Triangles, 2023. https://arxiv.org/abs/2304.14579

6 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: hao jia

Circular (20,7)-Coloring of Triangle-Free Subcubic Planar Graphs (OPG-401)Open Problem

Motivation

Circular coloring refines ordinary vertex coloring by placing colors on a cycle and measuring separation modulo the palette size. It records information that an ordinary chromatic-number bound can lose, and it interacts sharply with planarity, forbidden short cycles, and degree constraints. OPG-401 asks for a specific bound at the intersection of those themes: whether triangle-free planar graphs of maximum degree three always admit a circular coloring of ratio $20/7$ .

The question appears on Xuding Zhu's open-problem page and in the Open Problem Garden record. Nearby theorems on fractional coloring do not settle it: fractional chromatic number and circular chromatic number are distinct parameters, so the known fractional bounds for subcubic triangle-free graphs cannot simply be substituted for a circular-coloring proof. Work on circular recoloring likewise studies connectivity between colorings that already exist and does not supply the missing universal existence theorem.

Setting

For integers $p\ge 2q>0$ , a $(p,q)$ -coloring of a finite simple graph $G$ is a map

\varphi:V(G)\longrightarrow \mathbb Z_p

such that the shortest cyclic distance between $\varphi(u)$ and $\varphi(v)$ is at least $q$ for every edge $uv$ . Equivalently, using representatives in $\{0,\ldots,p-1\}$ , the modular difference lies between $q$ and $p-q$ , inclusive. The circular chromatic number is the infimum of the ratios $p/q$ for which such a coloring exists.

The root domain consists of all finite simple graphs that are planar, triangle-free, and subcubic. Disconnected and empty graphs are included. Planarity is represented by an injective straight-line drawing with no vertex in the interior of an edge and no intersection between nonincident edges. For finite simple graphs this is the standard straight-line form of planarity.

Formalization targets

Root question

The central target is

G\text{ finite, simple, planar, triangle-free, and }\Delta(G)\le 3 \quad\Longrightarrow\quad G\text{ has a }(20,7)\text{-coloring}.

This is exactly the claim $\chi_c(G)\le 20/7$ in a form suitable for finite Lean data.

Local extension table

A reusable finite milestone freezes the local palette arithmetic. For $a\in\mathbb Z_{20}$ , let $A(a)$ be the colors at cyclic distance at least seven from $a$ . For all $a,b$ ,

|A(a)\cap A(b)|=7-d_{20}(a,b), \qquad A(a)\cap A(b)\ne\varnothing\iff d_{20}(a,b)\le6.

This includes equal colors, antipodal colors, tied symmetries, and all twenty residues. It is the exact obstruction encountered when extending a coloring over a deleted degree-two vertex while preserving every old color. The repository artifact supporting this formulation is only candidate_only; the mission publishes the statement as an open formal target rather than claiming it as proved.

Significance

A proof of the root theorem would give the requested sharp circular-coloring guarantee uniformly over a broad planar graph class. It would also separate the circular problem from nearby fractional results by constructing the stronger cyclic palette assignment itself. A counterexample, if one exists, would have to survive the combined restrictions of planarity, triangle-freeness, and maximum degree three, and would identify a genuine boundary for local extension methods.

Formalization adds two concrete assets. First, the cyclic-distance convention is fixed once, avoiding common errors involving directed residues, unrestricted integer lifts, or truncated subtraction. Second, graph reductions can be checked against a precise preservation obligation: deleting a vertex does not help unless the chosen coloring of the smaller graph has compatible boundary colors. The mission therefore welcomes both global structural arguments and verified finite boundary classifications, but finite enumeration alone is not accepted as a proof for arbitrary graph order.

Difficulty

The obvious induction on vertices fails at degree two. A coloring of $G-v$ need not extend over $v$ : if its two neighbors receive colors at cyclic distance at least seven, their two allowed sets can be disjoint. The local table characterizes this failure exactly but does not guarantee that a different coloring of $G-v$ has favorable boundary values. Recoloring, reducible configurations, and planar discharging must therefore interact without silently assuming universal extension or connectivity of the recoloring graph.

A second source of difficulty is parameter confusion. Bounds for fractional colorings do not automatically yield $(20,7)$ -colorings, and a theorem about mixing existing circular colorings does not prove existence. Any proposed bridge must be stated and verified explicitly.

Formalization scope

Lean represents colors by Fin 20 and uses the minimum of the two directed modular differences as cyclic distance. Edge compatibility includes both the lower bound $7$ and the formal upper bound $13$ . Triangle-freeness is literal absence of three mutually cyclic adjacent vertices, and subcubic means every neighbor set has extended cardinality at most three.

The definition bundle contains no theorem and no sorry. Draft theorem items contain exactly one := by sorry. The local candidate computations and GitHub transport records are provenance, not evidence that either theorem is proved. A complete contribution may formalize the finite palette table, a faithful reducible configuration, a recoloring lemma with all quantifiers exposed, or the root theorem. Every claimed universal reduction must retain finiteness, simplicity, planarity, triangle-freeness, and the degree bound.

Selected references

X. Zhu, Circular chromatic number of triangle-free planar graphs with maximum degree three, open-problem page. https://www.math.nsysu.edu.tw/~zhu/open-problems/chic-k3free-planar.htm
Open Problem Garden, OPG-401. https://www.unsolvedmath.com/problems/OPG-401
X. Zhu, The fractional version of Hedetniemi's conjecture is true, European Journal of Combinatorics, 2011. https://doi.org/10.1016/j.ejc.2011.03.004
Z. Dvořák, J.-S. Sereni, and J. Volec, Subcubic triangle-free graphs have fractional chromatic number at most 14/5, Journal of the London Mathematical Society, 2014. https://arxiv.org/abs/1301.5296

3 thms2 active usersReviewed

All missions

Gribov Ambiguity: no continuous gauge fixing (Singer 1978)Research Paper

Motivation

Setting

Formalization targets

Goal — Corollary 4 (no gauge fixing)

Milestone level — Theorem 3

Milestone level — Theorem 5 and its homotopy inputs

Significance

Difficulty

Formalization scope

Selected references

Algebraicity of Weil classes on abelian sixfolds of discriminant -1Research Paper

Motivation

Setting

Formalization targets

Goal — Theorem 1.5.1 of arXiv:2502.03415

Milestone — Weil's plane of Hodge–Weil classes (§1.1)

Milestone — Schoen's degeneration step (§1.6)

Milestone — Corollary 1.6.1

Milestone — Lefschetz (1,1)(1,1)(1,1)

Significance

Difficulty

Formalization scope

Selected references

Schinzel's Hypothesis HOpen Problem

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Rudin PMA IV: ContinuityTextbook

Motivation

Setting

Formalization targets

Goal — uniform continuity on compacta (Theorem 4.19)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Brin–Squier: the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints has no free subgroup of rank greater than oneResearch Paper

Motivation

Setting

Formalization targets

Goal — no two elements generate freely

The dichotomy it rests on

The twenty-four milestones

Significance

Difficulty

Formalization scope

Selected references

Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper

Motivation

Setting

Formalization targets

Goal — reconstruction theorem, Theorem 3.10 for γ>0\gamma>0γ>0

Milestone level — the calculus around the reconstruction operator

Significance

Difficulty

Formalization scope

Selected references

Rudin PMA III: Numerical Sequences and SeriesTextbook

Motivation

Setting

Formalization targets

Goal — Riemann's rearrangement theorem (Theorem 3.54)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Rudin PMA II: Basic TopologyTextbook

Motivation

Setting

Formalization targets

Goal — Heine–Borel (Theorem 2.41)

Milestones

Milestone — Lefschetz $(1,1)$

Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$