All missions

Why subpolytopes matter

A convex polytope can be studied metrically, through coordinates and lengths, or combinatorially, through the inclusion order of its faces. Grünbaum's Convex Polytopes develops the second viewpoint systematically: two polytopes have the same combinatorial type when their complete face posets are order-isomorphic. Chapter 7 studies neighborly polytopes, which have as many low-dimensional faces as their vertex sets permit. These objects are central test cases because very strong local face incidence coexists with a large variety of realizations and combinatorial types.

The capstone of this mission is the rigidity statement attributed in §7.5 to Shemer: in even dimension, the combinatorial type of a neighborly polytope determines the combinatorial type of every subpolytope spanned by a subset of its vertices. Here “rigid” is exclusively combinatorial. It does not assert preservation of lengths, angles, coordinates, or projective realization. The source statement appears in Branko Grünbaum, Convex Polytopes, second edition, §7.5, printed p. 129b / PDF p. 161 (Springer edition).

Polytopes, faces, and neighborliness

The Lean development represents the ambient real space of dimension $d$ as Fin d → ℝ. A predicate IsDPolytope P says that $P$ is the convex hull of a finite nonempty vertex set and has full affine span. Faces are modeled by Mathlib's exposed-face predicate. The type PolytopeFace P contains all exposed faces ordered by inclusion, including the empty face and $P$ itself; an order isomorphism of these types is the formal representation of combinatorial equivalence.

For a positive integer $k$, a polytope is $k$-neighborly when every $k$-element set of vertices spans a proper face and is exactly the vertex set of that face. The definition IsKNeighborly k P states this directly for finite sets of exposed singleton vertices. Grünbaum defines an even-dimensional polytope of dimension $2r$ to be neighborly when it is $r$-neighborly. The theorem therefore assumes $r \ge 1$ and uses IsKNeighborly r for both parent polytopes.

Formalization target

Let $P$ and $Q$ be full-dimensional neighborly polytopes in $\mathbb{R}^{2r}$. Their vertices are enumerated injectively by maps $V,W : \operatorname{Fin}(m) \to \mathbb{R}^{2r}$. A permutation $\theta$ records the prescribed correspondence between the two vertex sets, and an order isomorphism $\Phi$ between the full face posets witnesses that this correspondence comes from a combinatorial equivalence of the parent polytopes.

For every index set $I \subseteq \operatorname{Fin}(m)$, the target produces an order isomorphism

$$\mathcal F\bigl(\operatorname{conv}(V(I))\bigr) \simeq \mathcal F\bigl(\operatorname{conv}(W(\theta(I)))\bigr),$$

and requires it to carry each selected singleton vertex $V(i)$ to $W(\theta(i))$. The quantifier over $I$ is unrestricted. Empty, singleton, lower-dimensional, and full vertex subsets are all included. No selected subpolytope is required to be full-dimensional or neighborly.

What the theorem determines

Knowing only how many neighborly combinatorial types exist would not reconstruct any particular vertex-induced subpolytope. The rigidity theorem is stronger: once the complete face-poset type of the parent and its vertex correspondence are fixed, the complete face-poset type of every labelled vertex subpolytope is fixed as well. This is why the formal conclusion keeps the label-preservation clause rather than stating only the existence of an abstract order isomorphism.

The result is known mathematics, while the Lean declaration supplied here is statement-only and retains sorry as its proof placeholder. The formalization contribution is therefore a precise target and its expression-essential vocabulary, not a claim that Shemer's proof has already been machine checked. A completed proof must establish exactly this uniform reconstruction theorem without adding metric hypotheses or restricting the allowed subsets.

Where the difficulty lies

The parent face-poset isomorphism directly identifies the faces already present in $P$ and $Q$, but a subpolytope can have faces that are not faces of its parent. Consequently, restricting $\Phi$ to selected vertices does not automatically yield the required subpolytope face-poset isomorphism. The theorem must control how all new faces created by taking a vertex subset depend on the original neighborly combinatorics. That gap is the substantive content of rigidity and prevents the conclusion from being a routine restriction of the given parent isomorphism.

Formalization scope

The scope is deliberately narrow. IsDPolytope, IsKNeighborly, and PolytopeFace are the only local definitions required to express the theorem. Vertices are exposed singletons, combinatorial types are full face-poset order types, and convex hulls remain in the original ambient space even when a selected subset is lower-dimensional. The theorem assumes positive even dimension through $2r$ with $r \ge 1$. It imposes no metric congruence, no choice of realization normal form, and no cardinality lower bound on the selected subset.

Useful contributions include a proof of the stated target and reusable lemmas connecting neighborliness, vertex subsets, and exposed-face posets. A reformulation that covers only nonempty or full-dimensional subsets, forgets the prescribed vertex labels, or replaces face-poset equivalence by equality of face counts would not satisfy this mission.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, especially §§2.4, 3.1–3.2, 7.1–7.2, and 7.5. DOI

Motivation

A basic classification question in polytope theory asks what combinatorial types can occur when the dimension and number of vertices are fixed. The question is not merely whether there are finitely many types. Effective enumeration asks for a uniform algorithm which produces the complete list, with no omissions and no repeated combinatorial type. This converts a structural finiteness assertion into a finite procedure that can in principle support tabulation, comparison, and exhaustive study of small polytopes.

Grünbaum formulates this enumeration problem in §5.5 of Convex Polytopes and states its solvability as Theorem 5.5.2, printed p. 91 (PDF p. 117 of the supplied source). The surrounding discussion represents a combinatorial type by a finite scheme recording which subsets of labelled vertices form proper faces. The source then selects one representative for every realizable type. This mission follows that statement and encoding, as recorded in the supplied edition of the book (Springer DOI).

Setting

Fix natural numbers $d$ and $k$. A $d$-polytope is a nonempty finite convex hull in real coordinate space $\mathbb R^d$ whose affine span is the whole space. Its faces are exposed faces. Following Grünbaum's convention, this includes the empty face and the polytope itself as improper faces. The natural-valued function $f_j(P)$ counts nonempty exposed faces whose affine direction has dimension $j$; in particular, $f_0(P)$ is the number of vertices.

A finite scheme is encoded as a list $S$ of lists of natural numbers. Each inner list represents a finite subset of vertex labels; its order and repeated entries have no mathematical meaning. The predicate SchemeRealizes k S P supplies an injective labelling $V:\operatorname{Fin}(k)\to\mathbb R^d$ whose range is exactly the set of exposed singleton vertices of $P$. For every finite subset $J$ of natural numbers, membership of $J$ in the scheme is equivalent to the existence of a nonempty proper exposed face whose labelled vertices are exactly $J$. Quantifying over every finite natural-number subset prevents an out-of-range label from silently denoting a face.

Two polytopes have the same combinatorial type when their complete face posets are order-isomorphic. The Lean subtype PolytopeFace P contains every exposed face of $P$, including the two improper faces, and inherits the inclusion order. Thus Nonempty (PolytopeFace P ≃o PolytopeFace Q) is the formal equivalence relation used in the target.

Formalization target

The target is Grünbaum's Theorem 5.5.2 (book record and DOI). In Lean it states that there is a single function

$$E:\mathbb N\to\mathbb N\to \operatorname{List}(\operatorname{List}(\operatorname{List}(\mathbb N)))$$

which is computable and has the required behavior for every $d$ and $k$. Its finite output $E(d,k)$ satisfies three clauses. First, every output scheme is realized by some $d$-polytope. Second, every $d$-polytope with $k$ vertices realizes an output scheme. Third, if realizations of two output positions have order-isomorphic complete face posets, then those positions are equal. The three clauses jointly express soundness, completeness, and selection of a single representative per combinatorial type.

The theorem is Grunbaum2003.combinatorial_types_effectively_enumerable. Its body is an intentional sorry: this package supplies the reviewed, compiling statement and does not claim a machine-checked proof.

Significance

The conclusion gives more than abstract finiteness. It asserts one terminating procedure, uniform in both parameters, whose finite result represents all and only the desired types. Soundness prevents junk schemes; completeness prevents a legitimate polytope type from being missed; uniqueness prevents the output from counting the same type twice under different label lists. The theorem thereby isolates the precise data that an implementation or a formal proof must justify.

A formal proof would connect geometric realizability, finite incidence data, and computability in one development. The reusable infrastructure includes a full-dimensional finite-hull predicate, exposed-face counting, the complete exposed-face poset, and a labelled finite-scheme realization predicate. These definitions can also support formal statements about realization tests and enumerations under additional restrictions, without changing this mission's source obligation.

Difficulty

Finite syntactic generation alone is insufficient: most arbitrary families of vertex subsets need not be face systems of convex polytopes. Conversely, merely knowing that only finitely many combinatorial types exist does not provide an effective method for recognizing realizable schemes. The target must establish a total algorithm while simultaneously proving that every accepted scheme is geometrically realizable, every eligible polytope is represented, and no two selected entries encode order-isomorphic face posets.

Vertex relabelling is another source of redundancy. Two different nested lists can describe the same incidence structure, and two different geometric realizations can have the same face lattice. The uniqueness clause therefore compares realized complete face posets rather than list equality. A procedure that only enumerates labelled presentations, or one that decides equivalence without selecting representatives, would not prove the stated theorem.

Formalization scope

The Lean function $E$ returns nested finite lists, so finiteness of each output and of each scheme is built into the type. Mathlib's Computable₂ supplies total computability on the paired natural inputs. The quantifier order chooses one $E$ before $d$, $k$, and any polytope, preserving uniformity. No rational-coordinate, simplicial, or fixed-combinatorics hypothesis is introduced.

IsDPolytope requires a nonempty finite convex hull with full affine span. faceCount P 0 = k imposes the prescribed vertex count. SchemeRealizes requires exactly the exposed singleton vertices and exactly the nonempty proper exposed faces under an injective finite labelling. PolytopeFace retains the empty and full improper faces for the final order-isomorphism comparison. These choices prevent the statement from becoming vacuous through an unconstrained incidence code or a predicate that assumes realizability.

Natural-number boundary cases remain explicit. If no $d$-polytope with $k$ vertices exists, an empty output is permitted. In dimension zero, the unique point has one vertex and no nonempty proper face, so the empty scheme represents it. This coding extension does not remove any positive-dimensional case. The expression dependencies are exactly the four definitions listed above; proof-only lemmas and unrelated theorems from the book are not included as mission items.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., prepared by Volker Kaibel, Victor Klee, and Günter M. Ziegler, Graduate Texts in Mathematics 221, Springer, 2003. §5.5, especially Theorem 5.5.2 on printed p. 91 / supplied PDF p. 117. https://doi.org/10.1007/978-1-4613-0019-9

Motivation

A convex set can be studied through its images in lower-dimensional spaces. Each image retains part of the geometry while discarding information along the directions that are collapsed. Finite convex hulls behave well under affine maps: the image of a convex hull of finitely many points is again the convex hull of finitely many points. The converse is subtler. It asks whether sufficiently comprehensive lower-dimensional image data forces the original bounded convex set itself to have a finite description by points.

This mission formalizes the projection-recognition criterion attributed to Klee in Branko Grünbaum's Convex Polytopes, second edition, §5.1, Theorem 5.1.8, printed page 74 (PDF page 100 of the supplied source). The criterion concerns every projection into one suitable intermediate dimension, not a chosen coordinate view. It therefore characterizes a global property of the original set by an entire family of dimension-reducing images.

Setting

Fix a natural number $d\geq 3$. Real coordinate space $\mathbb R^d$ is represented in Lean by functions from Fin d to the real numbers. A subset $K\subseteq\mathbb R^d$ is convex when it contains every line segment joining two of its points, and it is bounded when all of its points lie within some finite metric ball. Neither condition requires $K$ to be nonempty, closed, or full-dimensional.

For a set $V$, its convex hull $\operatorname{conv}(V)$ is the smallest convex set containing $V$. In the convention used by Grünbaum in §3.1, printed page 31 (PDF page 51), a polytope is equivalently the convex hull of a finite set. The generating set need not be a minimal vertex set, and the formal statement permits the finite set to be empty or contained in a proper affine subspace.

An affine map preserves affine combinations. A surjective affine map

$$f:\mathbb R^d\longrightarrow\mathbb R^j$$

