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 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.

Formalization scope

Vectors are functions on Fin n: the input $w$ is rational (Fin n → ℚ) in the goal, in Theorem 3.3 and in the subset-sum corollary, as in the algorithm's input line; it is real in Theorem 3.1, Lemma 3.2 and Lemma 4.1, as on the page. Integral vectors are Fin n → ℤ, and $A$ is a Matrix (Fin m) (Fin n) ℤ with every entry in $\{-1, 0, 1\}$, cast to $\mathbb{R}$; $b \in \mathbb{R}^m$ is unrestricted. Decompositions are indexed by $i \in \{1, \dots, k\} \subseteq \mathbb{N}$ as in the paper. $\|b\|_1$ is always the explicit sum $\sum_j |b(j)|$, compared with $N - 1$ in $\mathbb{Z}$; $\|v\|_\infty$ of an integer vector is a natural number (supNorm). Sign equality uses SignType.sign and includes the zero case. Condition (iii) is stated multiplicatively together with $v_i \ne 0$, which the paper's quotient presupposes; without $v_i \ne 0$ Lemma 3.2 fails. An optimal dual basis is a maximal linearly independent set of row indices together with an optimal dual solution supported on it.

Two formalizations would make the goal trivial and are excluded: dropping the bound on $\|\tilde w\|_\infty$ (a multiple of $w$ then works), and letting $\tilde w$ depend on $A$ and $b$ (the goal states $\exists \tilde w$ before $\forall A, b$). The $0, \pm1$ assumption on $A$ is part of every Section 4 statement.

A complete development needs a multidimensional pigeonhole argument, determinant and adjugate bounds for $0, \pm 1$ matrices, and basic LP duality (strong duality, complementary slackness, basic optimal dual solutions); the last two are reusable across linear-programming missions. Proofs of individual milestones, reusable lemmas on LP duality, and alternative proofs of Dirichlet's theorem are all welcome.

Selected references

• A. Frank and É. Tardos, An application of simultaneous diophantine approximation in combinatorial optimization, Combinatorica 7(1) (1987) 49–65. https://doi.org/10.1007/BF02579200
• A. K. Lenstra, H. W. Lenstra Jr. and L. Lovász, Factoring polynomials with rational coefficients, Math. Ann. 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Operations Research 34(2) (1986) 250–256. https://doi.org/10.1287/opre.34.2.250
• M. Grötschel, L. Lovász and A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
• J. W. S. Cassels, An Introduction to the Theory of Numbers (title as printed in the paper's reference [2]), Springer, Berlin, 1971; cited in the paper as [2, Sect. 1.10] for Dirichlet's theorem.

Motivation

In 1985 R. S. Ward conjectured that "many (and perhaps all?) of the ordinary and partial differential equations that are regarded as being integrable or solvable may be obtained from the self-dual gauge field equations (or its generalizations) by reduction". The self-dual Yang–Mills (SDYM) equations are therefore often called the master integrable system: choosing a gauge algebra and a symmetry group to reduce by produces, on the one hand, the classical soliton equations and the Painlevé transcendents, and on the other — once infinite-dimensional gauge algebras are allowed — a family of third-order equations whose solutions have movable natural barriers and are therefore not of Painlevé type.

This mission formalizes the endpoint of one such reduction chain, as surveyed by Ablowitz, Chakravarty and Halburd, Integrable systems and reductions of the self-dual Yang–Mills equations, J. Math. Phys. 44 (2003) 3147–3173, Section V. Reducing SDYM to functions of a single variable gives the Nahm equations; taking the gauge algebra to be the divergence-free vector fields on $S^3$ turns them into a matrix flow which, after diagonalizing the symmetric part, becomes the generalized Darboux–Halphen system. Its trace is governed by the Chazy equation, written down by Chazy in 1909, and — this is the paper's historical observation — the Chazy equation is equivalent to the differential system Ramanujan derived in 1916 for the Eisenstein series $P = E_2$, $Q = E_4$, $R = E_6$. Chazy and Ramanujan worked on the same equation at nearly the same time and apparently did not know it.

Setting

Throughout, $t$ and $q$ are complex variables and all functions are complex-valued; a "solution on $s$" means the stated derivative identities hold at every point of a set $s \subseteq \mathbb{C}$.

The classical Chazy equation is the third-order equation

The classical Darboux–Halphen system is the first-order system for $\omega_1,\omega_2,\omega_3$

together with its two cyclic images. It arose in Darboux's study of triply orthogonal surfaces and was solved by Halphen. Its generalized form adds a term $\tau^2 = \tau_1^2+\tau_2^2+\tau_3^2$ to each right-hand side, where $\dot\tau_1 = -\tau_1(\omega_2+\omega_3)$ and cyclically.

Ramanujan's system is