Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models table formatting, the placement of program segments on pages, and the allocation of files to disc tracks, and it is NP-complete, so exact solutions require search in general. Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3 (1974)) therefore studied four simple placement heuristics and bounded how far each can be from the optimum in the worst case. Their paper is one of the founding results of the worst-case analysis of approximation algorithms.

This mission concerns the two decreasing heuristics, which sort the items from largest to smallest before placing them. For them the paper proves that at most $\tfrac{11}{9}$ of the optimum, plus an additive constant, is ever used, and that the factor $\tfrac{11}{9}$ cannot be improved.

Timeline.

• 1973: D. S. Johnson's MIT thesis proves $FFD(L)\le \tfrac{11}{9}L^*+4$; the argument exceeds 75 pages.
• 1974: Johnson, Demers, Ullman, Garey and Graham publish the bound for FFD and BFD, with a complete proof of the reduction from BFD to FFD and an outline of the FFD argument.
• 1985: B. S. Baker gives a shorter proof of $FFD(L)\le\tfrac{11}{9}L^*+3$ (J. Algorithms 6).
• 1991: M. Yue publishes a proof of $FFD(L)\le\tfrac{11}{9}L^*+1$.
• 2007: G. Dósa determines the tight additive constant, $FFD(L)\le\tfrac{11}{9}L^*+\tfrac{6}{9}$ (ESCAPE 2007, LNCS 4614).

Setting

A list is a finite sequence $L=(a_1,a_2,\dots,a_n)$ of real numbers in $(0,1]$; values may repeat. A bin has capacity $1$; its level is the sum of the numbers placed in it. The optimum $L^*$ is the least number of bins into which the elements of $L$ can be distributed so that no bin has level exceeding $1$.

The bins $B_1,B_2,\dots$ start empty and the elements are placed one at a time, in list order.

• First-Fit (FF) places $a_i$ into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$.
• Best-Fit (BF) places $a_i$ into a bin whose level $\beta$ satisfies $\beta\le 1-a_i$ and is as large as possible, the one of least index among ties.
• First-Fit Decreasing (FFD) and Best-Fit Decreasing (BFD) first arrange $L$ into nonincreasing order and then apply FF, respectively BF.

$FFD(L)$ and $BFD(L)$ are the numbers of bins that receive at least one element.

Two auxiliary notions from the paper's proof also appear among the milestones. The position $(j,k)$ of an element in a packing means that it is the $k$-th element placed into bin $j$. The weight $W(X)$ of a collection of elements is defined through $k$-pieces, the elements in $(\tfrac1{k+1},\tfrac1k]$. Each element has the weight $w_1(x)=\lfloor 1/x\rfloor^{-1}$. A pair $(x,y)$ with $x$ a $k$-piece and $kx+y\le1$ has the discounted weight $w_2(x,y)=w_1(x)+\tfrac{k-1}{k}w_1(y)$, and any other pair has $w_1(x)+w_1(y)$. $W(X)$ is the least total weight over all ways of grouping $X$ into singletons and pairs.

Formalization targets

Goal: Theorem 3.2

For every list $L$,

$$FFD(L)\le \frac{11}{9}L^*+4\qquad\text{and}\qquad BFD(L)\le\frac{11}{9}L^*+4 .$$

The constants are the paper's. Both halves are part of the goal.

Milestones, in the order the argument uses them

1. Lemma 3.3. If $FFD(L)>rL^*+d$ with $r,d\ge1$, the list $L'$ keeping only the elements exceeding $(r-1)/r$ also has $FFD(L')>rL'^*+d$; the same for BFD. With $r=\tfrac{11}{9}$ this reduces the goal to lists in $(\tfrac2{11},1]$.
2. Claims 3.4.5 and 3.4.6, two steps of the proof of Theorem 3.4 that concern only the FFD packing $PF$ and the BFD run. On $[\tfrac16,1]$, BFD places every element exceeding $\tfrac13$ exactly where FFD does. Among the remaining positions of $PF$, the lexicographic order of positions respects the order of the sorted list.
3. Theorem 3.4. If $L\subseteq[\tfrac16,1]$, then $BFD(L)\le FFD(L)$. This transfers the bound from FFD to BFD on $(\tfrac2{11},1]$.
4. Lemma 4.2. For every integer $N\ge4$ and $L\subseteq(\tfrac1N,\tfrac12]$,

$$W(L)\ge FFD(L)-N+2 .$$

5. The reduced assertion (Section 4, p. 314). If $L\subseteq(\tfrac2{11},1]$, then

$$FFD(L)\le\frac{11}{9}L^*+4 .$$

6. Theorem 3.1, the matching lower bound: for each $k\ge1$ there is a list with $L^*=k$ and $FFD(L)=BFD(L)>\tfrac{11}{9}L^*-2$.

Significance

The bound makes FFD and BFD, which run in $O(n\log n)$ time, the reference heuristics for off-line bin packing. The $\tfrac{11}{9}$ bound and its proof technique of weighting functions were the model for the analysis of many later packing and scheduling heuristics. Theorem 3.1 shows that the factor is exact, so together with the goal it determines $\lim_{k\to\infty}R_{FFD}(k)=\lim_{k\to\infty}R_{BFD}(k)=\tfrac{11}{9}$, where $R_A(k)$ is the largest ratio $A(L)/L^*$ over lists with $L^*=k$.

The result is proved, but the source proves it only in part. The paper gives complete proofs of Lemma 3.3, Theorem 3.4 and Theorem 3.1. For the reduced assertion it gives only an outline, whose central inequalities involve maps the paper never defines, and it refers to the thesis for the details. Lemma 4.2 is proved in the paper through two claims. A formal proof of the goal must therefore either formalize one of the later complete proofs (Baker 1985, Yue 1991, Dósa 2007) or reconstruct the thesis argument. No machine-checked proof of the $\tfrac{11}{9}$ bound is present in Mathlib or on the platform.

Difficulty

The obvious approach, used for First-Fit in Section 2 of the same paper, assigns each element a weight depending only on its size, so that every bin of the algorithm's packing weighs at least $1$ and every bin of an optimal packing weighs at most the target ratio. For FFD no weighting of single elements works at ratio $\tfrac{11}{9}$. Summing $w_1$ over the elements overcharges the FFD packing: a set of elements fitting into one bin can carry total $w_1$-weight well above $\tfrac{11}{9}$. The paper's remedy is a weight defined on pairs, $W(X)$, which discounts elements that could share a bin with a larger one. Even with $W$, the bins of FFD whose largest element exceeds $\tfrac12$ do not fit the scheme. Handling them requires a case analysis that the paper only sketches and that runs to more than 75 pages in the thesis.

The BFD half cannot be obtained by bounding BFD by FFD in general: there are lists with $BFD(L)=\tfrac{10}{9}FFD(L)$. Theorem 3.4 works only because Lemma 3.3 first removes all elements below $\tfrac2{11}$.

Formalization scope

Lists are L : List ℝ with the predicate IsList L ($0<a\le1$ for every element), assumed by every statement. $L^*$ is optBins L, the least b : ℕ admitting a map from the items to Fin b with every bin sum at most $1$. A run keeps the nonempty bins as a List (List ℝ) in index order and opens a new bin at the end exactly when no nonempty bin fits, which matches the paper's "least $j$" over infinitely many empty bins. The fit test is non-strict. FFD and BFD are FF and BF applied to sortDesc L, a stable merge sort into nonincreasing order. They are defined for every list, so the goal is stated for arbitrary, unsorted $L$. Positions are $0$-based pairs (bin, place in bin) read off the run.