has image dimension exactly $j$. When $j<d$, it is singular. Grünbaum defines a projection at the opening of §5.1, printed page 71 (PDF page 97), as an image under a singular affine map. Using a surjective affine map to coordinate $j$-space represents a projection to a $j$-dimensional affine space followed by an affine choice of coordinates. Whether a set is a finite convex hull is unchanged by that coordinate identification.

Formalization target

For every bounded convex set $K\subseteq\mathbb R^d$, the target is the equivalence

$$K\text{ is a polytope} \quad\Longleftrightarrow\quad \exists j\in\mathbb N,\;2\leq j<d,\; \forall f:\mathbb R^d\twoheadrightarrow\mathbb R^j\text{ affine},\; f(K)\text{ is a polytope}.$$

The dimension $j$ may depend on $K$, but it is selected before the universal quantifier over affine maps. Every surjective affine map with that target dimension is tested. For each map, the finite set whose convex hull is $f(K)$ may be different; no common projected generator set and no uniform bound on its size is asserted. This is one theorem with both directions, so there are no separate milestone statements in the package.

Significance

The forward implication records the stability of finite convex hulls under affine images. The recognition implication is the substantive part: under boundedness and convexity, polytopality of every projection in one eligible intermediate dimension forces $K$ itself to be a polytope. The conclusion concerns $K$ rather than merely its closure and does not add a hidden closedness assumption.

The theorem is established mathematics in the cited textbook. The present artifact is a compiled formal statement, not a completed machine-checked proof: its theorem body is by sorry. Completing it would connect Mathlib's finite convex-hull and affine-map infrastructure to the classical projection-recognition argument while preserving the source's quantifier order and lower-dimensional boundary cases.

Difficulty

Each projected set may have its own unrelated finite generating set. Those separate witnesses do not directly assemble into a finite generating set in the original ambient space, because every projection has discarded a kernel direction. Checking one convenient projection is inadequate: that image can conceal structure occurring precisely in the collapsed directions. The challenge is therefore to use the universal family of projections at the selected dimension without replacing it by a fixed axis projection or adding compactness, full dimensionality, or nonempty interior.

Formalization scope

The Lean declaration is Grunbaum2003.polytope_iff_polytope_projections, in the book-wide namespace Grunbaum2003. It takes Bornology.IsBounded K and Convex ℝ K as the exact domain hypotheses. Polytopality is written directly as existence of a finite set with convex hull equal to the set; no stronger book-local full-dimensional polytope predicate is used. Projections are all surjective real affine maps from Fin d → ℝ to Fin j → ℝ.

The explicit premise $3\leq d$ records the admissible ambient range required by $2\leq j<d$. In dimension three, the only possible target dimension is two. No displayed existential claim is made for dimensions zero, one, or two, where no such $j$ exists. Within every admissible dimension, empty sets, singletons, and other lower-dimensional bounded convex sets remain in scope. Surjectivity prevents a map from having rank below $j$, and the strict inequality $j<d$ ensures dimension loss. There are no expression-essential book-local definitions or supporting theorems; the only dependencies are Mathlib modules for convex hulls, boundedness, finite-dimensional coordinate spaces, and affine maps.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, §3.1 and §5.1, especially Theorem 5.1.8 on printed page 74. Springer book record and DOI.

Motivation

The face structure of a cube is unusually regular: its vertices, edges, and higher dimensional faces are indexed by choices of fixed and free coordinates. A natural realization question asks how much of this structure can survive in a polytope of lower dimension. In §4.9 of Convex Polytopes, Grünbaum reports the Joswig–Ziegler construction of neighborly cubical polytopes. The source result says that a cubical $d$-polytope can retain a prescribed low dimensional skeleton of an $n$-cube even when $n>d$. It concerns the entire pattern of faces and containments within that skeleton, rather than a count of vertices or edges alone. The theorem appears on printed page 69b (PDF page 95) of the supplied 2003 edition.

Setting

Fix natural numbers $n>d\geq2$. A $d$-polytope here is a nonempty finite convex hull $P\subseteq\mathbb R^d$ with full affine span. A face is an exposed subset of $P$; the empty face and $P$ itself are included in the face poset. Its order is set inclusion. For a nonempty face, dimension is the dimension of its affine span. The standard $n$-cube is $[0,1]^n$ in $\mathbb R^n$, described coordinatewise by $0\leq x_i\leq1$.

A cubical $d$-polytope is such a full dimensional polytope whose every facet, meaning every nonempty exposed face of dimension $d-1$, has a full face poset order isomorphic to the face poset of a standard $(d-1)$-cube. This is combinatorial cubicality: a facet need not be congruent or affinely equal to a metric cube. It also does not say that the vertices of $P$ have binary coordinates.

The $k$-skeleton face poset consists of the empty face together with all exposed faces of affine dimension at most $k$, with their inherited inclusion order. The source speaks of a skeleton “of” an $n$-cube: the intended correspondence preserves and reflects face containment across the two ambient dimensions. An order isomorphism of the two skeleton face posets is the Lean expression of that combinatorial equivalence.

Formalization target

The single target is the unnumbered Joswig–Ziegler existence theorem as reported by Grünbaum. For every $n>d\geq2$, with $k=\lfloor d/2\rfloor-1$, it asks for a cubical $d$-polytope $P$ such that

$$\operatorname{Skel}_k(P)\cong\operatorname{Skel}_k([0,1]^n).$$

The witness $P$ may depend on both $n$ and $d$. The strict inequality $n>d$ and lower bound $d\geq2$ are source conditions. They have not been expanded or narrowed for this package. For $d=2$ and $d=3$, the cutoff is zero, so the skeleton includes the empty face and vertices. At larger dimensions the claim includes all faces through the stated cutoff and their order relations.

In Lean the theorem is Grunbaum2003.neighborly_cubical_realization. Its conclusion supplies a set in Fin d → ℝ, proves the cubical-polytope predicate of that set, and supplies a nonempty type of order isomorphisms between the two skeleton face posets. The declaration is a compiled statement with a sorry body. No machine-checked proof of the existence theorem is claimed here.

Significance

This theorem separates dimension of realization from the low dimensional combinatorics being realized. In particular, an $n$-cube skeleton can occur inside a lower dimensional cubical polytope, subject to the precise cutoff above. The conclusion is a structural face-poset match, not a numerical face-vector equality. A complete formal proof would establish an existence statement about genuine full dimensional convex polytopes and an order equivalence of their truncated face systems.

The reusable formal objects in this package are the full dimensional polytope predicate, the face subtype, the skeleton subtype, the standard cube, and the cubical-polytope predicate. They express the geometry and combinatorics independently of the particular neighborly realization theorem. The goal is kept as one mission because the source states one dimension-parametric existence result; the definitions are only its expression dependencies.

Difficulty

A lower dimensional realization cannot retain every face of a higher dimensional cube. The theorem therefore specifies exactly which dimensions of faces can be preserved. Merely matching the number of vertices would leave edges, higher faces, and incidence unconstrained. Likewise, requiring all facets to look like cubes says nothing by itself about whether a large cube's skeleton appears. A proof must produce a genuine cubical witness and the ordered skeleton correspondence simultaneously, for every allowed pair of dimensions.

Formalization scope

The Lean coordinate spaces are real functions on Fin d and Fin n. Natural division d / 2 is floor division, and the assumption $d\geq2$ makes natural subtraction by one agree with the source's integer cutoff. The full dimensional condition rules out an empty or lower dimensional witness. IsExposed supplies faces, including the improper empty and whole faces; the skeleton predicate treats the empty face explicitly because its conventional dimension is $-1$, outside natural-number dimensions. The nonempty face dimension is the finrank of the affine direction.

The face-poset order is inherited from set inclusion. Cubicality is checked on each qualifying facet by an order isomorphism with the full face poset of the reference cube. The target's order isomorphism similarly covers the whole selected skeleton rather than only vertices. Contributions toward a proof may introduce construction and comparison lemmas, but none is asserted as an additional theorem item in this reviewed package.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Springer, 2003, §4.9, unnumbered Joswig–Ziegler existence theorem, printed p. 69b / PDF p. 95 of the supplied source.pdf.
• Michael Joswig and Günter M. Ziegler, “Neighborly cubical polytopes,” 2000, arXiv:math/9812033. This is corroboration for the construction; the mission retains Grünbaum's stated parameter range.

Motivation

A polytope may be described by its vertices or by its facets. These descriptions can differ sharply in size even when every vertex has only binary coordinates. Grünbaum's account of 0/1-polytopes in §4.9 records a result of Bárány and Pór: the maximal number of facets grows superexponentially with dimension. The result is an existence statement about the geometry of binary coordinate sets. The source describes random polytopes as witnesses, without specifying a probability distribution as part of the theorem.

Setting

Fix a dimension $d$. A $d$-polytope here is a nonempty convex hull of finitely many points in $\mathbb R^d$ with full affine span. A 0/1-polytope is the convex hull of a subset of $\{0,1\}^d$. Both properties are required of the witness. A facet is a nonempty exposed face of affine dimension $d-1$. The count $f_{d-1}(P)$ uses the book's convention that the empty face has dimension $-1$ and is excluded from natural-indexed face counts. This representation follows Grünbaum §§2.4 and 3.1 for faces and full-dimensional polytopes, and §4.9 for the binary coordinate family.

Formalization target

The single source obligation is the unnumbered Bárány–Pór assertion quoted by Grünbaum in §4.9, printed p. 69a (PDF p. 94). In mathematical notation, the statement is

$$\exists c>1\;\exists D\geq 2\;\forall d\geq D\;\exists P\subseteq\mathbb R^d:\quad P\text{ is a full-dimensional 0/1-polytope}\quad\text{and}\quad c^{d\log d}<f_{d-1}(P).$$

The constant $c$ and threshold $D$ are chosen before $d$; the witness $P$ may depend on $d$. The logarithm in Lean is natural logarithm. Changing a fixed logarithm base rescales the existential constant. The result is asymptotic: it does not assert the inequality in every small dimension. The threshold $D\geq2$ also keeps the natural-number expression $d-1$ in the facet dimension away from underflow.

The goal item Grunbaum2003.barany_por_binary_facet_growth carries this entire obligation. Its body is sorry, so the package presents a compiled statement, not a machine-checked proof. There are no separate source lemmas in this mission and no milestones to assert beyond the goal.

Significance

The theorem shows that binary vertex coordinates do not impose a merely exponential ceiling on the number of facets. It gives a family of full-dimensional binary polytopes whose facet counts eventually exceed an expression of the form $c^{d\log d}$ for one fixed $c>1$. A formal proof would establish that family in the chosen polytope and face-count representation. The present statement makes the quantifier order, full-dimensionality, binary-coordinate restriction, and strict facet inequality explicit for such a proof.

Difficulty

The existence of many binary vertices alone does not certify many facets: one must establish distinct supporting faces of codimension one. The source attributes the strong lower bound to a random construction. A proof must connect that construction to the geometric facet count while keeping one constant valid for every sufficiently large dimension. The mission statement leaves the construction method to the proof, as the quoted book assertion supplies no probability-space parameters or probability bound.

Formalization scope

Lean represents a point of $\mathbb R^d$ by Fin d → ℝ and a polytope by a set of such points. IsDPolytope requires a finite nonempty convex-hull presentation and full affine span. IsZeroOnePolytope requires a convex-hull presentation whose generators have every coordinate equal to zero or one. faceCount P k uses the finite cardinality of nonempty exposed faces of affine dimension $k$; for the full-dimensional witness, faceCount P (d - 1) is the facet count. No face-finiteness, simplicity, or probabilistic assumption is added to the theorem.

The package uses these three expression-essential definitions and the Mathlib real-power and logarithm notation. IsDPolytope and faceCount match the definitions already staged for other missions in this textbook series. A proof may reuse geometric lemmas or supply a new formal version of the Bárány–Pór construction, provided it proves the stated inequality for the original full-dimensional binary family.

Selected references

• Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §§2.4, 3.1, 4.9, printed pp. 17, 31, 69a (supplied source.pdf, PDF pp. 35, 51, 94).
• Imre Bárány and Attila Pór, “On 0–1 Polytopes with Many Facets,” Advances in Mathematics 161 (2001), 209–228, Theorem 1.1, p. 210. https://www.renyi.hu/~barany/cikkek/86.pdf

Motivation

