Proofs from THE BOOK: verified results and open formalization tasks

This Textbook project develops a reusable Lean library around Martin Aigner and Günter M. Ziegler's Proofs from THE BOOK. It combines results imported from the existing proof_in_the_book repository with precise contribution targets from the sixth edition (2018). The aim is to preserve mathematical meaning, reuse existing proofs, and make the remaining work accessible to other contributors.

What is already verified

The original import contains 156 distinct platform-accepted results. Euclid, the original main theorem, is retained as a completed milestone when the project goal moves to the sixth-edition extension. Every one of the repository's 40 chapter topics has accepted results. Each result certifies its actual Lean statement, including its hypotheses; this does not certify every argument or every theorem in a chapter. Some proofs reuse Mathlib, while others were developed in the repository. Their source and proof notes retain that distinction.

The imported source snapshot is 873d52e0c88cd351f594221e70c3c5b3559777a9. Imported results use Lean 4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Immutable public source links are used only where the linked source matches the verified artifact. Compatibility changes, unsuccessful attempts, and verification evidence are retained in the integration project.

The live goal is the explicit conjunction of the 21 linked sixth-edition extension targets. Its reduction connects these targets to the goal, so proving the remaining children advances the project. This goal is deliberately narrower than “every theorem and every proof in the book”; the unlinked topology tasks below are additional formalization work.

Sixth-edition contribution targets

New milestones explicitly marked 6th ed. cover Chapters 7 (spectral theorem and determinants), 15 (round circles and links), 35 (finite Kakeya), 37 (permanents and entropy), and 45 (probabilistic counting). They include the precise definitions and boundary conditions needed to state the results. Compiled Open targets are requests for proofs, not proved results. The spectral theorem has a direct Mathlib proof; community results are reused under their actual statements and with attribution.

Two Chapter 15 tasks intentionally remain unlinked mathematical milestones: the full non-equivalence assertion for the depicted Borromean, Tait, and trivial links, and the Fox-coloring invariance bridge for equivalent link diagrams. These invite formalization of the diagrams and the topology bridge as well as proof. The separate modular Fox calculations do not by themselves establish ambient non-equivalence.

The crossing-lemma target is the universal good-drawing form: actual injective edge arcs and exact finite intersection records appear in its interface. It does not assume the desired crossing bound. The Ramsey target preserves the real exponent for odd k. The related public Erdős–Ramsey result with a rounded exponent is identified as a supporting result, not as proof of that full target.

Chapter numbering and statement scope

Older milestones use the repository's chapter labels. Repository Chapters 1–21 match the bundled fourth edition; Chapter 22 inserts Van der Waerden's permanent theorem, and Chapters 23–40 correspond to fourth-edition Chapters 22–39. The sixth edition has 45 chapters, so these organizational labels are not sixth-edition chapter numbers. New milestones give sixth-edition numbers and printed source pages explicitly.

Some existing formalizations preserve narrower statements or additional premises. Examples include repository Chapter 13's dihedral-angle conclusion, Chapter 28's Dilworth lower-bound result, and the geometric premises in Chapter 36. Read the actual linked theorem and its description before reusing it. A chapter title or the former Euclid main theorem is not a completion certificate for the collection.

How to contribute

Choose an Open linked theorem and inspect its definitions, exact binders, Mathlib revision, and prior attempts. Reuse a compatible existing result when it proves that statement; preserve the original contributor's attribution. Submit a matching proof for verification. For an unlinked milestone, first formalize and review the source statement and its definitions. These are known textbook results awaiting formalization or proof in this project, rather than claims of new unresolved mathematics.

Source repository: https://github.com/xiangyazi24/proof_in_the_book

Book: Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), https://doi.org/10.1007/978-3-662-57265-8

Motivation

The value of the Riemann zeta function at five is the convergent sum

The target is that this number cannot be expressed as a ratio of integers. This mission concerns the complete proof development in mo271/Zeta5, pinned to commit 7fe736760f4b96bfdb4334b68e3b3124ecbe10b0. The repository follows Aabir Fauzan's preprint ζ(5) is irrational, while explicitly changing parts of its arithmetic normalization. Its formal target is the individual value at five. Results asserting that at least one member of a list of odd zeta values is irrational do not establish this target.

The repository reports a complete Lean proof with only the standard axioms propext, Classical.choice, and Quot.sound. That is a statement about the source project. The existing Prove2.me goal remains Open, and importing and checking the source proof against the platform environment is the work tracked here. The exact existing goal is reused as a reference; there is no second copy of the irrationality assertion.

Setting

The construction uses Hankel matrices, whose entries depend on the sum of their row and column indices. For a natural index $n$, put $K=40n$, $N=3n$, and $h=37n$. The rational polynomial $D_m(t)=\prod_{j=1}^m(t+j^2)$ controls a family of rational functions. A rational linear functional takes prescribed Bernoulli-number values on powers of $t$ and prescribed affine-polynomial values on the simple poles $(t+j^2)^{-1}$. Polynomial division and residues extend it to $P(t)/D_K(t)$.

Applying this functional to $D_N(t)^6t^{i+j}/D_K(t)$ gives an $h\times h$ matrix $G_n(X)$ over $\mathbb Q[X]$. Write $\Delta_n(X)=\det G_n(X)$ and $F_n(X)=S_n\Delta_n(X)$, where $S_n$ is the explicit positive factorial ratio in the construction module. These are specified polynomials; their existence and properties are not abstract supply assumptions. The real number zeta5 is the convergent series, and a short bridge identifies it with Mathlib's complex zeta value.

Formalization targets

The goal is

It is the existing theorem FCP.Zeta.irrational_zeta_five. The supporting target from the source main estimate is

The formal statement also requires $Q_n$ to be a positive rational multiple of the explicit $F_n$.

The milestone list records the general polynomial irrationality criterion, the exact degree calculation, the moment representation with integrability, strict determinant positivity, the real-value upper bound, integral normalization with its growth estimate, and the final small-value statement. A further supporting theorem states that $b^{37n}e^{-cn^2}$ tends to zero for every fixed positive integer $b$ and every $c>0$. These targets cover the analytic, arithmetic, and final assembly parts of the source project.

Significance