$W$ sorts its argument into nonincreasing order, so index is the position in that order. It then minimizes over involutions of the positions, which encode the partitions into one- and two-element sets. Weights are real-valued; the paper's use of rationals is incidental. The range hypotheses are exactly the paper's: $[\tfrac16,1]$ is closed in Theorem 3.4, $(\tfrac2{11},1]$ is open at $\tfrac2{11}$, and Lemma 4.2 has $\tfrac1N<a\le\tfrac12$.

A weakened goal, such as $FFD(L)\le\tfrac{11}{9}L^*+c$ with a larger $c$, a bound for sorted lists only, or the FFD half alone, is a different theorem and does not close the mission. Claims 3.4.1–3.4.4 and 3.4.7 and the inequalities $(*)$, $(**)$ of the outline are not stated: they concern the paper's step-by-step construction and the undefined maps $f$, $g$.

A complete development needs basic lemmas about FF and BF runs (levels stay at most $1$, a new bin opens only when nothing fits, runs on prefixes). It also needs invariance of FFD and BFD under permutations of equal elements, the monotonicity of $L^*$ under deletion, and $L^*\ge\sum_i a_i$. These are reusable in the other missions of this series. Proofs of individual milestones, alternative complete proofs of the goal, and sharper additive constants are all welcome.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, Ph.D. thesis, Massachusetts Institute of Technology, 1973 (reference [8] of the paper above).
• B. S. Baker, A new proof for the first-fit decreasing bin-packing algorithm, Journal of Algorithms 6(1):49–70, 1985. https://doi.org/10.1016/0196-6774(85)90018-5
• M. Yue, A simple proof of the inequality FFD(L) ≤ 11/9 OPT(L) + 1, ∀L, for the FFD bin-packing algorithm, Acta Mathematicae Applicatae Sinica 7(4):321–331, 1991.
• G. Dósa, The tight bound of first fit decreasing bin-packing algorithm is FFD(I) ≤ 11/9 OPT(I) + 6/9, ESCAPE 2007, LNCS 4614:1–11, 2007. https://doi.org/10.1007/978-3-540-74450-4_1

Motivation

A set $A$ of positive integers is pairwise coprime if $\gcd(a,b)=1$ for all distinct $a,b\in A$. The primes are the model example, and a recurring theme in Erdős's combinatorial number theory is that pairwise coprime sets cannot do much better than the primes on natural additive or harmonic statistics. Erdős Problem 1210 asks for a sharp version of this principle for the harmonic weight $1/(n-a)$, which measures how densely a coprime set can crowd the point $n$ from below.

Timeline.

• 1977. In [Er77c, p.64] Erdős posed a question about the primes $q_1<\dots<q_k$ in an interval $(n,m]$: is $\sum_i 1/(q_i-n)<\sum_{p<m-n}1/p+O(1)$?
• 1980. In [Er80, p.112] he wrote that he had "not stated [this] quite correctly" in [Er77c] and posed the question for arbitrary pairwise coprime sets $A\subseteq[1,n)$, which is the form recorded as Problem 1210.
• 2026. On the erdosproblems.com forum, a reduction to a counting bound for $A\cap[n-x,n)$ was suggested; it was then observed that this counting bound would itself imply an open inequality of the type $\pi(x+y)\le\pi(x)+\pi(y)+O(y/(\log y)^2)$ (compare Problem 855). The problem remains open.

Setting

Fix a natural number $n$. Consider finite sets $A$ of integers with $1\le a<n$ for every $a\in A$, and with $\gcd(a,b)=1$ for all distinct $a,b\in A$. For such a set define the reciprocal gap sum

$$S_n(A)=\sum_{a\in A}\frac{1}{n-a}.$$

Every term is at most $1$, and the element $a=n-d$ contributes $1/d$. Write $\sum_{p<n}1/p$ for the sum of reciprocals of the primes below $n$; by Mertens' theorem it equals $\log\log n+O(1)$. Throughout, $\pi(x)$ denotes the number of primes $p\le x$.

Target

The goal of the mission is the affirmative answer to Problem 1210: there is an absolute constant $C$ such that

$$S_n(A)\;\le\;\sum_{p<n}\frac1p+C$$

for every $n$ and every pairwise coprime $A\subseteq[1,n)$. A negative answer is equally welcome and is recorded by disproving the goal statement.

The milestones are:

1. Small prime factors. For pairwise coprime $A$, at most $\pi(x)$ elements of $A\cap[n-x,n)$ have a prime factor $\le x$.
2. Partial summation reduction. If $|A\cap[n-x,n)|\le\pi(x)+O(x/(\log x)^2)$ uniformly, then the goal holds.
3. The [Er77c] variant. For the primes $q_i$ in $(n,m]$, $\sum_i 1/(q_i-n)<\sum_{p<m-n}1/p+O(1)$.

Significance

The result itself. An affirmative answer would say that, for the weight $1/(n-a)$, no pairwise coprime set beats the primes by more than a constant, and would give a quantitative form of the heuristic that coprime sets behave like sets of primes near a point. A negative answer would exhibit coprime sets that concentrate near $n$ more efficiently than the primes do in the harmonic sense. The [Er77c] variant concerns only primes, and relates the distribution of primes just above $n$ to the primes below the interval length $m-n$.

Formalizing it. Neither the goal nor the [Er77c] variant is known. The mission produces Lean statements checked against the source, a reduction (milestone 2), to be verified in Lean, that isolates exactly which counting estimate would suffice, and the elementary coprimality lemma (milestone 1). These pin down what a proof or disproof must supply.

Difficulty

The natural first attempt splits $A\cap[n-x,n)$ into elements with a prime factor $\le x$, of which there are at most $\pi(x)$, and $x$-rough elements, and then hopes that sieve bounds make the rough part $O(x/(\log x)^2)$. The obstruction is that $A$ may contain many primes in $[n-x,n)$. Bounding the number of primes in a short interval $[n-x,n)$ by $\pi(x)+O(x/(\log x)^2)$ is a form of the second Hardy–Littlewood conjecture $\pi(x+y)\le\pi(x)+\pi(y)$, which is open and known to be incompatible, in its exact form, with the prime $k$-tuples conjecture. So the counting route in milestone 2 needs input on primes in short intervals beyond current knowledge, and any proof of the goal must either supply such input or avoid pointwise counting.

Formalization scope

All objects are elementary: $A$ is a Finset ℕ, coprimality is Nat.Coprime, primes are Nat.Prime, $\pi$ is Nat.primeCounting, and the sums are real-valued. The source's $O(1)$ is encoded as an existentially quantified real constant $C$ chosen before $n$ and $A$. The source asks a yes/no question; each statement is posed in its affirmative form, and a disproof (a proof of the negation) settles the negative answer. The standing hypothesis $1\le a<n$ means every denominator $n-a$ is at least $1$, so no division-by-zero default can make the statement trivial. The window $[n-x,n)$ is written as $a\ge n-x$ with truncated natural subtraction together with $a<n$.

No new definitions are required. Useful reusable contributions include Mertens-type estimates for $\sum_{p<n}1/p$, partial summation lemmas for finite sums over $\mathbb N$, and upper bounds for primes in short intervals.

Selected references

• P. Erdős, Problems and results on combinatorial number theory. III, Number Theory Day (Proc. Conf., Rockefeller Univ., New York, 1976), (1977), 43–72. [Er77c]
• P. Erdős, A survey of problems in combinatorial number theory, Ann. Discrete Math. (1980), 89–115. [Er80]
• T. F. Bloom, Erdős Problem #1210, https://www.erdosproblems.com/1210 , and discussion thread https://www.erdosproblems.com/forum/thread/1210
• Formal Conjectures project, ErdosProblems/1210.lean, https://github.com/google-deepmind/formal-conjectures