A polytope can be given by a list of vertices, a list of inequalities, or much less explicit access. The last case arises when geometric information is available through queries to a physical or computational object but a full description is unavailable. Grünbaum's account of a result by Gritzmann, Klee, and Westwater asks how much of a polytope can be recovered when each query shoots a ray from a known interior point and reports where it meets the boundary. The target is the complete face lattice, including incidence among faces of every dimension, and the cost is the number of oracle calls. The result appears in Convex Polytopes, §3.6, printed pp. 52b–52c (PDF pp. 74–75 of the supplied source).

Setting

Fix a positive integer $d$. A $d$-polytope $P$ is a nonempty finite convex hull in real coordinate space $\mathbb R^d$ whose affine span is the whole space. The origin is known to lie in the interior of $P$. A ray query supplies a nonzero direction $v$; the oracle returns the intersection of the positive ray $\{tv:t>0\}$ with the boundary of $P$. The theorem requires this boundary-point property for every nonzero direction. It does not give the reconstruction program the vertices, inequalities, face counts, or coordinates of $P$.

A face is represented by an exposed subset of $P$, ordered by inclusion. The resulting face lattice includes the empty and whole faces. For $0\leq k<d$, $f_k(P)$ counts nonempty faces of affine dimension $k$; hence $f_0(P)$ is the vertex count and $f_{d-1}(P)$ is the facet count. The empty face has dimension $-1$ in the book's convention and is excluded from these natural-indexed counts. These conventions follow Grünbaum §§2.4 and 3.1 (printed pp. 17 and 31; PDF pp. 35 and 51).

Formalization target

The single source obligation is the unnumbered Gritzmann–Klee–Westwater theorem of Grünbaum §3.6. For each $d>0$, one finite exact-real ray-query program works for every eligible $P$ and every correct ray oracle for $P$. It halts with an encoding of the entire face lattice after at most

$$f_0(P)+(d-1)f_{d-1}(P)^2+(5d-4)f_{d-1}(P)$$

queries. The square on the facet count, both coefficients, and the continuation of “queries” across the page break are part of the printed statement. The program is selected before the unknown polytope and its oracle. The finite running time and output may depend on the instance. No common output, fixed runtime bound, or bit-complexity bound is asserted.

The Lean declaration is Grunbaum2003.ray_oracle_face_lattice_reconstruction. It asserts existence of the program, universal correctness, finite termination in a halt instruction, the displayed query inequality, and a concrete encoding of the whole face lattice. Its body is sorry: this package is a compiled statement and does not claim a machine-checked proof.

Significance

The conclusion recovers all face incidences from boundary samples on rays from one interior point. It is stronger than recovering only a vertex or facet list because the output explicitly determines the ordering of all faces. The bound measures the information requested from the oracle; the source does not constrain the number of internal arithmetic steps. A formal proof would connect the geometric reconstruction argument to a precise query machine and establish that its output matrix has exactly the claimed faces and inclusions.

Difficulty

Ray answers are geometric points, while the desired output is a global combinatorial structure. Sampling one direction per visible feature gives no direct certificate that all faces and incidences have been found. In particular, a proposed reconstruction must use only the permitted oracle answers and still know when its finite description is complete. The theorem also needs a uniform program for every polytope in a fixed dimension, with the instance dependent query count above. The present statement makes these quantifier and resource requirements explicit.

Formalization scope

The machine has a finite instruction list for rational constants, exact real arithmetic, sign branches, tape movement, oracle queries, and halt. Its tape begins at zero. A query reads a nonzero direction from the tape and writes back the oracle's boundary answer; only this instruction increments the query counter. A zero direction, invalid label, or division by zero fails instead of creating a successful execution. Thus an unrestricted oracle value at zero cannot certify the theorem. Arithmetic and sign tests are exact real operations, matching the source's query model rather than imposing a bit model.

The output is a self-delimiting Boolean inclusion matrix indexed by a finite type. A bijection connects its indices to all exposed faces of $P$, and each matrix entry is one precisely when the associated faces are ordered by inclusion. This rules out an output consisting merely of face counts, vertices, or facets. IsDPolytope, faceCount, PolytopeFace, the ray-oracle predicate, machine syntax and execution, and the output predicate are the expression dependencies of the goal. The exposed-face subtype and full-dimensional polytope predicate are shared unchanged with this book's other staged missions. Contributions needed for a proof may include geometric face finiteness and reconstruction lemmas, but those are not added as unreviewed mission items here.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Springer, 2003, §§2.4, 3.1, 3.6, especially the unnumbered Gritzmann–Klee–Westwater theorem on printed pp. 52b–52c (supplied source.pdf, PDF pp. 74–75).
• P. Gritzmann, V. Klee, and D. Westwater, original result cited by Grünbaum as Theorem 5.5 (1995), p. 715. This package follows Grünbaum's stated theorem; the original article was not independently inspected for this packaging step.

Motivation

Every consistency guarantee for an empirical-risk-minimization procedure — the Lasso, kernel ridge regression, maximum likelihood — ultimately rests on relating an empirical average to its population expectation, uniformly over the class of candidate functions or parameters being searched. Chapter 4 established the classical form of this connection: a uniform law of large numbers, bounding $\sup_{f\in F}|\|f\|_n^2-\|f\|_2^2|$ by an absolute quantity governed by the (unlocalized) complexity of $F$. Such a bound is often wasteful: it treats a function with small population norm the same as one with large population norm, when intuitively the empirical and population norms of a small function should already agree closely. This mission formalizes the sharper, localized form of this uniform law — the same localization principle Chapter 13 used for nonparametric least squares, now applied directly to the empirical-versus-population norm comparison itself, giving relative rather than absolute control and recovering optimal convergence rates that the unlocalized theory misses.

Setting

Fix a probability distribution $P$ over a covariate space $X$ and $n$ i.i.d. samples $x_1,\dots,x_n\sim P$. For $f:X\to\mathbb R$, the population norm is $\|f\|_2^2:=\int_Xf(x)^2\,P(dx)$ and the empirical norm is $\|f\|_n^2:=\frac1n\sum_{i=1}^nf(x_i)^2$; by linearity of expectation, $\mathbb E[\|f\|_n^2]=\|f\|_2^2$, so the question is how tightly $\|f\|_n^2$ concentrates around $\|f\|_2^2$, uniformly over a function class $F$. A class $F$ is star-shaped around the origin if $f\in F,\alpha\in[0,1]\implies\alpha f\in F$, and $b$-uniformly bounded if $\|f\|_\infty\le b$ for every $f\in F$. The relevant complexity measure is the population localized Rademacher complexity

$$R_n(\delta;F) := \mathbb E_{\varepsilon,x}\Big[\ \sup_{f\in F,\ \|f\|_2\le\delta}\ \Big| \tfrac1n\sum_{i=1}^n\varepsilon_if(x_i)\Big|\ \Big],$$

where $\varepsilon_1,\dots,\varepsilon_n$ are i.i.d. Rademacher signs independent of the samples — note that, unlike Chapter 13's Gaussian complexity for fixed design points, this expectation integrates out the randomness of the samples themselves, since this chapter treats $\{x_i\}$ as genuinely random throughout. A critical radius $\delta_n$ is any positive solution of $R_n(\delta;F)\le\delta^2/b$.

Formalization targets

Theorem 14.1 (goal). Given $F$ star-shaped and $b$-uniformly bounded, and $\delta_n$ solving the critical inequality, for any $t\ge\delta_n$,

$$\Big|\|f\|_n^2-\|f\|_2^2\Big|\le\frac12\|f\|_2^2+\frac{t^2}2 \qquad\text{for all }f\in F,$$

with probability at least $1-c_1e^{-c_2nt^2/b^2}$; and if additionally $n\delta_n^2\ge\frac2{c_2}\log(4\log(1/\delta_n))$,

$$\big|\|f\|_n-\|f\|_2\big|\le c_0\delta_n \qquad\text{for all }f\in F,$$

with probability at least $1-c_1'e^{-c_2'n\delta_n^2/b^2}$.

Significance

Theorem 14.1 is the technical engine behind two of the book's other sharp results: Example 14.2's derivation of the optimal $n^{-1/2}$ rate for bounded quadratic function classes (where the unlocalized analogue of this theorem only achieves the slower $n^{-1/4}$ rate), and, more broadly, every later argument in the book that needs to translate an empirical-norm guarantee (as produced directly by an M-estimator's optimality, e.g. Chapter 13's nonparametric least-squares bounds) into a population-norm guarantee, or vice versa. The gap between the "absolute" uniform law of Chapter 4 and the "relative" one here is exactly the difference between a bound that is only informative for functions of order-one population norm, and one that remains sharp arbitrarily close to the origin — which is precisely where a consistent estimator's error eventually lives. Formalizing the statement produces, for the first time on the platform, the localized-Rademacher-complexity vocabulary at the population level (as opposed to Chapter 13's fixed-design Gaussian-complexity version), reusable by any future mission needing to pass between empirical and population norms.

Difficulty