The goal distinguishes a single zeta value from the disjunctive irrationality results for finite lists. The intermediate results also provide reusable infrastructure: an irrationality criterion for polynomials of varying degree, integral moment representations of rational functionals, determinant positivity, and estimates controlling rational normalizers.

For formalization, the concrete task is to transplant the source development while preserving its definitions, hypotheses, and actual constants. The source's existing proofs provide the intended implementations; the mission does not replace the difficult analytic or arithmetic statements with assumed approximation families. Proof imports and accepted submissions must eventually connect those implementations to the existing goal. The source's Apache-2.0 license and commit-pinned attribution accompany the code.

Difficulty

Small real values alone do not suffice: the integer coefficients and the degree growth must be controlled at the same time. The normalization needed to obtain integer coefficients can enlarge the values enough to destroy the analytic estimate. The decisive quantitative requirement is that its growth constant stay below the magnitude of the negative analytic constant.

Here the analytic estimate uses $U=-2733991/2000000$, and the implemented normalization uses $A_{\rm eff}=136/100$. Their exact rational sum is negative. The milestone assertions retain the source's lower-order terms $27K\log K+200K$ and the eventual quantifiers in the normalization estimate. They do not strengthen an eventual estimate to a uniform one, or infer positivity from a vanishing upper bound.

Formalization scope

The scope is the complete importable proof path to Apery.irrational_five in the pinned repository, including the arithmetic modules, logarithmic-energy estimates, finite certificates, and the external prime-number-theorem dependency where the proof uses it. The headline milestones organize that full development; they are not a claim that every internal lemma is already published on the platform. The repository's optional stronger numerical rate and the preprint's irrationality-measure claim are outside this goal.

The source uses cutoff $400$, a full rank loss in its outer-prime estimate, and direct class-wise partial fractions, as documented in its implementation notes. Its final estimate asserts some positive decay constant, not the paper's $139/5$. The draft retains those choices. Polynomial evaluations take place over the reals, coefficients begin in the rationals and are normalized into the integers, and the moment integrals are Lebesgue integrals over $(0,\infty)$. Definitions are total at zero, while the positivity and real-bound milestones explicitly require $n>0$.

The source pins Lean 4.34.0-rc1 and Mathlib f385f9fd18abed332ebcd3df239cb357e264aceb. This proposal targets the available Lean 4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 environment. The draft definitions and milestone statements are checked locally in that target environment; acceptance of the complete imported proof graph is a separate verification step. The external dependency is mo271/PrimeNumberTheoremAnd at 04d81b2a68ea3548b9990813fdc463c78511f412. Any imported proof must retain a standard-axiom-only dependency check.

Selected references

• Aabir Fauzan, ζ(5) is irrational, preprint, 17 September 2026. Zenodo record and manuscript.
• mo271 and contributors, Zeta5, Lean source project, commit 7fe736760f4b96bfdb4334b68e3b3124ecbe10b0. Pinned repository.
• mo271 and contributors, PrimeNumberTheoremAnd, pinned dependency. Source.
• The Formal Conjectures Authors, Formal Conjectures, RiemannZetaValues.irrational_five. Pinned challenge source.

Motivation

The Riemann zeta function at integers splits into two very different worlds. At even arguments Euler's formula $\zeta(2k) = (-1)^{k+1} B_{2k} (2\pi)^{2k} / (2\,(2k)!)$ shows every $\zeta(2k)$ is a rational multiple of $\pi^{2k}$, hence irrational and even transcendental. At odd arguments almost nothing is known. The single exception is $\zeta(3)$, proved irrational by R. Apéry in 1978 (Astérisque 61 (1979), 11–13). For every other odd argument $\zeta(5), \zeta(7), \zeta(9), \dots$ the arithmetic nature is open to this day: no individual value is known to be irrational.

What is known are localisation results, which assert that an irrational number occurs somewhere in a finite or infinite list of odd zeta values without saying where.

• 2000 — T. Rivoal proves that infinitely many of $\zeta(3), \zeta(5), \zeta(7), \dots$ are irrational; more precisely the dimension of the $\mathbb{Q}$-vector space spanned by $1, \zeta(3), \zeta(5), \dots, \zeta(2k+1)$ grows at least like $\tfrac{1}{3}\log k$ (C. R. Acad. Sci. Paris 331 (2000), 267–270).
• 2001 — Rivoal, and independently W. Zudilin, prove that at least one of the nine numbers $\zeta(5), \zeta(7), \dots, \zeta(21)$ is irrational.
• 2001 — Zudilin sharpens the list to four numbers: at least one of $\zeta(5), \zeta(7), \zeta(9), \zeta(11)$ is irrational (Uspekhi Mat. Nauk 56:4 (2001), 149–150; English translation, Russian Math. Surveys 56:4 (2001), 774–776). This is the mission's source and remains the sharpest known localisation among small odd zeta values.

Setting

All objects below are those of the source note, in its own notation.

Fix odd integers $q$ and $r$ with $q \ge r + 4$, and positive integers $\eta_0, \eta_1, \dots, \eta_q$ subject to $\eta_1 \le \eta_2 \le \dots \le \eta_q < \eta_0/2$ and

For each integer $n > 0$ put $h_0 = \eta_0 n + 2$ and $h_j = \eta_j n + 1$ for $j = 1, \dots, q$, and consider the rational function

together with the linear form

Condition (1) gives $R_n(t) = O(t^{-2})$, so the series converges.

Two arithmetic quantities control the denominators of $F_n$. Write $D_N$ for the least common multiple of $1, 2, \dots, N$, put $m_j = \max\{\eta_r,\ \eta_0 - 2\eta_{r+1},\ \eta_0 - \eta_1 - \eta_{r+j}\}$ for $j = 1, \dots, q-r$, and set

the product running over primes, where $\varphi$ is the integer-valued, nonnegative, $1$-periodic function

The growth of $F_n$ is governed by the saddle points, the zeros of

and by the auxiliary function

Writing $\tau_0$ for the zero with $\operatorname{Im}\tau_0 > 0$ of largest real part, the two competing constants of the method are

with $\psi$ the logarithmic derivative of the gamma function.

Formalization targets

Goal

The goal fixes no witness: the statement is satisfied as soon as one of the four values is irrational, and remains the honest form of what the source proves. It is deliberately weaker than the (open) statement that each $\zeta(2k+1)$ is irrational, and weaker than any claim identifying which of the four is irrational.