Motivation

Addition and multiplication interact in rigid ways: a finite set of numbers that is highly structured with respect to one operation (an arithmetic progression, say) tends to be unstructured with respect to the other (a geometric progression). The sum–product problem asks for the sharp quantitative form of this principle. It was posed by Erdős and Szemerédi in 1983 (Erdős Problem 52) and has since become a central question of additive combinatorics, with applications in incidence geometry, exponential sum estimates, expanders and randomness extraction.

Timeline.

• 1983 — Erdős and Szemerédi show that $\max(|A+A|,|AA|)\ge c|A|^{1+\delta}$ for some absolute $\delta>0$ and every finite set of integers $A$, and conjecture exponent $2-\varepsilon$.
• 1997 — Nathanson obtains the explicit exponent $1+\tfrac1{31}$; Ford (1998) improves it to $1+\tfrac1{15}$.
• 1997 — Elekes, using the Szemerédi–Trotter incidence theorem, proves $|A+A|\,|AA|\gg|A|^{5/2}$ for finite sets of reals, hence exponent $5/4$.
• 2009 — Solymosi proves $|A+A|^2|AA|\gg |A|^4/\log|A|$ for finite sets of positive reals, hence exponent $4/3$ up to a logarithmic factor.
• 2015–2022 — Konyagin and Shkredov first break the $4/3$ barrier (exponent $4/3+c$ for a small explicit $c>0$); after several improvements, Rudnev and Stevens reach $4/3+2/1167$ up to logarithmic factors.

The conjecture itself remains open.

Setting

For a finite set $A\subset\mathbb Z$ define the sumset and product set

$$A+A=\{a+b : a,b\in A\},\qquad AA=\{ab : a,b\in A\}.$$

For nonempty $A$ both contain at least $|A|$ elements and at most $\binom{|A|+1}{2}$. The quantity of interest is $\max(|A+A|,|AA|)$ as a function of $|A|$.

Formalization targets

Goal (Erdős–Szemerédi conjecture)

For every $0<\varepsilon<1$ there is $C_\varepsilon>0$ such that for every finite set $A\subset\mathbb Z$,

$$\max(|A+A|,|AA|)\ \ge\ C_\varepsilon\,|A|^{2-\varepsilon}.$$

Known lower bounds (milestones, weakest to strongest)

$$|A+A|\ge 2|A|-1,\qquad \max(|A+A|,|AA|)\gg|A|^{1+\delta},\qquad \gg|A|^{5/4},\qquad \gg\frac{|A|^{4/3}}{(\log|A|)^{1/3}},\qquad \gg_\varepsilon |A|^{4/3+2/1167-\varepsilon}.$$

Sharpness

The $\varepsilon$ cannot be removed: there is no $C>0$ with $\max(|A+A|,|AA|)\ge C|A|^2$ for all $A$ (take $A=\{1,\dots,n\}$; the multiplication table $|AA|$ is $o(n^2)$ by Erdős).

Significance

A proof of the goal would settle the sharp form of the sum–product phenomenon over $\mathbb Z$. Sum–product estimates are an input to incidence bounds, to Bourgain–Katz–Tao-type results over finite fields, and to explicit constructions in theoretical computer science; improvements of the exponent over $\mathbb R$ have come together with new incidence-geometric tools.