The naive approach — apply Hoeffding's inequality to $|\|f\|_n^2-\|f\|_2^2|$ for a fixed $f$, then union-bound (or apply the unlocalized Rademacher-complexity uniform law of Chapter 4) over $F$ — gives a bound whose complexity term does not shrink as $\|f\|_2\to0$, since it uses the complexity of all of $F$ regardless of a given function's own size. This is exactly the sub-optimality Example 14.2 exhibits concretely: the naive bound gives rate $n^{-1/4}$ where the truth is $n^{-1/2}$. The fix is not merely technical bookkeeping — it requires a genuine peeling argument over dyadic norm-scales (exactly as in Chapter 13's proof of Theorem 13.13), applying the localized complexity $R_n(\delta;F)$ at the scale $\delta=\|f\|_2$ appropriate to each individual $f$, and controlling the resulting geometric sum of tail probabilities across scales. A reader's first instinct — bound $\|f\|_2$ in terms of $\|f\|_n$ and substitute — is circular, since $\|f\|_n$ is itself the random quantity being controlled.

Formalization scope

The covariate space X carries an arbitrary MeasurableSpace structure (no topology needed for the statement); the sample sequence and the Rademacher signs are both represented as families of measurable functions on a shared probability space Ω, with their joint independence stated as a single IndepFun between the two vector-valued sequences (rather than building a combined-index iIndepFun), since it is the two sequences — not each pair of individual variables — whose independence the book invokes. The two conclusions of Theorem 14.1 are stated as a conjunction with the second gated behind its own extra hypothesis, never collapsed into a single implication, since the book's own statement keeps them syntactically and logically distinct (the second requires a strictly stronger and additional condition on top of the first's). The universal constants (c1,c2,c0,c1',c2') are quantified before every instance object, so they cannot secretly depend on the function class, sample size, or radius. Every f ∈ F is required measurable (hF_meas, added in revision): the book's own framing implicitly restricts to measurable, square-integrable f throughout (p. 454), and without this hypothesis the population norm popNormSq, which appears directly in the goal's conclusion, could silently take Mathlib's Bochner-integral junk value 0 for a non-measurable, pointwise-bounded member of a star-shaped, uniformly-bounded F. The trivializing formalization ruled out here is stating the localization constraint at the empirical rather than population norm in popRademacherComplexity — this chapter's whole point (contrast Chapter 13's Gn, correctly localized at the empirical norm since there the design is fixed) is that $R_n(\delta;F)$'s localization is a population-level object, precisely because the samples are random here. Welcome future contributions: Corollary 14.3's covering-number sufficient condition for the empirical version of the critical inequality, and Theorem 14.20's Lipschitz/strongly-convex cost-function uniform law, both deferred from this mission (see STATUS.md) as they need substantial additional apparatus (metric entropy integrals; cost functions and strong convexity) beyond what Theorem 14.1 itself requires.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 14. https://doi.org/10.1017/9781108627771
• P. Bartlett, O. Bousquet and S. Mendelson, "Local Rademacher complexities," Annals of Statistics, 33(4):1497-1537, 2005. https://doi.org/10.1214/009053605000000282
• V. Koltchinskii, "Local Rademacher complexities and oracle inequalities in risk minimization," Annals of Statistics, 34(6):2593-2656, 2006. https://doi.org/10.1214/009053606000001019

Motivation

Many high-dimensional data sets — gene-expression profiles, sensor networks, social interactions — come with no natural ordering of variables, only pairwise dependencies whose structure is itself the object of interest. A graphical model encodes these dependencies as an undirected graph: vertices are variables, and edges mark direct (conditional) dependence. Recovering the graph from samples — graphical model selection — is a combinatorial problem masquerading as a statistical one: there are $2^{\binom{d}{2}}$ candidate graphs on $d$ vertices, far too many to search directly. For Gaussian data, however, graph structure is exactly the sparsity pattern of the inverse covariance (precision) matrix, which turns graph selection into $d$ coupled sparse-regression problems — one per vertex — each of which the Lasso theory of Chapter 7 already knows how to solve. This mission formalizes the theorem, due to Meinshausen and Bühlmann (2006), that shows this reduction actually works: solving $d$ independent Lasso problems and combining the results recovers the exact graph with high probability, at a sample complexity governed by the same kind of incoherence condition that governs Lasso support recovery itself.

Setting

An undirected graphical model on a finite vertex set $V$ pairs a graph $G=(V,E)$ with a random vector $X=(X_j)_{j\in V}$. Two equivalent structural properties connect $X$ to $G$ (Theorem 11.8, Hammersley-Clifford): $X$ factorizes according to $G$ if its density is a product of nonnegative functions, one per clique of $G$, each depending only on the variables in that clique (Definition 11.1); $X$ is Markov with respect to $G$ if, for every vertex cutset $S$ separating $V$ into disjoint pieces $A$ and $B$, the sub-vectors $X_A$ and $X_B$ are conditionally independent given $X_S$ (Definition 11.5). For a strictly positive density, these are the same condition.

For a zero-mean $d$-dimensional Gaussian vector with covariance $\Sigma^*$ and precision matrix $\Theta^*=(\Sigma^*)^{-1}$, the graph structure is exactly the support of $\Theta^*$: $(j,k)\in E \iff \Theta^*_{jk}\ne0$. The neighborhood $N(j):=\{k\mid(j,k)\in E\}$ of each vertex is itself a vertex cutset (separating $\{j\}$ from everything else), so the conditional independence $X_j\perp X_{V\setminus N^+(j)}\mid X_{N(j)}$ holds, and — by standard Gaussian conditioning — $X_j$ decomposes as a linear function of $X_{V\setminus\{j\}}$ plus independent Gaussian noise, with regression coefficients supported exactly on $N(j)$. Neighborhood regression exploits this directly: for each vertex $j$, solve the Lasso

$$\hat\theta_j \in \arg\min_{\theta\in\mathbb R^{d-1}}\ \frac1{2n}\|X_j-X_{\setminus\{j\}}\theta\|_2^2 +\lambda_n\|\theta\|_1,$$

read off $\hat N(j):=\{k\mid\hat\theta_{j,k}\ne0\}$, and combine the $d$ per-vertex estimates into a single edge set via the OR rule ($(j,k)\in\hat E_{\mathrm{OR}}$ iff $k\in\hat N(j)$ or $j\in\hat N(k)$) or the more conservative AND rule (iff both hold). The relevant incoherence condition, analogous to Chapter 7's, is stated for a positive definite matrix $\Gamma$ and subset $S$: $\Gamma$ is $\alpha$-incoherent with respect to $S$ if $\max_{k\notin S}\|\Gamma_{kS}(\Gamma_{SS})^{-1}\|_1\le1-\alpha$.

Formalization targets

Theorem 11.8 (Hammersley-Clifford). Factorizes G p ↔ IsMarkov G X P for any strictly positive density $p$.

Theorem 11.12 (goal — graph selection consistency). Suppose for every $j$, $\Sigma^*_{\setminus\{j\}}$ is $\alpha$-incoherent with respect to $N(j)$, and $|\!|\!|(\Sigma^*_{N(j),N(j)})^{-1}|\!|\!|_\infty\le b$. With $\lambda_n=c_0\frac1\alpha(\sqrt{\log d/n}+\delta)$, the neighborhood-Lasso estimate combined via either rule satisfies, with probability at least $1-c_2e^{-c_3n\min(\delta^2,1/m)}$:

$$\hat E\subseteq E \qquad\text{and}\qquad \forall (j,k):\ |\Theta^*_{jk}|\ge7b\lambda_n \implies (j,k)\in\hat E.$$

Significance

Theorem 11.12 is the statistical justification for one of the two standard approaches to Gaussian graphical model selection (the other being the penalized-likelihood "graphical Lasso" of §11.2.1). Its significance is computational as much as statistical: rather than solving one $d$-dimensional penalized-likelihood problem, neighborhood regression solves $d$ independent, embarrassingly parallel Lasso problems, each of dimension $d-1$ — a substantial practical advantage at scale, with (as this theorem shows) no loss in statistical guarantee. Formalizing it produces, for the first time on the platform, statement-level infrastructure for undirected graphical models (Hammersley-Clifford, the Markov property via vertex cutsets, neighborhood structure) together with the random-design analogue of the Lasso support-recovery machinery — a genuinely different technical regime from Chapter 7's fixed-design Lasso theory, since here the "design matrix" $X_{\setminus\{j\}}$ is itself Gaussian and statistically coupled to the response $X_j$ through the very covariance structure being estimated. As with the other missions in this series, only the statements are formalized here; the proofs (an extension of the primal-dual witness technique to random design, per the book's own proof sketch) are left as the draft goal for future proof contributions.

Difficulty

The proof of Theorem 7.21 (Chapter 7's Lasso support-recovery guarantee) is for a deterministic design matrix, with all randomness confined to the additive noise. Here the "design" $X_{\setminus\{j\}}$ is itself random and Gaussian, and — critically — it is statistically dependent on the very quantity ($N(j)$, encoded in $\Theta^*$'s support) the Lasso is trying to recover, since $X_{\setminus\{j\}}$'s own covariance structure is exactly what the incoherence condition constrains. The naive approach of just conditioning on the realized design matrix and invoking Theorem 7.21 fails, because the deterministic-design incoherence condition would then need to hold for the sample covariance $\Gamma=\frac1n X_{\setminus\{j\}}^TX_{\setminus\{j\}}$, not the population covariance $\Sigma^*_{\setminus\{j\}}$ that is actually assumed — and controlling the gap between sample and population incoherence under the joint (not fixed) randomness of predictors and response is exactly the extra step the book's proof needs, handled via an extension of the primal-dual witness technique that tracks both sources of randomness together.

Formalization scope

The vertex set V is an arbitrary finite type; the covariate space for X is ℝ throughout (all variables jointly Gaussian). The Gaussian design is characterized via its one-dimensional projections (every linear combination is univariate Gaussian with the matching variance) rather than via Mathlib's multivariate-Gaussian machinery directly, to keep the definition self-contained. IsAlphaIncoherent's ambient index set is realized as a subset of the full vertex type rather than as a literal submatrix, since the book's condition never references an entry outside it. The theorem states the conclusion jointly for both the OR-rule and AND-rule estimated edge sets on one shared high-probability event, matching "based on either rule" literally rather than picking one. The trivializing formalization ruled out here is treating the neighborhood-Lasso estimate as a fixed-design Lasso problem (silently dropping the joint randomness of predictors and response) — every design realization in this formalization is the actual random vector Xdes i ω, not a deterministic parameter, and the Gaussian design hypothesis (IsIIDGaussianDesign) is stated over the same probability space Ω as the least-squares residual. Theorem 11.8 (Hammersley–Clifford) is formalized only for the continuous case — a random vector with a density with respect to Lebesgue measure — matching what the Gaussian goal (Theorem 11.12) actually needs; the book's own Definition 11.1 also permits a discrete (counting-measure) density, with the Ising model (Example 11.4) as a worked instance, which this mission does not cover. Contributions welcome: the graphical Lasso's own guarantees (Propositions 11.9, 11.10, deferred from this mission — see STATUS.md), and the proof of Theorem 11.12 itself via the primal-dual witness extension the book sketches.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 11. https://doi.org/10.1017/9781108627771
• N. Meinshausen and P. Bühlmann, "High-dimensional graphs and variable selection with the Lasso," Annals of Statistics, 34(3):1436-1462, 2006. https://doi.org/10.1214/009053606000000281
• J. Hammersley and P. Clifford, "Markov fields on finite graphs and lattices," unpublished manuscript, 1971.

Motivation

A striking fact discovered by Dvoretzky in the 1960s (conjectured by Grothendieck, and sharpened into its modern quantitative form by Milman in 1971) is that every high-dimensional convex body, however irregular, contains a round slice: a random low-dimensional section (or projection) of any bounded convex set in $\mathbb R^n$ is, with high probability, close to a Euclidean ball — provided the dimension of the slice is small enough relative to a single geometric parameter of the body. This is remarkable because it holds for every bounded set, arbitrarily irregular; no special structure is assumed beyond boundedness. This chapter proves the theorem in its Gaussian form, as a culmination of every geometric and probabilistic tool the book develops: chaining and Dudley's inequality (Chapter 8), the matrix deviation inequality (Chapter 9), and Gaussian width and the stable dimension (Chapter 7) all combine into a single closing argument.

Setting

Fix a subset $T\subseteq\mathbb R^n$. For a standard Gaussian vector $g\sim N(0,I_n)$, the Gaussian width of $T$ is $w(T) := \mathbb E\sup_{x\in T}\langle g,x\rangle$ (Chapter 7), and the stable dimension of a bounded $T$ is $d(T) := w(T)^2/\mathrm{diam}(T)^2$ up to an absolute constant factor (Definition 7.6.2) — a robust substitute for the ordinary linear-algebraic dimension of $T$, which can jump discontinuously under a small perturbation of $T$, unlike $d(T)$.

An $m\times n$ Gaussian random matrix with i.i.d. $N(0,1)$ entries is a random matrix $A$ each of whose $mn$ entries is an independent standard normal random variable.

Formalization targets

Goal (Theorem 11.3.3, Dvoretzky-Milman's theorem, Gaussian form)

$$\exists\,c>0:\quad m\le c\varepsilon^2 d(T) \;\Longrightarrow\; \mathbb P\bigl[(1-\varepsilon)B \subseteq \mathrm{conv}(AT) \subseteq (1+\varepsilon)B\bigr] \ge 0.99$$

for every $m\times n$ Gaussian random matrix $A$ with i.i.d. $N(0,1)$ entries, every bounded $T\subseteq\mathbb R^n$ containing the origin, and every $\varepsilon\in(0,1)$, where $B$ is the Euclidean ball of radius $w(T)$ centered at the origin. The probability $0.99$ is the book's own literal numeral, not a free parameter — this is the theorem the book actually states, not a family of theorems indexed by a confidence level.

Significance

Dvoretzky-Milman's theorem is one of the foundational results of the local theory of Banach spaces (asymptotic geometric analysis): it says every $n$-dimensional normed space contains an almost-Euclidean subspace of dimension proportional to (a geometric invariant closely related to) $\log n$ in the worst case, and much larger for spaces whose unit ball is already well-behaved (the stable dimension of the cube $[-1,1]^n$, for instance, is proportional to $n$ itself — Example 11.3.6). This underlies results throughout convex geometry, compressed sensing, and high-dimensional statistics wherever a random low-dimensional projection needs to be shown to preserve geometric structure. The book's own framing makes clear why this chapter is placed last: the theorem's proof is a genuine capstone, invoking Chevet's inequality (itself built from the matrix deviation inequality of Chapter 9, which is built from chaining, Chapter 8) as its main technical tool.

The theorem and its proof are classical (Milman 1971; this book's specific route via Chevet's inequality is a standard modern exposition). This mission formalizes the goal theorem's statement — including its two supporting geometric quantities, Gaussian width and stable dimension, and the notion of a Gaussian random matrix — as a complete, faithful target for a solver, in the book's own sub-namespace built for this chapter (no dependency here is reusable from an earlier chunk, since none of this book series' Chapter 7 or Chapter 9 definitions has yet been published).

Difficulty

The natural first idea — bound $\mathrm{conv}(AT)$ directly using concentration of $\|Ax\|_2$ for each fixed $x\in T$ — runs into exactly the uniform-supremum obstacle the whole book has been building tools to overcome: a bound that holds for one $x$ at a time, even with a union bound over a net of $T$, does not obviously extend to the full convex hull without first controlling $\sup_{x\in T}|\langle Ax,y\rangle - w(T)\|y\|_2|$ uniformly over both $x\in T$ and $y$ on the unit sphere of the target space — a two-parameter supremum. The book's actual route goes through Chevet's inequality, itself proved using the matrix deviation inequality's own chaining-based argument, to control this two-sided supremum, and then converts the resulting inequality into the containment $(1-\varepsilon)B\subseteq\mathrm{conv}(AT)\subseteq(1+\varepsilon)B$ via a support- function duality argument (a convex body is pinned down by its support function, so bounding $\sup_{x\in T}\langle Ax,y\rangle$ uniformly over $y$ on the sphere is exactly what is needed).

Formalization scope

A is Ω → Matrix (Fin m) (Fin n) ℝ with an explicit IsGaussianMatrix hypothesis (entries i.i.d. $N(0,1)$, formalized entrywise with joint independence). conv(AT) is convexHull ℝ of the image of T under A's mulVec, round-tripped through EuclideanSpace's continuous linear equivalence with the underlying function type. w(T) reuses this mission series' ExpSup/GaussianWidth convention (redefined locally, per the drafts-cannot-import-drafts rule, following the same ProbabilityTheory.stdGaussian-based realization of a standard Gaussian vector as 08-matrix-deviation). The stable dimension $d(T)$ is formalized directly as $w(T)^2/ \mathrm{diam}(T)^2$ rather than via the book's literal (but only asymptotically equivalent, per Exercise 7.6.1) definition through a squared Gaussian width $h(T-T)^2$ — the goal theorem's own proof uses only the inequality direction of that equivalence, and the goal's hypothesis already carries an unpinned absolute constant that absorbs the equivalence constant, so this substitution preserves the theorem's exact truth content (see StableDimension's own doc-comment and MODERATION_NOTES.md for the full argument) rather than approximating it.

Ball-center deviation, disclosed. The book's printed theorem statement carries no hypothesis that $T$ contains the origin; its proof opens by translating $T$ so that it does ("Translating $T$ if necessary, we can assume that $T$ contains the origin"), and Remark 11.3.4 then confirms the ball is centered at the origin in that case. This mission states the WLOG-reduced case directly — adding $0\in T$ as an explicit hypothesis — rather than also formalizing the translation argument that recovers the fully general (untranslated) statement. This is disclosed as a genuine narrowing of the literal printed statement, though not of what the book's own proof actually establishes.

This mission covers Theorem 11.3.3 only, with no milestones: BRIEF.md explicitly instructs that if the chapter's full proof chain (general matrix deviation inequality, Chevet's inequality, random projections of sets — Theorems 11.1.5, 11.2.4, 11.3.1) proves too heavy for the session, milestones should be cut rather than the goal substituted. All three are left out, not approximated, given this chapter's five from-scratch definitions already needed for the goal's own statement. ExpSup, GaussianWidth, StableDimension and IsGaussianMatrix are reusable by any later development needing Gaussian width, the stable dimension, or a Gaussian random matrix. Solvers' contributions are welcome on the goal theorem itself and, beyond this mission's current scope, on the three named milestones.