Route to the goal

The milestones follow the source's own numbering: Lemma 1 (the linear form and its denominators), the prime-number-theorem asymptotics of $D_{m_j n}$, Lemma 2 (the saddle-point asymptotics of $F_n$ for $r = 3$), the small-values criterion for display (4), Lemma 3 (the criterion $C_0 > C_1$), and the numerical verification of $C_0 > C_1$ at $r = 3$, $q = 13$, $\eta_0 = 91$, $\eta_1 = \eta_2 = \eta_3 = 27$, $\eta_j = 25 + j$ for $4 \le j \le 13$, where $C_0 = 227.58019641\ldots$ and $C_1 = 226.24944266\ldots$.

Significance

The result itself. Together with Apéry's theorem it gives the smallest list of small odd zeta values known to contain an irrational number, and it fixes the current record of the Ball–Rivoal hypergeometric method: the same machinery yields quantitative lower bounds for the dimension of the $\mathbb{Q}$-span of odd zeta values, and any improvement of the arithmetic factor $\Phi_n$ or the saddle-point estimate propagates directly to those bounds.

Formalizing it. The result is proved mathematically; nothing here is open. What is missing is a machine-checked proof. Mathlib contains the Riemann zeta function, the gamma function, and the prime number theorem, but not Apéry's theorem, not the Ball–Rivoal construction, and not the Chudnovsky–Rukhadze–Hata arithmetic method. A complete development produces reusable infrastructure: integrality of very-well-poised hypergeometric sums, the $\varphi$/$\Phi_n$ denominator-saving mechanism, saddle-point asymptotics for a Barnes-type complex integral, and the standard linear-form irrationality criterion.

Difficulty

The obvious route — exhibit explicit rational approximations to a single $\zeta(2k+1)$ and estimate them — fails, and that failure is the content of the field: no construction is known that separates a single odd zeta value. Zudilin's construction instead produces one real sequence $F_n$ that is simultaneously a $\mathbb{Q}$-linear form in $1, \zeta(5), \zeta(7), \zeta(9), \zeta(11)$; irrationality of some coefficient's argument then follows from the two-sided estimate, but the argument is blind to which one.

The three hard steps are independent of one another. First, integrality: the coefficients of $F_n$ have denominators controlled by $D_{m_1 n}^r D_{m_2 n}\cdots D_{m_{q-r}n}$, and the extra factor $\Phi_n$ — a product of prime powers extracted from the $\varphi$-function — must be divided out; this is a delicate $p$-adic valuation count. Second, asymptotics: the exact exponential rate of $|F_n|$ comes from a complex integral over a vertical line, evaluated by the saddle-point method at a zero of a degree-$16$ polynomial with no closed form. Third, the final comparison $C_0 > C_1$ is a numerical inequality between two transcendental-looking constants that must be certified rigorously, including a Stieltjes integral of a piecewise-constant function against the digamma function.

Formalization scope

Statements are formalized over the reals, with $\zeta(k)$ for an integer $k \ge 2$ represented by the convergent series $\sum_{n\ge 1} n^{-k}$ (zetaR); a bridging statement identifies it with Mathlib's riemannZeta at natural arguments, so the goal theorem may be stated with riemannZeta as it already is in the platform library. Admissible parameter sets are a structure carrying $q$, $r$, the sequence $\eta$, and the hypotheses of the source, so no theorem quantifies over parameters the source excludes. R is a real-valued function of a real variable built from Real.Gamma, and $F_n$ is the tsum of its $(r-1)$-st iteratedDeriv at natural arguments; convergence is a separate milestone rather than a silent assumption, so that the value is not asserted to exist by fiat. $\varphi$ is the infimum over $y \in [0,1)$ of the integer-valued expression above, $\Phi_n$ a finite product over primes $p \le m_{q-r}n$ with $\eta_0 n < p^2$ (the integer form of $\sqrt{\eta_0 n} < p$), and $D_N$ the Finset.lcm of $1, \dots, N$. The Stieltjes integral $\int_0^1 \varphi\,\mathrm{d}\psi$ is written as $\int_0^1 \varphi(x)\psi'(x)\,\mathrm{d}x$, which agrees with the Riemann–Stieltjes integral because $\psi$ is continuously differentiable on $(0,1]$; $f_0$ uses the principal branch of the complex logarithm.

The saddle point $\tau_0$ is not defined by a choice function: every statement that mentions it takes it as a parameter together with the hypotheses "root of the polynomial", "positive imaginary part", "maximal real part among such roots", and the two side conditions $\operatorname{Re}\tau_0 < \eta_0$ and $\operatorname{Im} f_0(\tau_0)\notin\pi\mathbb{Z}$ of Lemma 2. No milestone is vacuous: for the concrete parameter set of the source such a $\tau_0$ exists, with $\tau_0 \approx 87.479005 + 3.328207\,i$.

Contributions of any size are welcome, including partial infrastructure: $p$-adic valuation lemmas for products of factorials, asymptotics of Finset.lcm, saddle-point estimates, and interval-arithmetic machinery for the final numerical comparison.

Selected references

• R. Apéry, Irrationalité de $\zeta(2)$ et $\zeta(3)$, Astérisque 61 (1979), 11–13. numdam
• T. Rivoal, La fonction zêta de Riemann prend une infinité de valeurs irrationnelles aux entiers impairs, C. R. Acad. Sci. Paris Sér. I Math. 331 (2000), 267–270. doi:10.1016/S0764-4442(00)01624-4
• T. Rivoal, Propriétés diophantiennes des valeurs de la fonction zêta de Riemann aux entiers impairs, Thèse de doctorat, Univ. de Caen, 2001.
• W. V. Zudilin, One of the numbers $\zeta(5), \zeta(7), \zeta(9), \zeta(11)$ is irrational, Uspekhi Mat. Nauk 56:4 (2001), 149–150. doi:10.4213/rm427

Call a set of reals a Sidon set when all its pairwise sums are distinct: if $a + b = c + d$ with all four in the set, then $\{a,b\} = \{c,d\}$.

The goal. There is an absolute constant $c > 0$ such that every finite set $X$ of positive reals contains a Sidon subset $S$ with $|S| \ge c\sqrt{|X|}$.