Formalization status: the milestones are published theorems (Erdős–Szemerédi, Elekes, Solymosi, Rudnev–Stevens, Erdős's multiplication table bound), but their proofs are not known to be formalized in Lean/Mathlib. The Szemerédi–Trotter theorem, multiplicative energy, and the Elekes and Solymosi arguments are reusable infrastructure. The goal itself is an open problem.

Difficulty

Incidence-geometric methods (Szemerédi–Trotter and its descendants) naturally produce exponents near $4/3$, and passing beyond $4/3$ has required intricate higher-energy arguments yielding only small gains. None of the existing approaches is known to reach exponents close to $2$; even over $\mathbb Z$, where arithmetic structure is available, the best general bounds are the real-number ones.

Formalization scope

Sets are Finset ℤ; $A+A$ and $AA$ are Mathlib's pointwise sumset and product set (open scoped Pointwise), and cardinalities are cast to $\mathbb R$. Powers are real powers (Real.rpow). The empty set is allowed; the hypothesis $\varepsilon<1$ keeps every exponent positive, so the empty set contributes the trivial inequality $0\ge 0$ rather than a junk value $0^0=1$. The constant $C$ may depend on $\varepsilon$ but not on $A$. The Solymosi milestone is stated for $|A|\ge2$ so that $\log|A|>0$.

The statements are for integer sets only; results proved over $\mathbb R$ specialise to them. Contributions of general-purpose infrastructure (Szemerédi–Trotter over $\mathbb R$, multiplicative energy, bounds for the multiplication table) are welcome.

Selected references

• P. Erdős, E. Szemerédi, On sums and products of integers, Studies in Pure Mathematics, Birkhäuser, 1983, 213–218.
• M. B. Nathanson, On sums and products of integers, Proc. Amer. Math. Soc. 125 (1997), 9–16.
• K. Ford, Sums and products from a finite set of real numbers, Ramanujan J. 2 (1998), 59–66.
• G. Elekes, On the number of sums and products, Acta Arith. 81 (1997), 365–367.
• J. Solymosi, Bounding multiplicative energy by the sumset, Adv. Math. 222 (2009), 402–408. https://arxiv.org/abs/0806.1040
• S. V. Konyagin, I. D. Shkredov, On sum sets of sets having small product set, Proc. Steklov Inst. Math. 290 (2015), 288–299. https://arxiv.org/abs/1503.05771
• M. Rudnev, S. Stevens, An update on the sum-product problem, Math. Proc. Cambridge Philos. Soc. 173 (2022), 411–430. https://arxiv.org/abs/2005.11145
• Erdős Problem 52, https://www.erdosproblems.com/52

Motivation

A $2n$-dimensional complex abelian variety $A$ is of Weil type for an imaginary quadratic field $K=\mathbb{Q}(\sqrt{-d})$ if $K$ acts on $A$ by rational endomorphisms in such a way that each of the two eigenspaces of $\sqrt{-d}$ on $H^1(A,\mathbb{C})$ meets $H^{1,0}(A)$ in an $n$-dimensional subspace. A. Weil observed that such $A$ carry a two-dimensional space of rational $(n,n)$-classes, the Hodge–Weil classes, that are in general not generated by divisor classes. Whether they are algebraic is one of the main test cases of the Hodge conjecture; by work of Schoen, Moonen–Zarhin and others, algebraicity for abelian fourfolds of Weil type implies the Hodge conjecture for all abelian fourfolds.

E. Markman (arXiv:2502.03415) proves this algebraicity by a new construction. Its starting point, developed in §§1.2 and 2 of the paper, is linear algebra: the even cohomology $H^{\mathrm{ev}}(X)$ of an abelian $n$-fold $X$ is a half-spin representation of $\mathrm{Spin}(V)$, where $V=H^1(X,\mathbb{Z})\oplus H^1(\hat X,\mathbb{Z})$, and a rational plane $P\subset H^{\mathrm{ev}}(X,\mathbb{Q})$ meeting the variety of pure spinors in two conjugate $K$-points (a $K$-secant) equips $X\times\hat X$ with the structure of an abelian variety of Weil type. This mission formalizes that construction and its explicit example in §2.4.

Timeline (as summarized in §1.1 of the source).

• Weil introduces abelian varieties of Weil type and their exceptional Hodge classes.
• Schoen proves algebraicity for fourfolds with $K=\mathbb{Q}(\sqrt{-3})$ (and for sixfolds with $K=\mathbb{Q}(\sqrt{-3})$ and trivial discriminant), and for fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$; van Geemen gives another proof of the latter.
• Koike treats sixfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$; Markman treats fourfolds with arbitrary $K$ and discriminant $1$.
• 2025: Markman proves algebraicity for sixfolds of discriminant $-1$ and every $K$, hence for all abelian fourfolds of Weil type.

Setting

Let $X$ be a complex torus of dimension $n$. Fix a basis of $H^1(X,\mathbb{Z})$, so that $H^1(X,\mathbb{C})=\mathbb{C}^{2n}$, and write $H^1(\hat X)\cong H^1(X)^*$ in dual coordinates. The complex structure of $X$ is a real matrix $J$ with $J^2=-1$ acting on $H^1(X,\mathbb{R})$; its $i$-eigenspace is $H^{1,0}(X)$. A number $z\in\mathbb{C}$ acts on $H^1(X,\mathbb{C})$ by $\operatorname{Re}z+\operatorname{Im}z\,J$ and on $H^k(X,\mathbb{C})=\wedge^kH^1(X,\mathbb{C})$ multiplicatively; a class of type $(p,q)$ is multiplied by $z^p\bar z^q$. The Hodge ring is $\bigoplus_pH^{p,p}(X,\mathbb{Q})$.

• $V_{\mathbb{C}}=H^1(X,\mathbb{C})\oplus H^1(\hat X,\mathbb{C})$ carries the pairing $((w_1,t_1),(w_2,t_2))_V=t_1(w_2)+t_2(w_1)$ and the complex structure $I=J\oplus(-J^{\mathsf T})$ of $X\times\hat X$; $V^{1,0},V^{0,1}$ are the $\pm i$-eigenspaces of $I$.
• $S_{\mathbb{C}}=H^*(X,\mathbb{C})=\wedge^*H^1(X,\mathbb{C})$ is the spin representation: $v=(w,t)$ acts by $m_v(s)=w\wedge s+D_t(s)$, with $D_t$ the contraction. A nonzero $s\in S^+_{\mathbb{C}}=H^{\mathrm{ev}}(X,\mathbb{C})$ is an even pure spinor if its annihilator $W_s=\{v:m_v(s)=0\}$ has dimension $2n$ (it is then maximal isotropic).
• For $d>0$ put $\sqrt{-d}=i\sqrt d$ and $K=\mathbb{Q}(\sqrt{-d})$. Given rational $a,b\in S^+$ with $\lambda_{1,2}=a\pm\sqrt{-d}\,b$ even pure spinors, the line $\mathbb{P}(P)$, $P=\operatorname{span}_{\mathbb{Q}}(a,b)$, is a $K$-secant to the spinor variety, with $W_1=W_{\lambda_1}$, $W_2=W_{\lambda_2}$. When $W_1\cap W_2=0$, the endomorphism $f=\eta_{\sqrt{-d}}$ acting by $\pm\sqrt{-d}$ on $W_{1,2}$ is rational (2.2.4), (2.4.1); $\Xi_P(x,y)=(f(x),y)_V$ and $g_P(x,y)=\Xi_P(I(x),y)$.
• For an ample class $\Theta\in H^{1,1}(X,\mathbb{Z})$ put $u=\sqrt{-d}\,\Theta$ and $P=\operatorname{span}\{\operatorname{Re}\exp(u),\operatorname{Im}\exp(u)/\sqrt d\}$ (2.4.5).

Formalization targets

Goal (Proposition 2.4.4, with (2.4.6) and Lemma 2.2.6)

For a complex torus $X$ of dimension $n\ge2$ with ample $\Theta$, and a positive integer $d$: $\exp(\pm\sqrt{-d}\,\Theta)$ are even pure spinors with $W_1\cap W_2=0$, and there is a rational $f$ acting by $\pm\sqrt{-d}$ on $W_{1,2}$ with

$$f^2=-d,\quad (fx,fy)_V=d\,(x,y)_V,\quad fI=If,\quad \dim(W_i\cap V^{1,0})=n,\quad g_P(x,x)<0\ \ (0\neq x\in V_{\mathbb{R}}).$$

That is, $(X\times\hat X,\eta,\Xi_P)$ is a polarized abelian variety of Weil type.

Milestones

Equation (2.4.6) (the annihilator of $\exp(u)$), Equation (2.4.5) (the plane lies in the Hodge ring), Lemma 2.2.6 (Weil's condition), the rational similarity $f$ of (2.2.4)/(2.4.1), the commutation $fI=If$ (§2.4, p. 20), and Lemma 2.4.2 (the formula for $g_P$).

Significance

The result. The construction supplies, for every imaginary quadratic field $K$ and every polarized abelian $n$-fold, a polarized abelian variety of Weil type $X\times\hat X$, together with a description of its Weil structure in spin-representation terms. The rest of the paper deforms this structure ($\mathrm{Spin}(V)_P$ plays the role of the special Mumford–Tate group) and uses Orlov's derived equivalence to obtain the Hodge–Weil classes from sheaves; the final application is the Hodge conjecture for abelian fourfolds.

Formalizing it. The results of this mission are proved in the paper; none of them has a machine-checked proof. The mission produces a reusable Lean model of the spin representation $H^*(X)$ of $V=H^1(X)\oplus H^1(\hat X)$, of pure spinors and their annihilators, and of Hodge types on $\wedge^*H^1$, all built on Mathlib's exterior and Clifford algebras.

Difficulty

The algebra in the explicit example is short, but the general milestones rest on facts about pure spinors (their annihilators are maximal isotropic; a conjugate pair with $W_1\cap W_2=0$ splits $V_K$; rationality of $f$ by Galois descent) and on Lemma 2.2.6, whose proof in the source uses Chevalley's isomorphism $S\otimes S\cong C(V)$ as a morphism of Hodge structures. A coordinate computation settles the example but not the general statements. Sign conventions (the choice of $\sqrt{-d}$, the complex structure on $H^1(\hat X)$, and the sign of ampleness) all enter the final negativity claim.

Formalization scope

• Everything is linear algebra over $\mathbb{C}$, with the rational and integral structures given by the coordinate basis; $X$ is a complex torus carrying the class $\Theta$.
• $H^*(X,\mathbb{C})$ is ExteriorAlgebra ℂ (Fin (2n) → ℂ); contraction is Mathlib's CliffordAlgebra.contractLeft; $\exp$ is the truncated exponential $\sum_{k\le2n}s^k/k!$.
• The complex structure of $V_{\mathbb{R}}$ is $I=J\oplus(-J^{\mathsf T})$, the extension of $J$ that is an isometry of $(\cdot,\cdot)_V$ (footnote 8 of the source).
• Ampleness sign. Ampleness is encoded as it is used in the proof of Proposition 2.4.4: $\Theta\in H^{1,1}(X,\mathbb{Z})$ and $\Theta(a\wedge I(a))>0$ for nonzero $a\in H^1(\hat X,\mathbb{R})$, with $I=-J^{\mathsf T}$ on $H^1(\hat X,\mathbb{R})$. With the opposite sign the last clause of the goal would become positive definiteness.
• $W_1\cap W_2=0$ is a hypothesis of the general milestones; in the source it is deduced from the non-isotropy of $P$ via Lemma 2.2.1.
• Not included: the spin group, the stabilizer $\mathrm{Spin}(V)_P$, the centralizer statement of Lemma 2.2.4 and the discriminant computation of Lemma 3.1.3. Contributions adding these are welcome.

Selected references

• E. Markman, Cycles on abelian 2n-folds of Weil type from secant sheaves on abelian n-folds, arXiv:2502.03415v2, 2025. https://arxiv.org/abs/2502.03415
• C. Chevalley, The algebraic theory of spinors, Columbia University Press, 1954.
• B. van Geemen, An introduction to the Hodge conjecture for abelian varieties, in: Algebraic Cycles and Hodge Theory, LNM 1594, Springer, 1994. https://doi.org/10.1007/BFb0074000
• P. Deligne, The Hodge conjecture, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/hodge.pdf

Motivation

Given a real matrix $A=(a_{ij})\in\mathbb R^{m\times n}$, consider maximizing the bilinear form $\sum_{i,j}a_{ij}x_iy_j$ over sign vectors $x\in\{\pm1\}^m$, $y\in\{\pm1\}^n$. This discrete optimum, written $\mathrm{OPT}(A)$, is closely tied to the cut norm of a matrix and is NP-hard to compute. Relaxing each sign to a unit vector and each product to an inner product gives the semidefinite value $\mathrm{SDP}(A)$, computable in polynomial time. Grothendieck's inequality (Grothendieck, 1953) states that the relaxation overshoots by at most a universal factor: there is a finite $K$, independent of $A$, of $m,n$, and of the dimension of the vectors, with $\mathrm{SDP}(A)\le K\cdot\mathrm{OPT}(A)$ for every $A$. The Grothendieck constant $K_G$ is the least such $K$ — equivalently, the worst-case integrality gap of the canonical semidefinite relaxation of this bilinear problem.

The constant is not a curiosity of one optimization problem. It originated in functional analysis, where it is central to the geometry of Banach spaces and to harmonic analysis; it governs the approximation ratio available for cut norms; and, in quantum information, it measures the maximal advantage of quantum over classical correlations in Bell-type experiments. Its exact value has been open since 1953.

A timeline of the bounds:

• 1953, Grothendieck. Existence of a finite $K$, together with the lower bound $K_G\ge\pi/2=1.5707\ldots$
• 1977, Krivine. $K_G\le\pi/\bigl(2\log(1+\sqrt2)\bigr)=1.7822\ldots$, obtained by analyzing hyperplane rounding, and conjectured to be optimal.
• 1984/1991, Davie and Reeds (independently). $K_G\ge1.6769\ldots$, from an explicit high-dimensional Gaussian hard instance.
• 2011, Braverman–Makarychev–Makarychev–Naor. Krivine's conjecture is false: $K_G<\pi/(2\log(1+\sqrt2))$ strictly, with no quantitative gap.
• 2014, Naor–Regev. Mixtures of Krivine schemes are asymptotically optimal: rounding schemes of this one family approach the true value of $K_G$.
• 2026, Heilman; Jones–Malavolta. The first improvements on Davie–Reeds, by $10^{-26}$ and $10^{-12}$ respectively; and the first explicit numerical improvements on Krivine's bound, of order $10^{-5}$ (Heilman; Li–Saha–Xue et al.).
• 2026, Saha–Li–Xue–Chaudhuri–Klivans–Kothari–Meka. The bounds this mission targets:

$$\frac{6\pi}{11}\ \le\ K_G\ \le\ \frac{\pi}{2\log(1+\sqrt2)}-3.47\times10^{-4},$$

i.e. $1.7135\ldots\le K_G\le1.7818\ldots$, which fixes the tenths digit of $K_G$ at $7$.

Setting

Fix $m,n\in\mathbb N$ and $A\in\mathbb R^{m\times n}$.

$$\mathrm{OPT}(A):=\max_{x\in\{\pm1\}^m,\;y\in\{\pm1\}^n}\sum_{i,j}a_{ij}x_iy_j,\qquad \mathrm{SDP}(A):=\sup_{d\in\mathbb N}\ \sup_{u_i,v_j\in S^{d-1}}\sum_{i,j}a_{ij}\langle u_i,v_j\rangle .$$

Here $u_1,\dots,u_m$ and $v_1,\dots,v_n$ are unit vectors of a common but arbitrary finite dimension $d$. Since a sign is a unit vector in dimension one, $\mathrm{OPT}(A)\le\mathrm{SDP}(A)$. Call $K$ a Grothendieck bound if $\mathrm{SDP}(A)\le K\cdot\mathrm{OPT}(A)$ for every $m$, $n$ and $A$, and set $K_G:=\inf\{K: K\text{ is a Grothendieck bound}\}$.

Upper bounds on $K_G$ come from rounding algorithms. A Krivine scheme of dimension $k$ is a pair of partitions of $\mathbb R^k$ into a $+1$ region and a $-1$ region, encoded by measurable odd functions $f,g:\mathbb R^k\to\{\pm1\}$: the algorithm maps each SDP vector to a Gaussian point in $\mathbb R^k$, correlated according to the inner products, and reads off the label of the region the point lands in. Taking $f=g=\operatorname{sgn}(z_1)$ recovers random hyperplane rounding. The quality of a scheme is carried by its normalized correlation function

$$H(t):=\frac{\pi}{2}\,\mathbb E\bigl[f(X)g(Y)\bigr],$$

where $X,Y$ are standard Gaussian vectors in $\mathbb R^k$ with $\mathbb E[X_iY_i]=t$ for every coordinate $i$. For the half-space partition $H(t)=\arcsin t$, whose analysis gives Krivine's bound. Writing the odd expansion $H(t)=b_1t+b_3t^3+\cdots$, the hyperplane scheme sits at $(b_1,b_3)=(1,\tfrac16)$.

Formalization targets

Goal

$$\frac{6\pi}{11}\ \le\ K_G\ \le\ \frac{\pi}{2\log(1+\sqrt2)}-3.47\times10^{-4}$$

This is the two-sided bound the source paper states as the outcome of its Theorems 2.1 and 2.2. It is the weakest statement that carries both of the paper's contributions at once; each side is also a milestone in its own right, so partial progress is recorded even if only one direction closes.

Milestones

The milestone list runs from the classical background to the two new bounds: $\mathrm{OPT}\le\mathrm{SDP}$; the existence of a finite Grothendieck bound; $K_G\ge\pi/2$; Krivine's $K_G\le\pi/(2\log(1+\sqrt2))$; the affine coefficient constraint $b_3\ge2b_1-\tfrac{11}{6}$ valid for every Krivine scheme (Theorem 2.2, equation (1)); the transfer of a member of the affine family into a lower bound on $K_G$ (Appendix A); the lower bound $K_G\ge6\pi/11$ (Theorem 2.2); and the cubic–quintic upper bound (Theorem 2.1).

Significance

The two target bounds narrow an interval that had been essentially static for four decades: before 2026 the state of the art was $1.6769\ldots\le K_G\le1.7822\ldots$, wide enough that the tenths digit was unknown. The lower bound is also methodologically new. Every previous lower bound was obtained by exhibiting a hard instance; this one instead proves a ceiling on the performance of every rounding scheme in the Krivine family and converts that ceiling, through the Naor–Regev optimality theorem, into a bound on the constant. The affine constraint $b_3\ge2b_1-\tfrac{11}{6}$ is the transportable core of that argument: being affine in the coefficients, it survives mixing schemes and passing to limits, which is exactly what the reduction to $K_G$ requires.

On the formalization side, nothing here is machine-checked today. The upper bound (Theorem 2.1) is certified by interval arithmetic in the companion paper, and the lower bound's central one-dimensional inequality likewise rests on a computer-assisted certificate; reproducing either inside Lean means building a rigorous numeric layer on top of the analytic argument. Ahead of that, the mission needs a formal definition of $K_G$ itself and of the Krivine-scheme apparatus, neither of which exists in Mathlib — these are reusable well beyond this mission, since Grothendieck's inequality feeds cut-norm approximation and Bell-inequality bounds. Contributions of intermediate lemmas about $\mathrm{OPT}$, $\mathrm{SDP}$, Gaussian correlation identities, and Hermite expansions are welcome even when the headline bounds stay open.

Difficulty

The obvious route to a lower bound is to write down a matrix and compute. That route is what Davie and Reeds exhausted; improving it has produced gains of order $10^{-12}$ at best, because the hard instances are high-dimensional Gaussian objects whose $\mathrm{OPT}$ is itself hard to bound tightly. The route taken here avoids instances entirely, and its difficulty lies elsewhere: a constraint on a single scheme is worthless unless it survives averaging over schemes and passing to limits of schemes of growing dimension, since only then does the Naor–Regev optimality theorem convert it into a statement about $K_G$. Constraints that are nonlinear in the scheme do not survive that passage, which is why the target inequality is affine in $(b_1,b_3)$. For the upper bound, the difficulty is that the improvement is genuinely asymptotic: it comes from a limit of schemes of growing dimension rather than any fixed low-dimensional partition, and the final margin of $3.47\times10^{-4}$ is certified numerically rather than in closed form.

Formalization scope

$\mathrm{OPT}(A)$ and $\mathrm{SDP}(A)$ are defined as suprema of explicitly described sets of reals, over matrices indexed by Fin m and Fin n with real entries; the sign vectors are real-valued functions constrained to take the values $1$ and $-1$, and the relaxation quantifies over unit vectors of EuclideanSpace ℝ (Fin d) for an existentially quantified $d$, so no dimension bound is built in. The empty-index cases $m=0$ or $n=0$ are included and give value $0$ on both sides. $K_G$ is the infimum of the set of Grothendieck bounds; that set is nonempty precisely by Grothendieck's inequality, which is itself a milestone, and it is bounded below, so the infimum is not a junk value.

A Krivine scheme is a structure carrying two measurable $\pm1$-valued functions on Fin k → ℝ, each odd almost everywhere. Almost-everywhere oddness is forced: no $\pm1$-valued function satisfies $f(-0)=-f(0)$ at the origin, so a pointwise requirement would make the structure empty and every statement about schemes vacuous. With the null-set relaxation the half-space partition is a scheme in every dimension $k\ge1$, and the definition file constructs it, pinning down non-vacuity; dimension $k=0$ admits no scheme. The correlation function is the explicit double Gaussian integral against the correlated-pair density, scaled by $\pi/2$, and the coefficients $b_1,b_3$ are read off as $H'(0)$ and $H'''(0)/6$ — where $H$ fails to be three times differentiable at $0$ these are the ambient junk value $0$, which a solver should keep in mind when reading the coefficient milestones.

No trivializing reading is available for the goal: it pins $K_G$ between two explicit numerical constants, so it can be satisfied neither vacuously nor by a degenerate convention. Solvers should be aware that the source paper states its two theorems in abridged form and refers to its companion paper for the full proofs, and that the further bounds reported there — the stronger lower rungs $27\pi/49$ and $51\pi/92$, and the upper values $1.781801841033$ and $1.7813319810625639$ — are explicitly described as system-tested but not author-verified; they are deliberately outside this mission's milestone list.

Selected references

• A. Grothendieck, Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79.
• J.-L. Krivine, Sur la constante de Grothendieck, C. R. Acad. Sci. Paris (1977).
• M. Braverman, K. Makarychev, Y. Makarychev, A. Naor, The Grothendieck constant is strictly smaller than Krivine's bound, FOCS 2011, 453–462. https://doi.org/10.1109/FOCS.2011.77
• A. Naor, O. Regev, Krivine schemes are optimal, Proc. Amer. Math. Soc. 142 (2014), 4315–4320. https://doi.org/10.1090/S0002-9939-2014-12145-3
• N. Alon, A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), 787–803. https://doi.org/10.1137/S0097539704441629
• A. Li, R. Saha, A. Xue, S. Chaudhuri, A. Klivans, P. K. Kothari, R. Meka, Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human–AI Mathematical Collaboration, arXiv:2608.11195v3, 2026. https://arxiv.org/abs/2608.11195
• R. Saha, A. Li, A. Xue, S. Chaudhuri, A. Klivans, P. K. Kothari, R. Meka, New upper and lower bounds for the Grothendieck constant, 2026 (companion paper containing the full proofs).

Erdős Problem 68: Irrationality of sum 1/(n! - 1)

Problem Statement & Context

Erdős Problem 68 asks whether the infinite series 184987\sum_{n=2}^{\infty} rac{1}{n! - 1}184987 is irrational.

Paul Erdős proved in 1948 that \sum_{n=1}^{\infty} rac{1}{2^n - 1} is irrational, but the problem for factorial denominators ! - 1$ remains open.

Main Target Theorem

Comparing random sums with continuous paths

A sum of independent random increments is a basic model for accumulated noise. A continuous Gaussian process offers a different description of that noise, one that can be studied at every nonnegative time. To compare their individual trajectories, both objects must live on the same probability space. The question is whether their paths can remain close over a whole finite range of observation times, with a quantitative bound on the chance of a large discrepancy. Ethier and Kurtz state such a result for independent sums in Chapter 7, Section 5, Theorem 5.1 of Markov Processes: Characterization and Convergence, printed page 356.

Probability laws and partial sums

Let $\mu$ be a probability measure on the real line. Assume that it has finite exponential moments in a neighborhood of zero: there is $a_0>0$ such that

$$\int_{\mathbb R} e^{ax}\,\mu(dx)<\infty\qquad (|a|\leq a_0).$$

This hypothesis controls both tails of the distribution. In particular, its mean $m$ and variance $\sigma^2$ are finite. The distribution need not be centered, symmetric, bounded, or have positive variance. Let $\xi_1,\xi_2,\ldots$ denote independent random variables each with distribution $\mu$, and write $S_k=\xi_1+\cdots+\xi_k$ for their partial sums.

A Brownian motion with drift and variance rate $m,\sigma^2$ can be written as $W(t)=mt+\sigma B(t)$, where $B$ is standard real Brownian motion and $\sigma$ is the nonnegative square root of the variance. When $\sigma=0$, this expression gives the deterministic path $mt$. A coupling specifies a joint probability law for the entire sequence and the Brownian path while preserving their required individual laws. The sequence coordinates are independent of one another; independence between the sequence and the Brownian path is not part of the requirement.

The strong approximation target

Theorem 5.1 asserts that a coupling and positive constants $C,K,\lambda$, depending only on $\mu$, exist such that

$$\mathbb P\!\left\{\max_{1\leq k\leq n}|S_k-W(k)|>C\log n+x\right\}<K e^{-\lambda x}$$

for every integer $n\geq1$ and every real $x>0$. Both inequalities displayed here are strict. One joint construction works simultaneously for every horizon $n$ and every positive excess $x$; neither the coupling nor the constants are chosen anew after those parameters are specified. At $n=1$, the logarithmic term is zero, so the same assertion controls the discrepancy at the first observation time.

The mission consists of this full theorem. The rescaling and Poisson consequences discussed later in the section are outside its target. There are no separate supporting theorem milestones in the accepted grouping.

What the estimate provides

The estimate controls the largest discrepancy among all partial sums up to a specified horizon. Its deterministic threshold grows logarithmically with that horizon, and its remaining tail decreases exponentially with the excess above the threshold. This makes the theorem a quantitative comparison of trajectories on a common space. The opening of Section 5 identifies strong approximation of independent sums as its subject and introduces approximation of the Poisson process as a subsequent consequence.

The mathematical result is a known theorem stated by Ethier and Kurtz. The present formal target asks for a checked proof of that statement, including the existence of its coupling. The statement is supplied with an unproved theorem body; no proof of the strong approximation estimate is asserted here.

Why the coupling is demanding

The prescribed marginal laws do not themselves determine the joint relationship that makes the paths close. The construction must preserve independence within the entire increment sequence and the Brownian finite-dimensional laws while also satisfying a maximal estimate for every finite horizon. A comparison of the distributions at one terminal time does not supply these simultaneous path requirements. The exponential tail and the uniform choice of constants are both part of the goal.

Representation and conventions

The common carrier is a pair consisting of a real sequence indexed by natural numbers and a continuous real path indexed by nonnegative real times. A probability measure on this carrier is the unknown coupling. Its first coordinate at index zero represents $\xi_1$, so summing over the first $k$ natural indices represents $S_k$ exactly. Its second coordinate is standard Brownian motion; the affine expression $mt+\sigma B(t)$ supplies the general drift and variance.

The finite maximum event is expressed by the existence of an integer $k$ with $1\leq k\leq n$ whose error exceeds the threshold. This avoids any convention for a maximum of an empty set. Exponential integrability supplies the finite moments needed for the mean and variance. The probability bound uses the nonnegative extended-real embedding of the positive finite quantity $K e^{-\lambda x}$. The formal statement retains the full exponential-moment class, including point masses. Existing probability-measure, independence, law, Brownian-motion, and variance definitions supply the mathematical vocabulary.

Selected references

Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986 (held reprint copyright 1986/2005), Chapter 7, Section 5, Theorem 5.1 and equation (5.1), printed page 356; local source PDF page 365. The book title and authors are recorded on local PDF page 2.

Why couple sums to Brownian motion

Independent sums are a basic model for accumulated random fluctuation. A central limit theorem describes their distribution at one large time, and a functional limit theorem describes weak convergence of a rescaled path. Strong approximation asks for substantially more: construct the sums and a Brownian motion on one probability space so that their paths remain close, with an explicit error bound that holds simultaneously over all earlier integer times. Such a coupling turns Brownian path estimates into quantitative information about random walks and independent sums.

Chapter 7, Section 5 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986) states this strong approximation result as Theorem 5.1. Its estimate has logarithmic deterministic error and a strictly exponential tail. The theorem is known as a Komlós–Major–Tusnády type approximation, but the mission follows the exact formulation and hypotheses printed by Ethier and Kurtz.