Selected references

• A. Dvoretzky, Some results on convex bodies and Banach spaces, Proc. Internat. Sympos. Linear Spaces (Jerusalem, 1960), 123–160.
• V. D. Milman, A new proof of A. Dvoretzky's theorem on cross-sections of convex bodies, Funkcional. Anal. i Priložen. 5 (1971), 28–37.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 11. https://doi.org/10.1017/9781108231596

Motivation

The central limit theorem says that $S_n/\sqrt n$ converges to a normal random variable. Donsker's theorem says something much stronger: the whole rescaled path of the random walk converges to the whole path of a Brownian motion, as a random element of $C[0,1]$.

The payoff is a machine. Once $S(n\cdot)/\sqrt n\Rightarrow B(\cdot)$ in $C[0,1]$, every functional of the path that is continuous — or merely continuous at almost every Brownian path — transfers automatically. The maximum of the walk converges to the maximum of Brownian motion; the fraction of time the walk spends above a level converges to the corresponding occupation time; the last zero before time $n$ converges to the last Brownian zero before time $1$, which is how the arcsine law escapes the simple random walk it was proved for. This is the invariance principle of Erdős and Kac: the asymptotic behaviour of a functional of $S_n$ should not depend on the step distribution, as long as the central limit theorem applies.

Chapter 8 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) proves this by embedding rather than by the usual tightness argument. Skorokhod's representation theorem puts a mean-zero, finite-variance random variable inside a Brownian motion as the value at a stopping time; iterating puts the whole walk inside one Brownian motion at a sequence of stopping times whose gaps are i.i.d.; and the law of large numbers then forces the embedded walk to be uniformly close to the Brownian path.

Setting

Let $X_1,X_2,\dots$ be i.i.d. with mean $0$ and variance $1$, and $S_m=X_1+\dots+X_m$. Define $S(u)$ to be $S_m$ at integer $u=m$ and linear in between, and set

$$W_n(t)\ =\ \frac{S(nt)}{\sqrt n},\qquad t\in[0,1],$$

a random element of $C[0,1]$, the continuous functions on the unit interval with the uniform norm and its Borel $\sigma$-algebra.

On the Brownian side, let $B$ be a Brownian motion, and write $B(\cdot)$ for its restriction to $[0,1]$, again a random element of $C[0,1]$.

Formalization targets

Goal — Theorem 8.1.4, Donsker's theorem

$$\frac{S(n\cdot)}{\sqrt n}\ \Longrightarrow\ B(\cdot)\qquad\text{in }C[0,1],$$

that is, the laws of $W_n$ on $C[0,1]$ converge weakly to the law of Brownian motion. This is a statement about measures on a function space, not about finite-dimensional marginals: it is exactly the extra content over the central limit theorem.

Supporting levels

Theorem 8.1.1, Skorokhod's representation theorem: a mean-zero, square-integrable law is the law of $B_T$ for a stopping time $T$ with $\mathbb ET=\mathbb EX^2$; Theorem 8.1.2, the embedding of the whole walk, giving stopping times $T_0=0,T_1,\dots$ with $(B(T_n))_n$ distributed as the walk and with i.i.d. gaps; Theorem 8.1.5, the continuous mapping theorem for almost surely continuous functionals; and its two workhorse instances, Example 8.1.6 on maxima and Example 8.1.8 on occupation times of half-lines.

Significance

The results themselves. Donsker's theorem is the reason the arcsine law, the distribution of the maximum, and the occupation-time law are universal rather than artefacts of the simple random walk for which they were first computed. It is also the prototype for every later functional limit theorem — for martingales in Durrett's section 8.2, for stationary sequences in 8.3, for the empirical process converging to a Brownian bridge in 8.4.

Skorokhod's embedding deserves separate billing. It says any centred law with finite variance sits inside Brownian motion, which is what makes the path-space comparison possible at all, and it is the tool behind the law of the iterated logarithm in Durrett's section 8.5. The construction is a two-point mixture: write the law as a mixture of two-point laws $\mu_{u,v}$ with mean zero, use the exit time of $(u,v)$ for each, and the exit-time identity $\mathbb ET_{a,b}=-ab$ integrates to $\mathbb EX^2$.

Formalizing them. Mathlib has the i.i.d. central limit theorem, convergence in distribution for random elements of an arbitrary topological space (TendstoInDistribution, with the continuous mapping theorem and Slutsky), Brownian motion as a process with its invariances, and the machinery of stopping times for filtered spaces. It has no functional limit theorem of any kind, no Wiener measure on $C[0,1]$, no Skorokhod embedding, and no continuous-time optional stopping. Nothing in the library relates a random walk to a Brownian path.

Difficulty

The goal is the hardest item in this series, and the embedding route is the reason the mission is stated the way it is. Durrett's proof: with $X_{n,m}=X_m/\sqrt n$ and stopping times $\tau^n_m$ realizing $(S_{n,1},\dots,S_{n,n})$ as $(B(\tau^n_1),\dots,B(\tau^n_n))$, Lemma 8.1.9 says that if $\tau^n_{\lfloor ns\rfloor}\to s$ in probability for each $s\in[0,1]$, then $\|S_{n,(n\cdot)}-B(\cdot)\|_\infty\to0$ in probability. The hypothesis is the weak law applied to the i.i.d. gaps of Theorem 8.1.2 after Brownian scaling; the conclusion plus the converging-together lemma gives the theorem. The work is uniform control of the Brownian path over shrinking time windows — the modulus of continuity — together with the bookkeeping of the polygonal interpolation.

Skorokhod's theorem needs the two exit-time facts for Brownian motion, Durrett's Theorems 7.5.3 and 7.5.5: $B_{T_{a,b}}$ takes the values $a$ and $b$ with probabilities $b/(b-a)$ and $-a/(b-a)$, and $\mathbb ET_{a,b}=-ab$. Both come from optional stopping applied to $B_t$ and $B_t^2-t$, and continuous-time optional stopping is itself not in the library. The mixture identity,

$$\int\varphi\,dF=c^{-1}\int_0^\infty dF(v)\int_{-\infty}^0 dF(u)\,(v-u) \Bigl[\tfrac{v}{v-u}\varphi(u)+\tfrac{-u}{v-u}\varphi(v)\Bigr], \qquad c=\int_0^\infty v\,dF(v),$$

is elementary but needs Fubini and the two expressions for $c$.

Theorem 8.1.5 is the Mann–Wald theorem in the form that allows a discontinuous $\psi$: Mathlib's TendstoInDistribution.continuous_comp handles genuinely continuous maps, and the extension to maps continuous almost everywhere with respect to the limit law is the milestone. Given it, the two examples are short — the maximum is continuous outright, and the occupation-time functional is continuous at every path spending no time at the level $a$, which Fubini shows is almost every Brownian path.

Formalization scope

$C[0,1]$ is C(Set.Icc (0:ℝ) 1, ℝ), whose compact-open topology is the uniform one because the domain is compact, with the Borel $\sigma$-algebra — Mathlib has no measurable-space instance on a space of continuous maps, so the mission supplies it, and a BorelSpace instance with it.

The polygonal interpolation is written as a finite sum,

$$S(u)=\sum_{k<n}X_k\cdot\operatorname{clamp}(u-k),\qquad \operatorname{clamp}(x)=\max(0,\min(1,x)),$$

which agrees with $S_m$ at integer $m\le n$ and is linear in between, and is manifestly continuous, so walkPath is a genuine element of $C[0,1]$ with no side condition. Both properties were proved in Lean before publishing rather than assumed. Indexing is from zero, so $S_m=X_0+\dots+X_{m-1}$.

The Brownian limit is brownianPath B, the restriction of the path to $[0,1]$. Restriction is a total function: it returns the zero path for a discontinuous argument. That junk branch is never reached, because every statement assumes every path of $B$ is continuous, not merely almost every one — one may always modify a Brownian motion on a null set to achieve this, and Durrett's canonical construction on $C[0,\infty)$ has it by definition. Without it there would be no $C[0,1]$-valued random variable to speak of.

Weak convergence is Mathlib's TendstoInDistribution, the same predicate mission II used for the Lindeberg–Feller theorem, instantiated at $C[0,1]$ rather than at $\mathbb R$.

Skorokhod's theorem and the embedding of the walk are stated as existence of a probability space carrying the Brownian motion, a filtration and the stopping times. This is how Durrett states them — the construction needs an independent pair $(U,V)$ alongside the Brownian motion, and he notes himself that $T_{U,V}$ is a stopping time only for the enlarged filtration. The filtration is therefore an explicit family $F_t$ that is increasing, sits inside the ambient $\sigma$-field, and contains $\sigma(B_s:s\le t)$ — the pastSigma of mission V, which this mission imports as a reference. The stopping-time property is {T ≤ t} ∈ F_t, stated directly rather than through a bundled filtration structure.

Theorem 8.1.2's conclusion "$S_n=_d B(T_n)$" is read as equality of the laws of the whole processes: the push-forward of $\omega\mapsto(n\mapsto B(T_n\omega))$ equals the law of the partial-sum process of an i.i.d. sequence with step law $\mu$, taken on the infinite product measure. The gaps are required to be independent and identically distributed, as the book says.

The counting in Example 8.1.8 is a sum of indicators rather than a filtered cardinality, to keep a decidability side condition out of the statement, and the limit is the Lebesgue measure of $\{t\in[0,1]:B_t>a\}$ as a real number. Example 8.1.6 takes the maximum over $0\le m\le n$, which includes $S_0=0$, and the limit is the supremum of $B$ over $[0,1]$, attained because the path is continuous on a compact interval.