This is the lower bound half of Erdos problem 530, which Riddell posed and which asks for the order of the largest guaranteed Sidon subset. That problem is open: it asks whether the guarantee is asymptotically $N^{1/2}$, and the constant is not known. What is settled is the order, by Komlos, Sulyok, and Szemeredi, Linear problems in combinatorial number theory, Acta Math. Acad. Sci. Hungar. 26 (1975) 113-121, as a case of a general theorem about linear equations. Erdos had previously observed the cube-root lower bound and the matching $(1+o(1))N^{1/2}$ upper bound from $A = \{1, \dots, N\}$. A second and much shorter proof is in Bailleul and Riblet, arXiv:2605.03181.

The exponent is the whole problem

A one-paragraph argument gives $|S| \ge c|X|^{1/3}$: take a Sidon subset $S$ of maximum size, and note that every $x$ outside it satisfies $x = c + d - b$ or $x = (c+d)/2$ for elements of $S$, so $|X| \le 3|S|^3$.

That cube root is not a weak first attempt, it is the ceiling for any argument that only counts. An arithmetic progression of length $n$ has additive energy of order $n^3$, so a probabilistic argument cannot see the difference between it and a generic set. Getting from $1/3$ to $1/2$ requires using the structure of the set, and that is what both published proofs do.

The idea both proofs share

Compress, then pigeonhole against a known Sidon set.

An arbitrary finite set of reals has no arithmetic to work with, so first move it into $\mathbb{Z}$: a finite set spans a finite dimensional $\mathbb{Q}$-vector space, and a generic rational functional separates its points while preserving every relation $a + b = c + d$. Then squeeze the resulting integers into an interval of length comparable to their number, keeping a constant fraction of them and keeping the property that a Sidon subset of the image lifts to one of the original. Finally intersect with a translate of the Erdos-Turan Sidon set, which has about $\sqrt{N}$ elements inside $\{0, \dots, N-1\}$. A set of size $\Theta(n)$ inside $[1,n]$ meets some translate of a Sidon set of size $\sqrt{n}$ in order $\sqrt{n}$ points, and that intersection is Sidon.

The two proofs differ only in the compression step, and the mission carries both.

The two routes

The 1975 route compresses in four lemmas driven by a remainder map: choose a modulus $q$ dividing no difference, dilate so that the remainders are small, and observe that a small remainder map preserves $a + b = c + d$. Finding the modulus needs a prime counting bound.

The 2026 route replaces all four with one averaging lemma over a real rotation parameter $\theta$, keeping the elements whose fractional part of $am\theta$ is below $1/2$, where no carry occurs. No prime counting appears anywhere.

Notes on the formalization

Every item is stated in Mathlib primitives alone, so the mission needs no definition items. The Sidon condition, the Erdos-Turan construction, and the reduction relation of the 1975 route are all written out at each use.

The published 2026 proof finishes with Singer's 1938 covering of $\mathbb{Z}/(q^2+q+1)\mathbb{Z}$ by $q+1$ Sidon sets. Mathlib has no perfect difference sets, so the mission uses averaging over translates instead. It does the same job at the same order and gives a worse constant, which costs nothing because the goal asserts only that some $c > 0$ exists.

Two lemmas of the 1975 paper are deliberately absent. A local formalization of Lemma 2 and Lemma 6 turned out to be false as stated, machine-checked in both cases, so neither is offered here as a milestone. Those are errors in that rendering rather than in the paper, and the 2026 route reaches the goal without either. Lemma 1' is absent for the same practical reason: the 2026 route does not need it.

Call $A \subseteq \mathbb{Z}/2^n\mathbb{Z}$ cube-free if no triple $x, y, z$ has all seven of $x$, $y$, $z$, $x+y$, $y+z$, $z+x$, $x+y+z$ inside $A$. The triple is unconstrained, so a degenerate one counts. Write $f(n)$ for the largest size of a cube-free subset.

The conjecture. $f(n) \le \frac{5}{8} 2^n$ for every $n$.

This is Conjecture 5.1 of Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of $\mathbb{Z}_{2^n}$, arXiv:1810.01225. It has been open since October 2018, and a 2026 journal paper still names it as conjectured: Yuchen Meng, On Cube-Free Problems, Electron. J. Combin. 33(1) (2026) #P1.16.

The constant is attained

The bound is sharp, and the extremal set is explicit: $A = \{v : v \bmod 8 \in \{1,3,4,5,7\}\}$, the odd residues together with those congruent to 4 mod 8. Its size is $2^{n-1} + 2^{n-3} = \frac{5}{8} 2^n$. In the layer language of Long and Wagner this is $C_3 = L_1 \cup L_3$.

What is known

The conjecture holds for unions of layers. That is Long-Wagner Theorem 1.10 at $d = 3$, and it is the largest class on which the conjectured constant is proved.

For arbitrary sets the best published unconditional bound is $f(n) < \frac{2}{3} 2^n$. Meng calls this bound "quite trivial" and gives it in one paragraph for every cyclic group, so it should not be read as progress toward $5/8$. The residual gap is exactly $\frac{2}{3} - \frac{5}{8} = \frac{1}{24}$, that is $2^n/24$ elements.

Small values are $f(1) = 1$, $f(2) = 2$, $f(3) = 5$, $f(4) = 10$, $f(5) = 20$, $f(6) = 40$, $f(7) = 80$, matching $2^{n-1} + 2^{n-3}$ from $n = 3$ on.

State those values honestly. They come from solver searches, Gurobi in Long and Wagner for $n \le 7$ and an independent SAT reproduction. The SAT half that matters, the unsatisfiability of "a cube-free set of size 81 exists at $n = 7$", is a solver claim with no proof certificate checked and no kernel check behind it. The witness half is verified: a set of exactly 80 elements was produced and re-checked cube-free. So $f(7) \ge 80$ is solid and $f(7) \le 80$ is not certified. Nothing in this mission rests on either.

What the items are

The goal item is the conjecture itself, for $n \ge 4$, and it is open. Every other item is a milestone that is proved mathematics, and the two closed instances $n = 4$ and $n = 5$ are stated separately because they are the only cases of the goal that a proof assistant has actually settled here.