Probability law and common space

Let $\mu$ be a probability measure on $\mathbb R$. The hypothesis requires an $\alpha_0>0$ such that

$$\int_{\mathbb R} e^{\alpha x}\,\mu(dx)<\infty \qquad\text{whenever }|\alpha|\leq \alpha_0.$$

Thus the moment-generating integral is finite on a neighborhood of zero. No centering, symmetry, bounded-support, or positive-variance assumption is made.

The conclusion constructs one probability space carrying an iid sequence $(\xi_i)_{i\geq1}$ with common law $\mu$ and a Brownian motion $W$. The Brownian motion has drift and variance chosen to match one summand:

$$E[W(1)]=E[\xi_1]=m, \qquad \operatorname{var}(W(1))=\operatorname{var}(\xi_1)=\sigma^2.$$

Writing $S_k=\sum_{i=1}^k\xi_i$, both $S_k$ and $W(k)$ are evaluated on this same space. The theorem does not require the iid sequence to be independent of the Brownian coordinate; their dependence is precisely what permits a close coupling.

Formalization target

There are positive constants $C$, $K$, and $\lambda$, depending only on $\mu$, such that for every integer $n\geq1$ and every real $x>0$,

$$P\left\{\max_{1\leq k\leq n}|S_k-W(k)|>C\log n+x\right\} <K e^{-\lambda x}.$$