Existence of a Brownian motion is a hypothesis, not a claim, exactly as in mission V, except in Theorems 8.1.1 and 8.1.2 where the existence of a suitable space is the content of the statement and a Brownian motion must be produced; that is Durrett's Theorem 7.1.1, which the library does not yet have, so those two items subsume it.

Contributions welcome beyond the listed items: Lemma 8.1.9 on its own; Theorem 8.1.3, the CLT derived from the embedding; Example 8.1.7, the last zero before time $n$ and the arcsine law; continuous-time optional stopping and the exit identities 7.5.3 and 7.5.5 that Skorokhod's theorem rests on; the extension to $C[0,\infty)$; and the martingale, stationary-sequence and empirical-process versions of sections 8.2 to 8.4.

Selected references

• Rick Durrett, Probability: Theory and Examples, Version 5 (11 January 2019), chapter 8, section 8.1 (pp. 389–395); Theorems 8.1.1, 8.1.2, 8.1.4, 8.1.5, Examples 8.1.6 and 8.1.8. Published as the 5th edition, Cambridge University Press, 2019, DOI 10.1017/9781108591034
• M. D. Donsker, An invariance principle for certain probability limit theorems, Memoirs of the American Mathematical Society 6 (1951).
• A. V. Skorokhod, Studies in the Theory of Random Processes, Addison-Wesley, 1965.
• P. Erdős and M. Kac, On certain limit theorems of the theory of probability, Bulletin of the American Mathematical Society 52 (1946), 292–302. DOI 10.1090/S0002-9904-1946-08560-2
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, chapters 2 and 8. DOI 10.1002/9780470316962

Motivation

Central values of twists of elliptic-curve and modular-form $L$-functions govern arithmetic questions ranging from Mordell--Weil ranks to the distribution of nonvanishing twists. Classical Iwasawa theory organizes twists whose conductors grow vertically through powers of one prime. Kriz and Nordentoft introduce a horizontal analogue in which the order of the character is fixed while its conductor acquires new prime factors. Their paper Horizontal p-adic L-functions constructs measures encoding these twists and proves a structure theorem that forces quantitative nonvanishing.

The mission formalizes the paper's common mechanism behind its nonvanishing theorems: Fourier theory of horizontal measures, norm-compatible modular-symbol theta elements, interpolation of central values, and propagation from nonzero measures to logarithmic-power lower bounds. The elliptic-curve statements in Theorems 1.1 and 1.2 are obtained in the paper by specializing this mechanism to weight-two newforms and adding the stated Galois-representation hypotheses.

Setting

Fix a prime $p$. The digit group is the compact product

$$G_p=\prod_{n\ge 0}\mathbf Z/p\mathbf Z.$$

A continuous character of $G_p$ has finite image and factors through a finite product. For a complete algebraically closed nonarchimedean field $K$ of residue characteristic $p$, a horizontal measure is represented in Lean by a continuous $K$-linear functional on the Banach space $C(G_p,K)$. Its Fourier transform is

$$\widehat\nu(\chi)=\int_{G_p}\chi\,d\nu.$$

The integral measures arising from the digit Iwasawa algebra have Fourier norms in a discrete geometric lattice. This is recorded explicitly by HasDiscreteFourierNorm; it is the norm-language counterpart of the discrete valuation hypothesis used in Corollary 2.9.

On the arithmetic side, modular symbols produce theta elements at finite squarefree conductors. Their projection maps do not initially form a compatible inverse system: an Euler factor appears each time a prime is removed. At an orderly prime this factor is a unit, so normalization produces a compatible system and hence a horizontal $p$-adic $L$-function. Evaluation at a character gives the modified central $L$-value of the corresponding twist.

Formalization targets

Finite-correction structure and interpolation

For every nonzero integral horizontal measure $\nu$, there is a finite set $M_\nu$ of characters and a constant $c>0$ such that

$$\lvert\widehat\nu(\chi\chi_0)\rvert_p=c$$

for some $\chi_0\in M_\nu$, for every continuous character $\chi$. If $\nu$ interpolates modified central values, these corrected values are nonzero and have optimal $p$-adic size. This is Theorem 1.6, equivalently the digit-algebra case of Corollary 2.9, combined with Corollary 5.4.

Elliptic-curve specialization

For a modular elliptic curve over $\mathbf Q$, the normalized theta system is assembled into the horizontal $p$-adic $L$-function of Definition 5.3 and shown to satisfy Corollary 5.4. The final milestones then specialize the structure and propagation theorems to prove Theorems 1.1 and 1.2 (assuming modularity), retaining the three alternative hypotheses of Theorem 1.1 and the jointly-good hypothesis for simultaneous nonvanishing in Theorem 1.2.

Quantitative propagation

If a fixed-order family has counting function bounded below by $X/(\log X)^{1-\alpha}$ and every character is related to a nonvanishing one by one of finitely many conductor-bounded corrections, the same lower bound holds for the nonvanishing subfamily. This isolates the formal content of Theorem 5.9 used in the applications of Section 5.4.

Significance

The structure theorem replaces one-variable Weierstrass preparation in an infinite-dimensional, non-noetherian Iwasawa algebra. It shows that the zero set of a nonzero horizontal measure is rigid enough that finitely many translations detect an optimal Fourier value everywhere. Through interpolation, this converts a single nonzero horizontal $p$-adic $L$-function into infinitely many nonzero complex central values with a quantitative lower bound.

A formal proof will add reusable infrastructure for nonarchimedean Fourier analysis on profinite products, finite group rings, inverse systems of theta elements, and character-counting asymptotics. None of these results currently has a machine-checked proof in Mathlib. The development is arranged so the analytic structure theorem and the modular-symbol construction can be attacked independently.

Difficulty

The central obstacle is that the horizontal Iwasawa algebra is neither noetherian nor reduced. A direct compactness or finite-generation argument on its spectrum is unavailable. At finite level, Fourier inversion introduces the group order into the valuation estimates; globally, one must control compatible finite quotients while keeping the exceptional correcting set finite. The arithmetic half has a separate normalization problem: raw theta elements satisfy norm relations only up to Euler factors, and interpolation must track imprimitive characters and the removed Euler factors exactly.

Formalization scope

The first version works with the exponent-$p$ digit group $G_p$, which is the setting of Theorem 1.6. Characters take values in the unit group of a complete algebraically closed ultrametric field $K$. Measures are continuous linear functionals on $C(G_p,K)$, and discreteness of integral Fourier values is an explicit hypothesis. The definition does not assume the finite-correction conclusion.

The modular-form layer is exposed through RawThetaSystem, ThetaSystem, and InterpolationDatum. Milestones must construct these data from genuine modular symbols and prove their norm and interpolation fields; merely postulating the desired nonvanishing values does not satisfy the goal. The quantitative statement uses an explicit eventual lower bound rather than asymptotic notation hidden behind an uninterpreted predicate.

Selected references

• Daniel Kriz and Asbjørn Christian Nordentoft, Horizontal p-adic L-functions, arXiv:2310.20678v3, 2025. https://arxiv.org/abs/2310.20678
• Yuri Manin, Periods of parabolic forms and p-adic Hecke series, Mathematics of the USSR-Sbornik 21 (1973). https://doi.org/10.1070/SM1973v021n03ABEH002016
• Glenn Stevens, The cuspidal group and special values of L-functions, Transactions of the AMS 291 (1985). https://doi.org/10.1090/S0002-9947-1985-0797057-3

Current proof decomposition

The new definition node isolates the horizontal Iwasawa algebra and the interpolation interface. The first new milestone constructs a nonzero horizontal $2$-adic $L$-function $\nu_E$. The second milestone assumes such a pair $(\nu_E,\nu_E\ne0)$ and combines the horizontal-measure structure theorem, the Friedberg--Hoffstein quadratic seed, Corollary 5.10, and fixed-order character counting to obtain the lower bound in Theorem 1.1(1). The mission goal then follows immediately by applying the existence milestone and passing its witness to the implication milestone.

Motivation

A unit fraction is the reciprocal $1/n$ of a positive integer. The number $1$ can be written as a sum of distinct unit fractions in infinitely many ways — $1 = \tfrac12+\tfrac13+\tfrac16$, $1 = \tfrac12+\tfrac14+\tfrac16+\tfrac1{12}$, and so on — and the combinatorics of such representations is one of the oldest recurring themes in Erdős's problem lists. Most questions in the area concern size: how many terms are needed, how small the largest denominator can be, how large the smallest one must be. Erdős Problem 287 asks instead about the shape of a representation: how tightly can the denominators be packed?

Order the denominators increasingly and look at their consecutive differences. For $1 = \tfrac12+\tfrac13+\tfrac16$ the differences are $1$ and $3$. The question is whether a difference of at least $3$ must always occur, in every representation of $1$, no matter how many terms it has. The problem is recorded in Erdős and Graham's 1980 problem book (ErGr80, p. 33) and was selected for the booklet of favourite problems prepared for the 1999 Budapest conference on Erdős's mathematics ([Va99, 1.15]). It remains open.

Timeline. The weaker statement that some difference must be at least $2$ — equivalently, that $1$ is never the sum of the reciprocals of a block of consecutive integers — is classical. Theisinger (1915) proved that the harmonic number $H_n$ is not an integer for $n \ge 2$, using Bertrand's postulate. Kürschák (1918) introduced the $2$-adic argument that proves the general block statement: for $m \le n-2$, the difference $H_n - H_m$ is not an integer. Erdős's 1932 paper [Er32], whose title translates as "A generalisation of an elementary number-theoretic theorem of Kürschák", extends the result from blocks of consecutive integers to arithmetic progressions; the erdosproblems.com entry for Problem 287 cites it for the difference-$\ge 2$ bound. Nothing stronger appears to be known: the passage from $2$ to $3$ is the open part, and no partial result is recorded in the entry beyond a conditional one, namely that the conjecture would follow for all but finitely many exceptions if it were known that for every large $N$ there is a prime $p \in [N, 2N]$ with $(p+1)/2$ also prime.

Setting

Fix an integer $k \ge 2$ and integers

$$1 < n_1 < n_2 < \cdots < n_k$$

with

$$1 \;=\; \frac{1}{n_1} + \frac{1}{n_2} + \cdots + \frac{1}{n_k},$$

the sum taken in $\mathbb{Q}$. Call such a tuple a representation of length $k$. The denominators are strictly increasing, hence distinct, and all exceed $1$: the value $n_1 = 1$ is excluded because $1/1$ already exhausts the total. The gaps of the representation are the $k-1$ consecutive differences $n_{i+1} - n_i$ for $1 \le i \le k-1$, and its maximal gap is $\max_i (n_{i+1} - n_i)$.

Representations exist for every $k \ge 3$, and for $k = 1$ only the excluded $n_1 = 1$; no representation of length $2$ exists. Examples: $(2,3,6)$ with gaps $1, 3$; $(2,4,6,12)$ with gaps $2,2,6$; $(3,4,6,10,12,15)$ with gaps $1,2,4,2,3$.

Formalization targets

Goal — Erdős Problem 287

$$\text{every representation } 1 < n_1 < \cdots < n_k \ (k \ge 2) \text{ of } 1 \text{ satisfies } \max_{1 \le i < k} (n_{i+1} - n_i) \;\ge\; 3.$$

This is the open conjecture, stated with no bound on $k$ and no restriction on the denominators beyond those in Setting. It is the weakest form that captures the question: asserting a bound for one particular $k$, or for denominators in some range, would be a different and strictly easier statement.

Milestone — the gap-two bound (Kürschák; Erdős [Er32])

$$\text{every representation satisfies } \max_{1 \le i < k}(n_{i+1} - n_i) \;\ge\; 2.$$

Equivalently: no block of two or more consecutive integers has reciprocals summing to $1$. This is closed mathematics and the natural first target.

Milestone — the classical block theorem (Kürschák)

$$\text{for } n \ge 1 \text{ and } k \ge 2, \qquad \sum_{i=0}^{k-1} \frac{1}{n+i} \notin \mathbb{Z}.$$

The gap-two bound is an immediate consequence, since a representation all of whose gaps equal $1$ is exactly a block of consecutive integers.

Milestone — sharpness

$$1 = \tfrac12+\tfrac13+\tfrac16 \text{ is a representation all of whose gaps are at most } 3.$$

So the constant $3$ in the goal is optimal and cannot be replaced by $4$.

Significance