The chain runs: the base case mod 8 by exhaustion, monotonicity under subsets, the bridge between the membership form and the Finset form of the forbidden configuration, sharpness, the odd-residue tight case, the layer-union theorem, the two-thirds bound, and then $n = 4$ and $n = 5$.

Notes on the formalization

Six definitions live in one definition item, Def_Z2nCubeFreeLayers: HasCube, CubeFree, config, ConfigFree, layerIdx and IsLayerUnion. layerIdx is written through the 2-adic valuation rather than through a congruence, because the congruence form leaves $0$ in no layer at all and needs the last layer special-cased.

CubeFree and ConfigFree are two encodings of the same condition and they are not definitionally equal, because config collapses duplicates on a degenerate triple. Their equivalence is a milestone rather than an assumption.

The Lagrange spectrum describes the asymptotic quality of rational approximation to irrational real numbers. The Markov spectrum is defined through minima of indefinite binary quadratic forms. Freiman determined the exact starting point of the maximal half-line contained in each spectrum.

This mission aims to formalize his theorem that this half-line is $[c_F,\infty)$, where

The formalization must establish membership of every real number at least $c_F$, including the endpoint, and show that no half-line starting below $c_F$ is contained in either spectrum.

The sources are Freiman's Russian monograph and an accompanying detailed reconstruction of its proof, with an English translation, exact computational certificates, and verification scripts. The project follows Freiman's continued fraction construction, incorporating the corrections and supplementary arguments established in the report.

The intended result is a complete Lean 4 proof. Its scope includes the equivalence of the classical and continued fraction definitions of the spectra, the infinite constructions that realize spectral values, and the exact finite calculations used in the argument.

Source material

• Proof report (PDF) — the complete argument, exact certificate appendices and corrected English translation of Freiman's Russian text. Download PDF.
• Verification package (ZIP) — the report, its LaTeX sources, the Russian source, certificate data, verification programs and reproduction instructions. Download ZIP.

Start with README.md and PROOF_GUIDE.md in the package. The files formalization/MISSION.md and formalization/MILESTONES.md describe the scope and proposed stages of the formalization. For reproducing the report, use the PDF and sources contained in the ZIP.

References to the report in the individual source fields use its printed page numbers.

Why construct a p-adic L-function?

A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).

The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 (MTT); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).

Modular forms, periods, and measures

Fix a prime $p$, a positive integer $N$, and a weight $k\ge2$. Let $f$ be a normalized cuspidal Hecke eigenform of weight $k$ on $\Gamma_1(N)$ with nebentypus $\epsilon$ and Fourier coefficients $a_n$ (necessarily algebraic). Fix embeddings $\iota_\infty:\overline{\mathbb Q}\hookrightarrow\mathbb C$ and $\iota_p:\overline{\mathbb Q}\hookrightarrow\mathbb C_p$. No condition $p\nmid N$ is imposed. The character $\epsilon$ is extended by zero on nonunits modulo $N$.

The form is ordinary when $|\iota_p(a_p)|_p=1$. The ordinary root $\alpha$ is the root of

with $|\alpha|_p=1$. This convention also covers the $U_p$ case: if $p\mid N$, then $\epsilon(p)=0$ and the unit root is $\iota_p(a_p)$ (MTT I.§12).

A measure means a continuous $\mathbb C_p$-linear functional on the continuous functions $C(\mathbb Z_p^\times,\mathbb C_p)$. It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's AbstractMeasure on (PadicInt p)ˣ.

The two periods $\Omega^+$ and $\Omega^-$ normalize the signed modular integrals. Write

and use $(\Phi_j(r)+s(-1)^j\Phi_j(-r))/2$ for sign $s\in\{+1,-1\}$. A period system specifies nonzero periods, algebraic normalized values for $0\le j\le k-2$, and finite generation over $\mathbb Z$ of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in MTT I.§2; see also the explicit treatment of general eigenforms in Williams, §11.7.

Formalization targets

The goal is to construct an ordinary root, a period system, and a measure $\mu$ with the following interpolation property. Let $\chi$ be a primitive Dirichlet character of conductor $m=p^n$, where $n\ge0$, and let $0\le j\le k-2$. Put $s=\chi(-1)(-1)^j$. With the positive-exponential Gauss sum $\tau(\chi)=\sum_{a\bmod m}\chi(a)e^{2\pi ia/m}$, define the algebraic number $A_{\chi,j}$ by

The required identity is

where all algebraic character values in the following expression are transported by $\iota_p$:

This is the scalar period-normalized form of MTT I.§14. At $n>0$ both character values at $p$ vanish, leaving $\alpha^{-n}$. At $n=0$ the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.

Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.

What the formalization supplies

The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.

Where the difficulty lies

Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.

Formalization scope and conventions

The cusp form is Mathlib's analytic CuspForm, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for $f_{\chi^{-1}}$, and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.

The embeddings share the abstract algebraic closure of $\mathbb Q$; there is no asserted continuous map from $\mathbb C$ to $\mathbb C_p$. The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including $2$, are allowed. Natural-number subtractions occur only in theorem contexts with $k\ge2$ and $j\le k-2$.

The signed projections use a factor of $1/2$. Their normalized measures are added, and the period sign is $\chi(-1)(-1)^j$. These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.

Selected references

• B. Mazur, J. Tate and J. Teitelbaum, On p-adic analogues of the conjectures of Birch and Swinnerton-Dyer, Inventiones Mathematicae 84 (1986), 1–48, Chapter I, §§1–4 and 7–14. DOI; digitized original.
• G. Shimura, On the periods of modular forms, Mathematische Annalen 229 (1977), 211–221. DOI.
• C. Williams, An introduction to p-adic L-functions II: Modular forms, lecture notes, §§11.6–11.8, particularly Proposition 11.21, for period normalization of general eigenforms. Author's notes.

Primes in progressions, uniformly in the modulus

Applying the circle method to an additive problem about primes requires counting primes in arithmetic progressions with an error term uniform in the modulus: the modulus is not fixed in advance, it grows with the size of the numbers being represented. The Siegel–Walfisz theorem is the classical statement of that uniformity, valid for every modulus up to a fixed power of $\log x$, and it is the one analytic ingredient the standard proof of Vinogradov's three primes theorem cannot do without.

The history is a sequence of partial uniformities:

• 1837. Dirichlet proves that every progression $a \bmod q$ with $(a,q)=1$ contains infinitely many primes, for each fixed $q$, with no rate (Dirichlet's theorem).
• 1896–1899. De la Vallée Poussin proves the prime number theorem with the error term $O(x e^{-c\sqrt{\log x}})$, and extends the zero-free region from $\zeta$ to $L(s,\chi)$, obtaining the prime number theorem in progressions for each fixed $q$ (PNT).
• 1918–1935. Landau and Page isolate the obstruction to uniformity: a single real zero near $s=1$, attached to a quadratic character. Landau shows at most one of two distinct real primitive characters can have such a zero; Page shows at most one modulus below a given bound can, yielding unconditional uniformity for $q$ up to a bounded power of $\log x$ (Page's theorem).
• 1935. Siegel proves $L(1,\chi) \gg_\varepsilon q^{-\varepsilon}$ for real primitive $\chi$, at the price of an ineffective constant (Siegel).
• 1936. Walfisz combines Siegel's bound with the de la Vallée Poussin machinery and obtains uniformity for every fixed power $q \le (\log x)^A$ (Walfisz).
• 1937. Vinogradov proves that every sufficiently large odd integer is a sum of three primes (Vinogradov's theorem).
• 2013. Helfgott removes the "sufficiently large", settling ternary Goldbach for all odd $n > 5$ (arXiv:1312.7748).

Setting

The von Mangoldt function $\Lambda(n)$ equals $\log p$ if $n = p^m$ is a prime power and $0$ otherwise. The Chebyshev function $\psi(x) = \sum_{n \le x} \Lambda(n)$ counts primes with weights; the prime number theorem is the assertion $\psi(x) \sim x$.

A Dirichlet character modulo $q$ is a multiplicative function $\chi : \mathbb{Z}/q\mathbb{Z} \to \mathbb{C}$, supported on the units and taking root-of-unity values there. The principal character $\chi = 1$ is the indicator of the units; a character is quadratic (real) if $\chi^2 = 1$ and $\chi \neq 1$, and primitive if it is not induced by a character of a proper divisor of $q$. The Dirichlet $L$-function $L(s,\chi) = \sum_{n\ge 1}\chi(n)n^{-s}$, defined for $\operatorname{Re} s > 1$, extends meromorphically to $\mathbb{C}$, entire except for a simple pole at $s = 1$ when $\chi$ is principal.

The two counting functions of the mission are the twisted von Mangoldt sum and the progression sum

related by finite character orthogonality. Write $\delta_\chi = 1$ for $\chi$ principal and $\delta_\chi = 0$ otherwise. A zero $\beta \in (0,1)$ of $L(s,\chi)$ lying inside the classical zero-free region is an exceptional zero (a Siegel zero); the set of such zeros for a given $\chi$ is the exceptional set $E$, which the results below constrain to have at most one element.

Formalization targets

The attack path follows Davenport, Multiplicative Number Theory, 3rd ed., §§14, 18, 20, 21, 22.

(1) zero_free_region (§14, pp. 88–96). There is an absolute $c>0$ such that for every $q \ge 1$ and every $\chi \bmod q$,

with at most one exception, which is real, lies in $(0,1)$, is a simple zero, and can occur only for quadratic non-principal $\chi$.

(2) pnt_dlvp (§18, pp. 111–114). For some $c > 0$ and all $x \ge 2$,

(3) psi_char_of_region (§20, pp. 121–125). For a region constant $c>0$ there are $c_1, c_2 > 0$ such that, whenever $E$ is an exceptional set for $\chi \bmod q$ with respect to $c$ and $q \le \exp(c_2\sqrt{\log N})$,

(4) siegel (§21, pp. 126–131). For every $\varepsilon > 0$ there is $C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,

(5) siegel_zero (§21, second form). For every $\varepsilon > 0$ there is $C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,

(6) siegelWalfisz (§22, pp. 132–134). For every $A > 0$ there are $C, c > 0$ such that for all $q \ge 1$, all $\chi \bmod q$, and all $N \ge 2$ with $q \le (\log N)^A$,

This is literally the platform proposition ThreePrimes.SiegelWalfisz.

A corollary, not a milestone, records the progression form siegel_walfisz_ap: for $(a,q)=1$ and $q \le (\log N)^A$,

Goal (three_primes, §26). There is $N_0$ such that every odd $n \ge N_0$ is a sum of three primes. It follows from milestone (6) by the existing platform theorem deducing ThreePrimes.ThreePrimesExistence from ThreePrimes.SiegelWalfisz. The goal leaves $N_0$ unspecified rather than hard-coding a numeric threshold, so it is not invalidated by later improvements to that threshold.

What the result gives, and what remains to be formalized

Siegel–Walfisz is the standard uniform input downstream of which sit the circle method for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without it, the three primes theorem's major-arc analysis has no main term.

Platform status is the reason this mission exists. A complete, machine-checked formalization of the three primes theorem already exists in the namespace ThreePrimes (by user tabbott), following Vaughan, The Hardy–Littlewood Method, Ch. 3, and Davenport §26. It is conditional: it takes Siegel–Walfisz as an explicit hypothesis ThreePrimes.SiegelWalfisz. Discharging that hypothesis makes the three primes theorem unconditional, and is the whole content of this mission.

Mathlib contains the analytic continuation of $L(s,\chi)$ (DirichletCharacter.LFunction), its functional equation, the non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$, Dirichlet's theorem, and the Chebyshev function. It does not contain the zero-free region for $L(s,\chi)$, the explicit formula for $\psi(x,\chi)$, Siegel's theorem, or Siegel–Walfisz. The platform additionally hosts the PNT+ project contour machinery for $\zeta$ — Borel–Carathéodory, the $3 + 4\cos\theta + \cos 2\theta$ inequality, a zero-free rectangle, and MediumPNT, $\psi(x) = x + O(x\exp(-c(\log x)^{1/10}))$. That is a template for the $L(s,\chi)$ analogues, not a proof of them, and its error term is weaker than the de la Vallée Poussin form milestone (2) asks for.

Where the obvious argument fails

The first idea is to run the $\zeta$ argument character by character. It works for complex $\chi$ and breaks for real ones. The positivity device that pushes zeros off $\operatorname{Re} s = 1$ compares $\chi$, $\chi^2$ and the trivial character at nearby points; when $\chi$ is quadratic, $\chi^2$ is principal and contributes the pole of $L(s,\chi_0)$ at $s = 1$ at exactly the height where the putative zero sits, so the inequality degrades from "no zeros" to "at most one zero" and stops there. Every later step inherits that unexcluded zero: milestone (3) can only be stated with the $N^\beta/\beta$ term present, and milestone (6) is exactly the assertion that for $q \le (\log N)^A$ this term is small — which Siegel's ineffective bound supplies and nothing effective is known to.

A second shortcut, deducing uniformity from Mathlib's non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$ together with Dirichlet's theorem, also fails: those results are qualitative, carry no rate, and are not uniform in $q$.

Formalization scope

Sums run over $n < N$ with $N \in \mathbb{N}$, matching Vino.vmSumChar and ThreePrimes.SiegelWalfisz; Davenport sums over $n \le x$. The two differ by the single term $\Lambda(N) \le \log N$, negligible against every error term above. Milestone (2) alone uses a real argument, via Mathlib's Chebyshev.psi. $L(s,\chi)$ is Mathlib's DirichletCharacter.LFunction, so no continuation is reconstructed.

The zero-free region is Davenport.InRegion c q s, namely $\operatorname{Re} s \ge 1 - c/\log(q(|\operatorname{Im} s| + 2))$; the exceptional zero is packaged as IsExceptionalSet c χ E: $E$ is a subsingleton, every element is a real zero of $L(\cdot,\chi)$ in $(0,1)$ and can exist only for quadratic non-principal $\chi$, and $L(s,\chi) \neq 0$ at every $s \neq 1$ of the region outside $E$. Milestone (1) adds simplicity as $L'(\beta,\chi) \neq 0$ for $\beta \in E$.

Milestone (3) takes the region constant $c > 0$ as a parameter rather than importing it from milestone (1), so the milestones can be attempted in any order. For large $c$ the hypothesis IsExceptionalSet c χ E may be unsatisfiable for some $\chi$, making the statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing reading: milestone (1) produces a definite small $c > 0$ with a witness $E$ for every $\chi$, so instantiating milestone (3) at that $c$ discharges the hypothesis rather than voiding it.

Siegel's theorem is stated for χ.IsQuadratic, χ ≠ 1, χ.IsPrimitive characters, with the conclusion a lower bound on $\operatorname{Re} L(1,\chi)$; since $L(1,\chi)$ is real for real $\chi$, this is the value itself, not a weakening. The constants in milestones (4), (5) and (6) are ineffective; the statements are plain existentials, so ineffectivity is invisible to Lean, but no numeric constant can be extracted from anything downstream of them.

The principal character is included in the character-form statements, with main term $N$ (if χ = 1 then (N : ℂ) else 0); milestones (3) and (6) therefore contain the prime number theorem itself and cannot be proved by restricting to non-principal $\chi$. Milestone (6) requires $c > 0$ strictly, which is what makes $Ne^{-c\sqrt{\log N}}$ a genuine saving over the trivial $\psi(N,\chi) \ll N$; with $c = 0$ allowed it would be empty.

Beyond the six milestones, a complete development needs Hadamard factorization for $L(s,\chi)$ as an entire function of order $1$, the zero-counting estimate $N(T,\chi)$ (§16, pp. 101–103), the truncated explicit formula for $\psi(x,\chi)$ (§19, pp. 115–120), Perron-type contour truncation, and the imprimitive-to-primitive reduction $|\psi(N,\chi) - \psi(N,\chi^{*})| \ll (\log q)(\log N)$. All of it is reusable well beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's theorem, and effective Chebotarev. Contributions of these supporting results, of alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the $\pi(x;q,a)$ versions, and of sharper constants are welcome.

Selected references

• H. Davenport, Multiplicative Number Theory, 3rd ed., revised by H. L. Montgomery, GTM 74, Springer, 2000. §§14, 18, 20, 21, 22, 26. doi:10.1007/978-1-4757-5927-3
• H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I: Classical Theory, Cambridge University Press, 2007. Ch. 11–12 (Theorems 11.3, 11.14, 11.16, 12.10; Corollaries 11.10, 11.12, 11.17, 11.19). doi:10.1017/CBO9780511618314
• R. C. Vaughan, The Hardy–Littlewood Method, 2nd ed., Cambridge University Press, 1997. Ch. 3. doi:10.1017/CBO9780511470929
• C. L. Siegel, Über die Classenzahl quadratischer Zahlkörper, Acta Arithmetica 1 (1935), 83–86. eudml:205054
• A. Walfisz, Zur additiven Zahlentheorie II, Mathematische Zeitschrift 40 (1936), 592–607. doi:10.1007/BF01218882
• I. M. Vinogradov, Representation of an odd number as a sum of three primes, Doklady Akad. Nauk SSSR 15 (1937), 291–294. Vinogradov's theorem
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. arXiv:1312.7748
• Siegel–Walfisz theorem, Wikipedia. link
• Page theorem, Encyclopedia of Mathematics. link
• A. Kontorovich et al., PrimeNumberTheoremAnd (PNT+), Lean formalization project. github
• Mathlib, Mathlib.NumberTheory.LSeries.DirichletContinuation. docs

Determine the exact second-order term in the least possible largest factor in a factorization of $n!$ into distinct integers exceeding $n$, with the proposed rational constant $4029639598/25970038185$.

Motivation

An algorithm for linear programming is strongly polynomial if the number of arithmetic operations it performs is bounded by a polynomial in the dimension of the problem alone (the number of variables and constraints), independently of the bit lengths of the numbers in the input. Many combinatorial optimization problems are linear programs over polyhedra of the form $P = \{x \in \mathbb{R}^n : Ax \le b\}$ whose constraint matrix $A$ has entries $0, +1, -1$, but whose objective vector $w$ is an arbitrary rational weight vector. Polynomial-time algorithms for such problems (for instance the ellipsoid-based algorithms of Grötschel, Lovász and Schrijver for maximum-weight cliques in perfect graphs, submodular flows, and matroid polyhedra) have running times that depend on the length of $w$.

Frank and Tardos (Combinatorica 1987) remove this dependence once and for all: they replace $w$ by an integral objective $\tilde w$ whose entries have $O(n^3)$ bits and which has exactly the same optimal solutions and the same optimal dual bases as $w$ over every such polyhedron. Any algorithm that is polynomial in $n$ and in the length of the objective then becomes strongly polynomial. The tool is simultaneous Diophantine approximation, used through the lattice-basis-reduction algorithm of Lenstra, Lenstra and Lovász (Math. Ann. 1982). The technique extends Tardos's strongly polynomial algorithm for linear programs with small constraint matrices (Oper. Res. 1986), which applies only to explicitly given programs.

Setting

For $x \in \mathbb{R}^n$ write $\|x\|_\infty = \max_j |x(j)|$ and $\|x\|_1 = \sum_j |x(j)|$; $\operatorname{sign}$ takes the values $-1, 0, +1$.

Decomposition. Fix a positive integer $N$. A decomposition of $w \in \mathbb{R}^n$ is an expression

It satisfies condition (iii) if for $i = 2, \dots, k$ the vector $v_i$ is nonzero and $\lambda_i/\lambda_{i-1} \le 1/(N\|v_i\|_\infty)$: the coefficients decrease so quickly that each term is negligible against the previous one.

Preprocessing. Given a rational $w$ and $N$, the paper's preprocessing algorithm finds a decomposition with $k \le n$, condition (iii), and the size bound (ii)' $\|v_i\|_\infty \le 2^{n^2+n}N^n$, and outputs

Linear programs. Let $A$ be an $m \times n$ matrix with entries in $\{0, \pm 1\}$ and $b \in \mathbb{R}^m$. The primal program is $\max\{wx : Ax \le b\}$ and the dual program is $\min\{yb : yA = w,\ y \ge 0\}$. A point $\bar x \in P$ is $w$-maximal if $w\bar x = \max(wx : x \in P)$. A dual basis is a maximal set of row indices of $A$ whose rows are linearly independent; it determines at most one $y$ with $yA = w$ supported on it (the basic dual solution), and it is an optimal dual basis if that $y$ exists and is optimal for the dual program.

Formalization targets

Goal — Theorem 4.2 (p. 58)

For every $w \in \mathbb{Q}^n$, with $N = (n+1)! + 1$, there is $\tilde w \in \mathbb{Z}^n$ with

such that for every $0, \pm1$ matrix $A$ with $n$ columns and every $b$: (i) $x \in P$ is $w$-maximal if and only if it is $\tilde w$-maximal; (ii) a set of rows of $A$ is an optimal dual basis for $w$ if and only if it is one for $\tilde w$. The vector $\tilde w$ depends on $w$ only, not on $A$ or $b$.

Milestones

1. Dirichlet's theorem (p. 52): for $N \ge 1$ and $\alpha \in \mathbb{R}^n$ there are $p \in \mathbb{Z}^n$ and $1 \le q \le N^n$ with $|q\alpha(i) - p(i)| < 1/N$ for all $i$.
2. Theorem 3.1 (p. 53): every $w \in \mathbb{R}^n$ has a decomposition with $k \le n$, $\|v_i\|_\infty \le N^n$ and condition (iii).
3. Lemma 3.2 (pp. 54–55): under condition (iii), for integral $b$ with $\|b\|_1 \le N - 1$, $\operatorname{sign}(b \cdot w) = \operatorname{sign}(b \cdot v_j)$ for the smallest $j$ with $b \cdot v_j \ne 0$, and $b \cdot w = 0$ if there is no such $j$.
4. Theorem 3.3 (p. 56): the preprocessed $\tilde w$ satisfies $\|\tilde w\|_\infty \le 2^{4n^3}N^{n(n+2)}$ and $\operatorname{sign}(w \cdot b) = \operatorname{sign}(\tilde w \cdot b)$ for all integral $b$ with $\|b\|_1 \le N-1$.
5. The case $N = n+1$ (p. 55): an integral $\tilde w$ with $\|\tilde w\|_\infty \le 2^{4n^3}(n+1)^{n(n+2)}$ and $\tilde w(X) \le \tilde w(Y) \iff w(X) \le w(Y)$ for all subsets $X, Y$ of coordinates.
6. Lemma 4.1 (i) (p. 57): if $\operatorname{sign}(w' \cdot h) = \operatorname{sign}(w'' \cdot h)$ for all integral $h$ with $\|h\|_1 \le (n+1)!$, then $w'$ and $w''$ have the same maximizers over $\{Ax \le b\}$ for every $0, \pm1$ matrix $A$.
7. Lemma 4.1 (ii) (p. 57): under the same hypothesis, a dual basis is optimal for $w'$ if and only if it is optimal for $w''$.

Significance

The result gives a general reduction: whenever a class of polyhedra with $0, \pm1$ constraint matrices admits an optimization algorithm that is polynomial in $n$ and in the length of the objective, it admits a strongly polynomial one. The paper applies this to maximum-weight cliques in perfect graphs, optimization over submodular flow polyhedra, and matroid polyhedra membership, and its Section 5 applies the same rounding to the integer programming algorithms of Lenstra and Kannan. The subset-sum corollary (milestone 5) is independently useful: every rational weight function on a finite set can be replaced by an integral one with $O(n^3)$-bit entries that orders all subset sums identically.

All statements of this mission have been proved on paper since 1987. None is formalized on Prove2Me, and Mathlib contains only the one-dimensional Dirichlet approximation theorem. The mission produces a machine-checked version of the exact statements, with the explicit constants of the paper; the complexity claims (operation counts, strong polynomiality) are not part of it.

Difficulty

The goal combines two independent parts. The number-theoretic part (milestones 1–5) needs a multidimensional Dirichlet theorem, an induction producing the decomposition, and exact inequality chains with the constants $2^{n^2+n}N^n$ and $2^{4n^3}N^{n(n+2)}$. The linear-programming part (milestones 6–7) needs bounds on the entries of inverses of nonsingular $0, \pm1$ submatrices, the existence of optimal dual solutions supported on a dual basis, LP duality and complementary slackness. The obvious first idea, scaling $w$ to an integer vector by a common denominator, preserves every sign but gives no bound on $\|\tilde w\|_\infty$ in terms of $n$; the bound is the content of the theorem. Likewise, rounding each coordinate of $w$ separately to a fixed precision does not preserve the sign of $w \cdot b$ when $w \cdot b$ is tiny but nonzero.