Both inequalities are strict: the discrepancy event uses $>$ and its probability is $<K e^{-\lambda x}$. The constants and the entire coupling are chosen before $n$ and $x$. The logarithmic term is retained at $n=1$, where $\log 1=0$.

The Lean statement uses sequence coordinates indexed from zero, so coordinate $i$ represents the source variable $\xi_{i+1}$ and Finset.range k is exactly the sum of the first $k$ variables. An existential index $k$ with $1\leq k\leq n$ expresses the finite maximum event without replacing either strict inequality.

What the theorem provides

Weak convergence compares distributions after rescaling and does not place a prelimit sum and its limiting process on the same sample point. This theorem instead supplies a simultaneous pathwise comparison through a common-space construction. The exponential tail quantifies the chance that the uniform error up to time $n$ exceeds the logarithmic scale by an additional amount $x$.

The formal statement records the complete coupling rather than only its consequence for normalized terminal sums. It exposes the iid coordinate laws, mutual independence of those coordinates, the Brownian law, the moment-matched affine scaling, the positivity and quantifier order of the constants, and the exact maximal-error event. This is a statement-only formalization: the theorem remains an open Lean goal, and no proof claim is made.

Where the difficulty lies

Matching a single sum to a Gaussian random variable is not enough. The construction must coordinate every partial sum with one Brownian path, uniformly over all $k\leq n$, while keeping the error logarithmic and the excess probability exponentially small. Independent coupling at each time would destroy consistency across times, while an ordinary invariance principle gives convergence in distribution without the stated finite-$n$ tail. The difficulty is therefore the joint construction with all of these quantitative requirements at once.