The result itself. A positive answer would say that a representation of $1$ by unit fractions can never have all its denominators within distance $2$ of each other — a structural constraint of a kind that the size-based results in this area do not provide. The conditional route recorded on the problem page is instructive about where the difficulty sits: it reduces the conjecture, up to finitely many exceptions, to the existence of primes $p$ in $[N,2N]$ with $(p+1)/2$ prime, a statement of Bertrand-with-extra-structure type that is itself out of reach of current technology. A direct proof would therefore either bypass that route or resolve the conjecture for the remaining cases by different means.

Formalizing it. The gap-two bound and the block theorem behind it are closed mathematics, so the honest description of that part of this mission is formalization, not research. It is nevertheless not already available: Mathlib proves Theisinger's case harmonic_not_int, that $H_n \notin \mathbb{Z}$ for $n \ge 2$, but not Kürschák's block version $H_n - H_m \notin \mathbb{Z}$, which is the form Problem 287 needs. Supplying it is a genuine strengthening of the library's existing development and is reusable for any question about reciprocal sums over intervals. The goal itself is open, and this mission does not claim otherwise: it is registered with an open proof, and the milestones are what a solver can realistically close today.

Difficulty

The obvious first idea — bound the number of terms, then check finitely many cases — fails immediately, because $k$ is unbounded: representations of $1$ exist with arbitrarily many terms, so no finite computation can settle the conjecture. The second idea, extending the $2$-adic argument that gives the gap-two bound, also fails, and instructively. That argument works because a block of consecutive integers contains exactly one element of maximal $2$-adic valuation, which leaves the total with negative valuation. Once gaps of size $2$ are permitted the denominators may be chosen to avoid that configuration — for instance all even, as in $(2,4,6,12)$ — and the valuation obstruction disappears. There is no evident replacement prime or weighting that rules out all gap-$\le 2$ configurations simultaneously, and the conditional result quoted above suggests why: the known routes pass through the distribution of primes in short intervals with a multiplicative side condition, rather than through a congruence obstruction.

Formalization scope

A representation is encoded as a function $f : \mathbb{N} \to \mathbb{N}$ together with the hypotheses ∀ i < k, 1 < f i and ∀ i j, i < j → j < k → f i < f j, and the requirement ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1. Only the values of $f$ below $k$ are constrained; the function is not required to be monotone or bounded elsewhere, and nothing outside the window is used. The conclusion is ∃ i, i + 1 < k ∧ 3 ≤ f (i + 1) - f i, the existential form of "the maximal gap is at least $3$"; the subtraction is natural-number subtraction, which is harmless because $f$ is increasing on the window, so no truncation can occur. The sum is a rational equality, not an approximation.

The statement admits no trivializing reading. The hypothesis 1 < f i is essential and is not vacuous — dropping it would admit $f\,0 = 1$, $k = 1$; the strict monotonicity is what makes the gaps well defined and the denominators distinct; and k ≥ 2 guarantees that at least one gap exists, so the conclusion is not an empty existential. Asserting exactly $3$ rather than at least $3$ would be false, as $(2,4,6,12)$ has a gap of $6$.

Infrastructure: the block theorem is proved from Mathlib's padicNorm and padicValNat API — padicNorm.add_eq_max_of_ne, padicNorm.sum_lt', padicNorm.not_int_of_not_padic_int, pow_padicValNat_dvd and pow_succ_padicValNat_not_dvd — and needs no new definitions. That development is reusable beyond this mission and is a candidate for upstreaming to Mathlib alongside harmonic_not_int. Contributions are welcome on any milestone independently; a formalization of the conditional reduction to primes $p$ with $(p+1)/2$ prime would also be a valuable addition, and is not included as a milestone here only because the problem page states it too briefly to formalize faithfully without consulting a primary source.

Selected references