Formalization scope and conventions

The common carrier is the product of a real sequence space with the subtype of continuous functions from nonnegative real time to $\mathbb R$. A probability measure $Q$ on that carrier is the joint law. iIndepFun asserts mutual independence of all sequence coordinates, and HasLaw gives each coordinate the law $\mu$. IsBrownianReal specifies the standard Brownian second coordinate.

The Brownian motion appearing in the estimate is defined from that standard coordinate by

$$W(t)=mt+\sqrt{\operatorname{var}_\mu(X)}\,B(t).$$

This representation covers the zero-variance case: then the scaled Brownian fluctuation vanishes and $W$ is deterministic, while the auxiliary standard Brownian coordinate may still be present on the common carrier. The exponential-moment hypothesis supplies the intended finite first and second moments. Probabilities use extended nonnegative reals, and the finite positive real bound $K e^{-\lambda x}$ is embedded with ENNReal.ofReal.

No local auxiliary definition is expression-essential: all objects in the theorem are provided by Mathlib. The mission intentionally excludes the section's rescaling observations and Poisson corollaries, which do not form separate capstone goals in the accepted grouping. Useful future contributions include the proof of this exact common-space theorem and reusable coupling infrastructure that preserves strict tail estimates.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 7, Section 5, Theorem 5.1, equation (5.1), printed p. 356. Wiley DOI

Motivation

Regression is usually taught with a fixed parametric model: linear regression fits a $d$-dimensional coefficient vector, and the estimation error is controlled by $d/n$. Many regression problems in practice have no such finite-dimensional description — the regressor is only known to be, say, convex, monotone, or smooth, and the estimator is a least-squares fit over the (infinite-dimensional) set of functions with that shape. This is nonparametric regression, and the basic question is the same as in the parametric case: how close is the fitted function to the truth, as a function of the sample size $n$? Answering it requires replacing "dimension" with a genuinely functional notion of complexity, since an infinite- dimensional function class can still be small enough to estimate well (a Sobolev ball) or too large to estimate at all. The theory in this mission, due to van de Geer and developed in Chapter 13 of Wainwright (High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019), gives a single non-asymptotic template — the localized Gaussian complexity — that answers this question for an arbitrary star-shaped function class, and recovers the familiar parametric and Sobolev/RKHS rates as special cases.