• P. Erdős, Egy Kürschák-féle elemi számelméleti tétel általánosítása (A generalisation of an elementary number-theoretic theorem of Kürschák), Mat. és Phys. Lapok 39 (1932), 17–24.
• P. Erdős and R. L. Graham, Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique, Geneva, 1980, p. 33. scan
• Various, Some of Paul's favorite problems, booklet for the conference "Paul Erdős and his mathematics", Budapest, July 1999, item 1.15.
• K. Conrad, The $p$-adic growth of harmonic sums, expository notes (Theorem 2 is Kürschák's block theorem, with the $2$-adic proof). pdf
• T. F. Bloom, Erdős Problem #287, erdosproblems.com/287.

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

Motivation: when pairwise square conditions limit a set

Diophantine equations ask for integer solutions to arithmetic equations. One family of questions starts with a set of positive integers and imposes the same condition on every pair: their product, increased by one, must be a square. The question is how many distinct integers can satisfy all those conditions together. It connects a simple definition with a global restriction on simultaneous integer solutions.

The paper There is no Diophantine quintuple, by Bo He, Alain Togbé, and Volker Ziegler, resolves the nonexistence question for sets of five elements. This mission targets its headline result, Theorem 1 in Section 1. The mathematical theorem is proved in the paper; the remaining goal is a complete Lean proof of that result.

Setting: positive integers and pairwise perfect squares

A perfect square is an integer of the form $r^2$ for a natural number $r$. A Diophantine $m$-tuple is a set of $m$ distinct positive integers such that the product of any two different members, plus one, is a perfect square. Here $m$ records the number of elements, not a bound on their sizes. A Diophantine quintuple would have exactly five members (definition in Section 1).

Write those five integers as $a_1,\ldots,a_5$. Positivity means $a_i>0$ for every index. Distinctness means $a_i\ne a_j$ whenever $i\ne j$. The square condition requires a possibly different square root for each pair. There is no requirement that the ten square roots coincide, be distinct, or satisfy an additional ordering condition.

The theorem concerns positive integers. Replacing them by rational numbers changes the question. Likewise, allowing zero changes the admissible objects, and allowing repeated entries ceases to represent a five-element set. These domain choices are explicit in the formal target.

Formalization target: no Diophantine quintuple

The single goal is the following nonexistence statement:

$$\nexists\,a_1,\ldots,a_5\in\mathbb Z_{>0}\quad \left[ (\forall i\ne j,\ a_i\ne a_j) \ \land\ (\forall\,1\le i<j\le5,\ \exists r_{ij}\in\mathbb N,\ a_i a_j+1=r_{ij}^{,2}) \right].$$

This is Theorem 1 of the paper. The mission's goal is the existing declaration no_diophantine_quintuple.

The integers are unrestricted in size. The target does not fix the smallest entry, require a particular triple among the entries, or assume that an entry falls below a numerical search threshold. A proof must cover every quintuple satisfying the stated domain conditions.

Significance: an exact obstruction to larger sets

The result rules out an entire class of simultaneous square equations. As an immediate consequence, any set of distinct positive integers satisfying the same pairwise condition has at most four elements: a larger set would contain five distinct members that inherit the condition. This consequence explains why the five-element statement also constrains larger configurations.

A completed formalization would supply a reusable theorem that can be invoked whenever five distinct positive integers and their pairwise square witnesses arise. It would turn the informal nonexistence claim into a checked contradiction from precisely those hypotheses. The published statement is currently open for a Lean proof; its successful compilation verifies that the statement is well formed, not that the theorem has been proved.

Difficulty: the quantifier over all positive integers

Testing examples cannot establish this target by itself. Any computation with a fixed search limit addresses only a bounded collection, while the statement quantifies over all positive integers. A formal proof that uses a finite computation must also establish why the computation covers every possible case.

The conditions are simultaneous: each entry participates in four pairwise equations. Solving or excluding one isolated pair does not by itself settle whether all ten equations can hold together. The paper's proof overview in Section 2 describes the arithmetic estimates and computational components behind its result. Formalizing those components entails checking their hypotheses and connecting their conclusions to the unrestricted goal.

Formalization scope: five indexed natural numbers

The Lean declaration represents the entries by a function a : Fin 5 → Nat. It places the existence of that function under a negation and includes three conditions: every value is positive, different indices have different values, and every pair of different indices has a natural-number square witness.

The square condition is written for all unequal indices. This is equivalent to the usual condition for increasing pairs because multiplication is commutative. No increasing ordering of the five values is imposed. A development using sorted entries must justify its connection to this unrestricted indexed representation.

The root statement needs only Lean's core natural numbers, finite index type, arithmetic, and logic. It introduces no custom predicate whose meaning could hide additional assumptions. A complete proof may use Mathlib and reusable supporting results about integer arithmetic, squares, and the arithmetic tools required by the chosen argument. Supporting declarations should state their hypotheses explicitly and ultimately connect to this exact root theorem. Contributions establishing the known result, including an alternative rigorous proof, are within scope.

Selected references

• Bo He, Alain Togbé, and Volker Ziegler, There is no Diophantine quintuple, arXiv preprint, 2016; revised 2018, arXiv:1610.04020v2. Paper. The target is Section 1, Theorem 1; the definition precedes it, and Section 2 gives the proof overview.

For every integer

$$n > 1$$

, there exists a prime p such that

$$n ^2 < p < n^2 + n$$

Motivation

An almost complex structure gives every tangent space of a smooth manifold the linear algebra of a complex vector space, but it need not come from complex-valued coordinate charts. The gap between these two notions is a global differential-geometric question, not a change of terminology. Granja and Milivojević describe the following as “a major open problem in differential geometry”: whether every closed almost complex manifold of dimension at least six admits an integrable complex structure (Introduction, p. 1). This mission records that question as an open conjecture, not as an established theorem.

Timeline

• 1957: Newlander and Nirenberg proved that an almost complex structure is integrable exactly when its Nijenhuis tensor vanishes, under the regularity assumptions in their theorem. This turns integrability into a nonlinear first-order differential condition rather than a consequence of the pointwise equation $J^2=-\mathrm{id}$ (article).
• 2014–2021: Bryant’s account of Chern’s program still calls the existence of an integrable almost complex structure on $S^6$ open, while referring to the sphere’s well-known almost complex structure (abstract).
• 2022: Granja and Milivojević state the broader closed-manifold question above and study the topology of spaces of almost complex structures on six-manifolds (SIGMA article).

Setting

Fix an integer $n\ge 3$. Let $M$ be a connected, compact, Hausdorff, second-countable smooth manifold without boundary and of real dimension $2n$. An almost complex structure on $M$ is a smooth field

$$J_x:T_xM\longrightarrow T_xM$$

of real-linear maps satisfying $J_x(J_xv)=-v$ for every $x\in M$ and $v\in T_xM$. This condition forces even real dimension, but by itself supplies no complex coordinate charts.

A complex structure of complex dimension $n$ is an atlas with values in $\mathbb C^n$ whose transition maps are complex differentiable. Such an atlas induces an integrable almost complex structure. The target concerns existence on the underlying smooth manifold: the complex structure obtained may induce a different almost complex structure from the supplied $J$. It does not claim that every chosen almost complex structure is integrable.

Here “closed” means compact and without boundary. Connectedness is explicit because it is part of the standing manifold convention in the cited 2022 source. The lower bound is on real dimension: $2n\ge 6$, equivalently $n\ge 3$.

Formalization target

Main open conjecture

For every $n\ge 3$ and every closed connected smooth real $2n$-manifold $M$,

$$M\text{ admits a smooth almost complex structure} \quad\Longrightarrow\quad M\text{ admits a compatible complex atlas of complex dimension }n.$$

“Compatible” means that the underlying real smooth structure of the complex atlas is smoothly equivalent to the given smooth structure on the same topological space. No claim of uniqueness, equality with the original atlas, or integrability of the supplied $J$ is made.

The real six-dimensional case is essential. Since $S^6$ carries an almost complex structure, the conjecture would imply that its underlying smooth manifold carries some complex structure. That special case remains unresolved; restricted nonexistence results, such as results imposing compatibility with a particular metric, do not decide the unrestricted existence question.

Significance

A positive solution would replace a pointwise tangent-bundle reduction by genuine holomorphic coordinates for every manifold in the stated class. It would in particular settle the existence question for $S^6$. A negative solution would identify additional global obstructions to complex atlases that are invisible to the existence of an almost complex structure.

The formalization isolates a reusable smooth almost complex structure on top of Mathlib’s tangent-bundle and manifold APIs, while making the desired complex atlas explicit. This prevents the central distinction from being hidden inside an unconstrained predicate named “integrable.” It also exposes the compatibility between the original real smooth atlas and the real atlas underlying the complex charts, which future work on characteristic classes, Nijenhuis tensors, and concrete six-manifolds can reuse.

Difficulty

The equation $J^2=-\mathrm{id}$ is fiberwise algebra. Integrability requires local complex coordinates whose overlaps are holomorphic, equivalently the vanishing condition identified by Newlander and Nirenberg. Smooth variation of $J$ does not make that differential condition automatic. Thus simply viewing each tangent space as a complex vector space does not construct a complex manifold.

The six-sphere shows why the dimension threshold cannot be treated as a routine stable-range simplification. Its known almost complex structure supplies the hypothesis in real dimension six, while no arbitrary complex atlas is known. Likewise, replacing the conclusion by a complex vector-space structure on each tangent fiber would merely repeat the hypothesis and would not address the open problem.

Formalization scope

The namespace AlmostComplexToComplex uses Mathlib’s boundaryless Euclidean manifold model. AlmostComplexStructure n M contains a continuous real-linear map on every tangent space, the pointwise identity $J^2=-\mathrm{id}$, and smoothness of the induced self-map of the total tangent bundle. It contains no integrability field.

The main theorem assumes the real atlas is modeled on $\mathbb R^{2n}$ and concludes the existence of charts modeled on $\mathbb C^n$. Mathlib’s IsManifold condition over $\mathbb C$ at order one states complex differentiability of chart transitions. Two $C^\infty$ conditions on the identity map compare the original real atlas and the real manifold structure underlying the complex charts in both directions; an unrelated smooth structure therefore cannot satisfy the conclusion merely by being placed on the same carrier type.

This is a chart-level interface, not yet a development of analytic integrability theory. Mathlib at the pinned revision has no ready-made almost-complex/Nijenhuis package connecting the structure above to the Newlander–Nirenberg criterion. The target does not assert that the supplied $J$ is integrable or homotopic to the one induced by the resulting atlas. A dedicated $S^6$ milestone is also outside this minimal draft because faithfully constructing the standard sphere and its known almost complex structure would require additional sourced infrastructure; no surrogate special case is inserted.

Selected references

• Gustavo Granja and Aleksandar Milivojević, Topology of Almost Complex Structures on Six-Manifolds, SIGMA 18 (2022), 093, Introduction, p. 1. DOI; arXiv.
• August Newlander and Louis Nirenberg, Complex Analytic Coordinates in Almost Complex Manifolds, Annals of Mathematics 65 (1957), 391–404. DOI.
• Robert L. Bryant, S.-S. Chern’s Study of Almost-Complex Structures on the Six-Sphere, arXiv:1405.3405v2 (2021 revision), abstract. arXiv.

Motivation

The traveling salesman problem — visit $n$ cities by the cheapest round trip — is the most widely known problem in combinatorial optimization, and its central open question concerns a linear program. The subtour-elimination relaxation (the Held–Karp bound) replaces tours by fractional edge weights, and both in theory and in practice (it powers the lower bounds inside the Concorde solver) it is remarkably close to the true optimum. How close, in the worst case, is the integrality gap of the relaxation: the supremum of $\mathrm{OPT}/\mathrm{LP}$ over metric instances. Explicit instance families push the gap up to $4/3$; the best proven upper bound sits just barely below $3/2$. The 4/3 conjecture — the gap is exactly $4/3$ — has been the benchmark question of approximation algorithms for four decades.

Timeline

• 1954. Dantzig, Fulkerson, and Johnson solve a 49-city instance by hand with the cutting planes that become the subtour-elimination LP.
• 1970–1971. Held and Karp introduce the 1-tree/Lagrangian bound and show it equals the subtour LP value — since then, "the Held–Karp bound".
• 1976/1978. Christofides, and independently Serdyukov, give the $3/2$-approximation: minimum spanning tree plus a matching on odd-degree vertices.
• 1980. Wolsey (Math. Prog. Study 13) shows Christofides' analysis goes through against the LP: $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, so the integrality gap is at most $3/2$. Shmoys and Williamson (IPL 1990) rediscover this via a monotonicity property.
• 1995. Goemans (Math. Programming 69) analyzes the worst-case ratios of TSP relaxations and states the $4/3$ conjecture explicitly; the $4/3$ lower-bound families (three parallel paths) are by then folklore.
• 2011–2014. For graph metrics (shortest-path metrics of unweighted graphs) the barrier breaks: Oveis Gharan–Saberi–Singh and Mömke–Svensson beat $3/2$, and Sebő–Vygen (Combinatorica 2014) reach $7/5$ — the conjectured-optimal shape of progress, but only for a special class.
• 2020–2022. Karlin, Klein, and Oveis Gharan prove a $3/2 - \varepsilon$ approximation for general metric TSP (STOC 2021) and then an integrality-gap bound $\gamma \le 3/2 - \varepsilon$ with $\varepsilon > 10^{-36}$ (FOCS 2022), via max-entropy sampling of spanning trees and strongly Rayleigh distributions — the first general improvement over Wolsey in forty years, by an astronomically small margin.
• Today. The gap between the $4/3$ lower bound and the $3/2 - 10^{-36}$ upper bound is the conjecture. For half-integral LP solutions — where the conjectured extremal instances live — the bound has been pushed to $1.4983$ (Gupta, Lee, Li, Mucha, Newman, and Sarkar, via matroid-based rounding).

Setting

An instance on $n \ge 3$ cities is a cost function $c$ assigning to each ordered pair of cities $u, v$ a real cost $c(u,v)$, required to be a metric cost: symmetric ($c(u,v) = c(v,u)$), zero on the diagonal ($c(v,v) = 0$), and satisfying the triangle inequality $c(u,w) \le c(u,v) + c(v,w)$. Nonnegativity follows; distinct cities at distance zero are allowed, as usual for metric TSP.

A tour visits every city exactly once and returns to its start. Formally a tour is given by an ordering: a permutation $\pi$ of the cities, traversed as $\pi(0), \pi(1), \dots, \pi(n-1)$ and back to $\pi(0)$; its cost $\mathrm{tourCost}(c, \pi)$ is the sum of the costs of consecutive steps, and $\mathrm{OPT}(c)$ — written tspOpt c — is the minimum over all orderings.

The subtour-elimination (Held–Karp) relaxation replaces the tour by a fractional edge weight $x(u,v)$ for each pair of cities. A weight vector $x$ is feasible (IsHeldKarp x) when it is symmetric with zero diagonal, has entries in $[0,1]$, gives every city fractional degree two ($\sum_u x(v,u) = 2$), and crosses every nontrivial cut at least twice: for every set $S$ of cities other than $\emptyset$ and all cities, $\sum_{u \in S} \sum_{v \notin S} x(u,v) \ge 2$. The Held–Karp bound hkValue c is the infimum of $\frac{1}{2}\sum_u \sum_v c(u,v)\,x(u,v)$ over feasible $x$ (the double sum counts each edge twice, hence the $\frac12$). The incidence vector of any tour is feasible, so $\mathrm{LP} \le \mathrm{OPT}$ always.

Formalization targets

Goal — the 4/3 conjecture

$$\mathrm{OPT}(c) \;\le\; \tfrac{4}{3}\,\mathrm{LP}(c) \qquad \text{for every } n \ge 3 \text{ and every metric cost } c.$$

Together with the known lower-bound families this says the integrality gap is exactly $4/3$. The goal carries no algorithm and no constant to improve: it is the terminal statement of the ladder, open in both directions (a proof or a counterexample instance would each settle it).

Milestones — the known ladder

Five results over the same definitions: the relaxation is valid ($\mathrm{LP} \le \mathrm{OPT}$); instance families force the gap arbitrarily close to $4/3$; tree doubling gives $\mathrm{OPT} \le 2\,\mathrm{LP}$; Wolsey's theorem gives $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, the classical upper bound; and the Karlin–Klein–Oveis Gharan record $\mathrm{OPT} \le (\frac{3}{2} - \varepsilon)\,\mathrm{LP}$ for some $\varepsilon > 10^{-36}$ (FOCS 2022). The last milestone is a statement-level target: its known proof (max-entropy sampling, strongly Rayleigh polynomials) is far beyond current formalization practice, so the mission's usable proving frontier remains Wolsey — the milestone records the state of the art as a formal statement.

Significance

The 4/3 conjecture is the reference open problem of approximation algorithms: the quality of the subtour LP calibrates every algorithmic advance on TSP, and the conjectured extremal instances guide the search for better rounding schemes. The bound is also what practical solvers actually compute — branch-and-cut on this LP solves instances with tens of thousands of cities — so the conjecture is a statement about the observed tightness of the world's most-used combinatorial lower bound.

Nothing in this circle exists in any proof assistant: Mathlib has no TSP, no LP relaxations, no polyhedral combinatorics of tours. The mission's milestones force the base layer into existence — tours over Equiv.Perm, cut constraints over Finset, and, for the upper bounds, the parity and tree arguments (spanning trees against the LP, T-joins for the $3/2$ bound) whose infrastructure is reusable for matching theory and network design far beyond TSP.

Difficulty

The naive plan — round the LP solution to a tour — has no known analysis losing less than $3/2$ in general, and the half-integral extremal instances show the hard cases are structured and simple-looking at once. Christofides' matching argument is provably stuck at $3/2$ against the LP; forty years of work moved the constant by $10^{-36}$, and that advance needed an entirely new probabilistic toolkit. On the other side, no instance family with ratio above $4/3$ has ever been found despite extensive computational search over small instances (Benoit–Boyd and successors). Both directions of the goal are genuinely open territory.

Formalization scope

The Lean model commits to: cities Fin n; costs c : Fin n → Fin n → ℝ with IsMetricCost (symmetry, zero diagonal, triangle inequality — nonnegativity is derived, and semimetrics are included as in the standard statement of the conjecture); tours as orderings π : Equiv.Perm (Fin n) traversed cyclically via finRotate, so every permutation denotes a Hamiltonian cycle and every Hamiltonian cycle is denoted; both optimal values as sInf over nonempty, bounded-below sets of reals, so they are genuine minima for n ≥ 3. The hypothesis 3 ≤ n is load-bearing: for n ≤ 2 the degree-2 constraints are infeasible, sInf ∅ = 0 by convention, and the bounds would be false — every theorem therefore carries it.

Welcome contributions: the milestones in any order — held_karp_le_opt is the natural entry point (the tour's incidence vector crosses every cut at least twice); integrality_gap_lower_bound needs the three-path instance family and a case analysis on its tours; tree_doubling_bound needs spanning trees against the LP; wolsey_bound adds the T-join/parity argument and is the summit. Reusable infrastructure — spanning tree polytopes, T-joins, Eulerian traversals, cut lemmas — is welcome as platform theorems. Graph-TSP ($7/5$), path TSP, and asymmetric TSP are deliberately left to future missions; the Karlin–Klein–Oveis Gharan bound is stated as a milestone, but its sampling machinery is expected to arrive, if ever, as shared infrastructure built over many contributions.

Selected references

• G. Dantzig, R. Fulkerson, S. Johnson, Solution of a large-scale traveling-salesman problem, Oper. Res. 2 (1954).
• M. Held, R. Karp, The traveling-salesman problem and minimum spanning trees, Oper. Res. 18 (1970); Part II, Math. Programming 1 (1971).
• N. Christofides, Worst-case analysis of a new heuristic for the travelling salesman problem, CMU report (1976); A. Serdyukov, Upravlyaemye Sistemy 17 (1978).
• L. Wolsey, Heuristic analysis, linear programming and branch and bound, Math. Prog. Study 13 (1980). doi:10.1007/BFb0120913
• D. Shmoys, D. Williamson, Analyzing the Held-Karp TSP bound: a monotonicity property with application, Inf. Process. Lett. 35 (1990). doi:10.1016/0020-0190(90)90028-V
• M. Goemans, Worst-case comparison of valid inequalities for the TSP, Math. Programming 69 (1995). doi:10.1007/BF01585563
• A. Sebő, J. Vygen, Shorter tours by nicer ears, Combinatorica 34 (2014). arXiv:1201.1870
• A. Karlin, N. Klein, S. Oveis Gharan, A (slightly) improved approximation algorithm for metric TSP, STOC 2021. arXiv:2007.01409
• A. Karlin, N. Klein, S. Oveis Gharan, A (slightly) improved bound on the integrality gap of the subtour LP for TSP, FOCS 2022. arXiv:2105.10043
• V. Traub, J. Vygen, Approximation Algorithms for Traveling Salesman Problems, Cambridge University Press, 2024. book page