Setting

Fix $n$ design points $x_1,\dots,x_n$ in an arbitrary covariate space $\mathcal X$ (fixed, not random — this is the fixed-design setting) and observe

$$y_i = f^*(x_i) + \sigma w_i, \qquad i = 1,\dots,n,$$

where $f^*$ is the unknown regression function, $\sigma > 0$ is a known noise level, and $w_1,\dots,w_n$ are i.i.d. standard Gaussian. Given a class $F$ of candidate functions, the nonparametric least-squares estimate is any minimizer

$$\hat f_n \in \arg\min_{f\in F}\ \frac1n\sum_{i=1}^n \big(y_i - f(x_i)\big)^2.$$

Error is measured in the empirical (design-dependent) seminorm $\|g\|_n^2 := \frac1n\sum_{i=1}^n g(x_i)^2$. A class $H$ of functions is star-shaped if $h\in H$ and $\alpha\in[0,1]$ together imply $\alpha h \in H$ — every convex class containing the origin has this property, and it is the minimal structural assumption under which the theory below applies. For a star-shaped class $H$ and radius $\delta>0$, the local Gaussian complexity

$$G_n(\delta; H) := \mathbb E_w\Big[\ \sup_{h\in H,\ \|h\|_n\le\delta}\ \Big|\tfrac1n \sum_{i=1}^n w_i h(x_i)\Big|\ \Big]$$

measures how much a mean-zero Gaussian process can be made to look like a member of $H$ restricted to the ball of radius $\delta$. A critical radius $\delta_n$ is any positive solution of $G_n(\delta;H)/\delta \le \delta/(2\sigma)$; by Lemma 13.6, $\delta\mapsto G_n(\delta;H)/\delta$ is non-increasing on $H$ star-shaped, so this inequality always has a smallest positive solution.

Formalization targets

Lemma 13.6. For any star-shaped $H$, $\delta \mapsto G_n(\delta;H)/\delta$ is non-increasing on $(0,\infty)$, and consequently $G_n(\delta;H)/\delta \le c\delta$ has a smallest positive solution for every $c>0$.

Theorem 13.5 (special case, $f^*\in F$).

$$\mathbb P\big[\|\hat f_n - f^*\|_n^2 \ge 16\,t\delta_n\big] \le e^{-nt\delta_n/(2\sigma^2)} \qquad \text{for all } t \ge \delta_n.$$

Theorem 13.13 (goal — general oracle inequality, $f^*$ not assumed in $F$). With $\delta_n$ solving the critical inequality for $\partial F := F - F$, there are universal constants $(c_0,c_1,c_2)$ such that for all $t\ge\delta_n$,

$$\|\hat f_n-f^*\|_n^2 \le \inf_{\gamma\in(0,1)}\left[\frac{1+\gamma}{1-\gamma}\|f-f^*\|_n^2 +\frac{c_0}{\gamma(1-\gamma)}t\delta_n\right]\quad\text{for all }f\in F,$$

with probability at least $1-c_1e^{-c_2nt\delta_n/\sigma^2}$. The goal is deliberately the statement with unresolved universal constants and an infimum over $\gamma$, rather than any single instantiated bound, so the target survives sharper constant tracking.

Significance

Theorem 13.13 is the "master" result behind essentially every concrete rate in the chapter: orthogonal series regression, convex/monotone regression, and (via the KRR specialization of Section 13.4) kernel ridge regression rates for Sobolev and Gaussian-kernel classes are all obtained by bounding $G_n$ for a particular $F$ and reading off $\delta_n$. Its value is that it isolates exactly the one place where the geometry of $F$ enters — the local Gaussian complexity — while the probabilistic argument (a peeling/chaining argument controlling a localized empirical process) is generic. Formalizing it produces, for the first time on the platform, the statement-level infrastructure (star-shaped classes, local Gaussian complexity, critical radius) that any future mission on a concrete nonparametric-regression rate — kernel ridge regression, convex regression, isotonic regression — can specialize, without re-deriving the oracle inequality from scratch. The proof itself (concentration of Gaussian complexity via Borell-TIS/Gaussian comparison plus a peeling argument over dyadic scales) is not attempted here; only the statement is formalized, as a draft goal for future proof contributions.

Difficulty

The naive route to Theorem 13.13 is to bound $\|\hat f_n - f^*\|_n$ pointwise via the basic inequality $\tfrac12\|\hat f_n-f^*\|_n^2 \le \tfrac{\sigma}{n}\sum_i w_i(\hat f_n(x_i)-f^*(x_i))$ and then bound the right side by $\sigma\,G_n(\delta;\partial F)$ for $\delta = \|\hat f_n-f^*\|_n$ — but $\delta$ is itself random (it depends on the estimate), so this is circular: the bound on the right depends on the very quantity being bounded. The chapter's actual argument resolves this with a peeling device: partition the event space by which dyadic annulus $\|\hat f_n-f^*\|_n$ falls into, and apply a uniform (non-circular) bound on each annulus separately via Gaussian concentration, summing a geometric series of tail probabilities. This is the step every first attempt misses, and it is why the local Gaussian complexity — rather than the simpler global complexity of Chapter 4/5 — is the right object: localizing to radius $\delta$ is what makes the per-annulus bound tight enough for the final sum to converge.

Formalization scope

Design points are an arbitrary type X (no topology or metric structure is needed for the statements themselves); the least-squares estimate is represented as a Prop (IsLeastSquaresEstimate) picking out any function achieving the empirical minimum, matching the book's "any minimizer" phrasing rather than assuming uniqueness. The local Gaussian complexity is defined as an expectation over an explicit i.i.d.-standard-Gaussian noise vector on an abstract probability space, with the inner supremum taken over the subtype of the radius-restricted slice of the class — this is well-defined (not the junk value 0 of an unbounded Set ℝ supremum) whenever the slice is nonempty, which holds automatically for any nonempty star-shaped class (taking $\alpha=0$ exhibits $0$ in the class). Since neither X nor H carries a topology, separability or countability constraint, SatisfiesCriticalInequality adds an explicit Integrable hypothesis on that same supremum (added in revision), guarding against Mathlib's Bochner integral silently returning the junk value 0 for a non-measurable integrand — a value that would otherwise trivially satisfy the critical inequality for every positive δ, regardless of the function class's actual local complexity. The trivializing formalization to rule out here is stating Theorem 13.13's universal constants after the quantification over the function class and sample size, which would let $(c_0,c_1,c_2)$ secretly depend on the instance and make the "universal" claim vacuous; this mission places the constant quantifiers first, before the class, design and noise data they must not depend on. A complete downstream development would add: the concentration-of-Gaussian-complexity step (Borell–TIS or a comparable tail bound), the peeling argument, and the metric-entropy / Dudley-integral machinery of Section 13.2.1 for bounding $G_n$ explicitly on concrete classes (Sobolev balls, RKHS balls) — none of which is attempted here.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 13. https://doi.org/10.1017/9781108627771
• S. van de Geer, Empirical Processes in M-Estimation, Cambridge University Press, 2000.
• S. van de Geer, "Estimating a regression function," Annals of Statistics, 18(2):907-924, 1990. https://doi.org/10.1214/aos/1176347627