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

Problem Statement & Context

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

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

Main Target Theorem

Motivation

Write the primes in increasing order, take the absolute differences of consecutive entries, take the absolute differences of the resulting row, and repeat. Every row produced this way appears to begin with $1$:

$$\begin{array}{llllllll} 2 & 3 & 5 & 7 & 11 & 13 & 17 & \dots\\ 1 & 2 & 2 & 4 & 2 & 4 & \dots\\ 1 & 0 & 2 & 2 & 2 & \dots\\ 1 & 2 & 0 & 0 & \dots\\ 1 & 2 & 0 & \dots \end{array}$$

Gilbreath's conjecture asserts that this never fails. The observation is due to Norman L. Gilbreath (1958), who rediscovered a statement already published by François Proth in 1878 together with an argument that is not accepted as a proof. It is attractive because it is elementary to state and because it is one of the few statements about the primes whose difficulty is not visibly analytic: it concerns the combinatorics of iterated differences rather than the distribution of primes directly.

Timeline.

• 1878 — Proth states the property and publishes a proof that is now regarded as erroneous.
• 1958 — Gilbreath rediscovers the pattern; it circulates as a conjecture.
• 1959 — Killgrove and Ralston verify the leading entry for the first $63{,}418$ rows (MTAC 13 (1959), 121–122).
• 1993 — Odlyzko reports a verification of the leading entry for all rows of index at most $\pi(10^{13}) \approx 3.4 \times 10^{11}$, using an argument that propagates a long block of entries lying in $\{0,2\}$ downwards through the triangle (Math. Comp. 61 (1993), 373–380).

No proof is known.

Setting

Let $p_0 = 2 < p_1 = 3 < p_2 = 5 < \dots$ be the increasing enumeration of the prime numbers, indexed from $0$. Define the rows of the Gilbreath triangle by

$$d^0(n) = p_n, \qquad d^{k+1}(n) = \bigl| d^{k}(n+1) - d^{k}(n) \bigr| \quad (k, n \ge 0).$$

Thus $d^k$ is an infinite sequence of natural numbers for every $k$, row $0$ is the sequence of primes, row $1$ is the sequence of prime gaps $p_{n+1}-p_n$, and each later row is the sequence of absolute differences of consecutive entries of the row above it. Only the leading entry $d^k(0)$ of each row is at issue.

More generally, for an arbitrary sequence $a : \mathbb{N} \to \mathbb{N}$ write $(\Delta a)(n) = |a(n+1) - a(n)|$ and $\Delta^j a$ for the $j$-fold iterate, so that $d^k = \Delta^k p$.

Formalization targets

Goal

$$\forall k \ge 1,\qquad d^{k}(0) = 1 .$$

This is the conjecture in its standard form: every row after the row of primes begins with $1$. It fixes no constants and no ranges, so no computational advance can invalidate it.

Milestones

The milestone list collects the statements that a proof, or a further computational verification, would be built from: the two low-level structural facts about the triangle (row $1$ is the gap sequence; from row $1$ on, the leading entry is odd and all later entries are even), a finite verification of the first rows, and the two statements underlying Odlyzko's method — the propagation lemma for an arbitrary sequence beginning $1$ and continuing in $\{0,2\}$, and the reduction of the conjecture to the existence, for each row index, of an earlier row with a long enough block of entries in $\{0,2\}$.

Significance

The result itself. The conjecture is not known to imply other open statements about the primes, and its interest lies elsewhere: it is a test case for how much of the fine structure of the prime sequence is forced by coarse information. The propagation mechanism shows that the conjecture for a given row index follows from purely local data about an earlier row, and that mechanism is what every verification to date has relied on. A proof would have to show that such blocks of entries in $\{0,2\}$ always appear early enough, which is a statement about the density of small prime gaps in disguise.

Formalizing it. Nothing here is currently formalized: Mathlib has the prime enumeration $n \mapsto p_n$ (Nat.nth Nat.Prime) and the basic facts about it, but not the iterated-difference triangle nor any of its properties. This mission contributes the definition of the triangle, the structural facts about its rows, and a machine-checked version of the reduction step that all computational work on the problem uses. The goal theorem itself is open — the milestones are known mathematics, and each is provable with current tools, while the goal is not.

Difficulty

The obvious attack is induction on the row index: to see that $d^{k+1}(0) = 1$ it suffices to know that $d^{k}(0) = 1$ and $d^{k}(1) \in \{0,2\}$. But controlling $d^{k}(1)$ requires controlling $d^{k-1}(1)$ and $d^{k-1}(2)$, and so on: the invariant that closes is not "the row begins with $1$" but "the row begins with $1$ and its next $m$ entries lie in $\{0,2\}$", and each application of the difference operator consumes one entry of that block. So a finite block of good entries only carries the conclusion a finite number of rows further down, and the conjecture needs such blocks to keep reappearing forever, arbitrarily far down the triangle. Nothing is known that produces them.

A second warning, due to Hallard Croft: the property is not specific to the primes. Sequences that start with $2$, continue with odd numbers, and have gaps that are not too large empirically exhibit the same behaviour, so any proof that uses only such coarse features would prove a much more general statement — and conversely, an argument exploiting deep properties of primes is likely to be proving the wrong thing.

Formalization scope

Rows are total functions $\mathbb{N} \to \mathbb{N}$, defined for every index, and the whole triangle is a single family indexed by the row number. Differences are taken as Int.natAbs of a difference computed in $\mathbb{Z}$, so truncated natural subtraction never occurs; the one place where $\mathbb{N}$-subtraction does appear is the milestone identifying row $1$ with the gap sequence, where the subtraction is justified by monotonicity of $n \mapsto p_n$.

Primes are indexed from $0$ via Mathlib's Nat.nth Nat.Prime, so $p_0 = 2$; rows are indexed with row $0$ the primes, and the goal quantifies over all $k \ge 1$ in the form d (k + 1) 0 = 1, with no upper bound and no extra hypothesis, so no vacuous or finitely-truncated reading of the goal is available. The general difference operator is stated for arbitrary sequences $\mathbb{N} \to \mathbb{N}$, which is what makes the propagation lemma usable as a black box, and reusable beyond this mission.

A complete development needs no analytic input for the milestones: Mathlib's Nat.nth, Nat.prime_nth_prime, Nat.nth_prime_zero_eq_two and the strict monotonicity of the prime enumeration suffice. Contributions that would extend the mission beyond its current list: a formal version of a concrete computational verification (checking that the leading entries of the first $N$ rows are $1$ for an $N$ well beyond the hand-checkable range), and formalizations of the general statement for non-prime sequences of the Croft type.

Selected references

• N. L. Gilbreath, as reported in R. B. Killgrove and K. E. Ralston, On a conjecture concerning the primes, Mathematical Tables and Other Aids to Computation 13 (1959), 121–122. https://doi.org/10.1090/S0025-5718-1959-0105398-3
• A. M. Odlyzko, Iterated absolute values of differences of consecutive primes, Mathematics of Computation 61 (1993), 373–380. https://doi.org/10.1090/S0025-5718-1993-1192979-9
• Gilbreath's conjecture, Wikipedia. https://en.wikipedia.org/wiki/Gilbreath%27s_conjecture

Motivation

Galois theory attaches to every finite Galois extension $L/K$ a finite group $\mathrm{Gal}(L/K)$, the group of field automorphisms of $L$ fixing $K$ pointwise, and the fundamental theorem of Galois theory turns the subfield structure of $L/K$ into the subgroup structure of that group. The inverse Galois problem asks whether this correspondence is surjective over the rationals: given an arbitrary finite group $G$, is there a Galois extension $L/\mathbb{Q}$ with $\mathrm{Gal}(L/\mathbb{Q}) \cong G$? The question was posed in the early nineteenth century and is unsolved.

What makes it a live research question rather than a curiosity is that the known positive results come from genuinely different sources, and none of them covers all finite groups.

• Cyclic and, more generally, finite abelian groups are realizable over $\mathbb{Q}$ by an explicit cyclotomic construction resting on Dirichlet's theorem on primes in arithmetic progressions.
• Symmetric and alternating groups are realizable over $\mathbb{Q}$; this is due to Hilbert, who realized them first over the rational function field $\mathbb{Q}(t)$ and then specialized $t$ using his irreducibility theorem.
• Every finite solvable group is realizable over $\mathbb{Q}$; this is Shafarevich's theorem (I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219), obtained by solving embedding problems.
• Over $\mathbb{C}(t)$ — and over $K(t)$ for any algebraically closed $K$ of characteristic zero — every finite group is realizable, by the Riemann existence theorem. The obstruction to the goal is not the group theory; it is descending the field of constants to $\mathbb{Q}$.
• Case-by-case work covers large finite lists: all transitive permutation groups of degree at most $23$, and every sporadic simple group, are known to be realizable over $\mathbb{Q}$.

Setting

Fix a field $K$ and a group $G$. A Galois realization of $G$ over $K$ is a field $L$ equipped with a $K$-algebra structure such that the extension $L/K$ is Galois — normal and separable — together with a group isomorphism

$$G \;\cong\; \mathrm{Gal}(L/K),$$

where $\mathrm{Gal}(L/K)$ denotes the group of $K$-algebra automorphisms of $L$ under composition. The group $G$ is realizable over $K$, written IsRealizable K G, when at least one Galois realization of $G$ over $K$ exists. No finiteness of $L/K$ is imposed in the definition; it is automatic once $G$ is finite, because an infinite Galois extension has infinite automorphism group.

Two base fields beyond $\mathbb{Q}$ appear throughout. $K(t)$ denotes the field of rational functions in one variable over $K$, written RatFunc K; and for the statement that a group is realizable over some number field, the base field ranges over the intermediate fields of $\mathbb{C}/\mathbb{Q}$.

Formalization targets

Goal — the inverse Galois problem

$$\text{for every finite group } G, \qquad \exists\, L/\mathbb{Q} \text{ Galois with } \mathrm{Gal}(L/\mathbb{Q}) \cong G.$$

The goal fixes no degree, no polynomial and no construction: it asserts only the shape of the truth, so no later refinement of the known constructions can invalidate it.

Milestones — the known partial results

$$G \text{ cyclic} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, \qquad G \text{ abelian} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\mathrm{Sym}(S),\; A_n \text{ realizable over } \mathbb{Q}, \qquad G \text{ solvable} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\exists\, K,\ \mathbb{Q} \subseteq K \subseteq \mathbb{C},\ G \text{ realizable over } K,$$ $$G \text{ realizable over } \mathbb{C}(t), \qquad G \text{ realizable over } K(t) \ (K \text{ algebraically closed, char } 0),$$ $$G \text{ realizable over } \mathbb{Q}(t) \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}.$$

The last milestone is the Hilbert-irreducibility descent step; together with the geometric milestones it makes precise which half of the classical programme is missing.

Significance

The result itself would settle a two-century-old question and, with it, the surjectivity of the Galois correspondence over $\mathbb{Q}$: every abstract finite group would be known to arise from an explicit arithmetic object, a polynomial with rational coefficients. Its absence is felt in practice — constructing a single new Galois group over $\mathbb{Q}$ is publishable work, as the recent additions of the degree-$17$ group $17T7$ (van Bommel–Costa–Elkies–Keller–Schiavone–Voight, 2024) and of the Mathieu group $M_{23}$ show.

Formalizing it produces something available today independently of the goal: a machine-checked library of the known realizability results. Mathlib has the fundamental theorem of Galois theory, cyclotomic extensions, the Kronecker–Weber theorem, solvability of groups and symmetric/alternating group theory, but it does not have a predicate for "$G$ is a Galois group over $K$", nor any of the milestones above. Every milestone here is a proved theorem of classical number theory and an unformalized one; the cyclic and abelian cases are within reach of current Mathlib, while the Shafarevich and Riemann-existence milestones are substantial formalization projects in their own right.

Difficulty

The obvious strategy fails at a well-understood point. Over $\mathbb{C}(t)$ the problem is solved: by the Riemann existence theorem every finite group occurs as the deck-transformation group of a branched cover of the projective line. Hilbert's irreducibility theorem then descends realizability from $\mathbb{Q}(t)$ to $\mathbb{Q}$. What is missing is the step in between: producing the cover over $\mathbb{Q}$ rather than over $\mathbb{C}$, i.e. showing that the geometric solution can be chosen with rational field of constants. The rigidity method makes this work for many groups, but there is no known argument covering all of them; an approach that only produces realizability over some number field is not enough, and that weaker statement is included as a milestone precisely to mark the line.

A second, purely formal difficulty: the milestones are classical but their published proofs are long. Shafarevich's theorem rests on a delicate analysis of embedding problems, and the Riemann existence theorem is analytic input that Mathlib does not currently have in the required form.

Formalization scope

The mission fixes one definition file, published first, carrying the structure GaloisRealization and the one-field class IsRealizable. Conventions it commits to:

• IsGalois K L is Mathlib's Galois condition (normal and separable); finiteness of the extension is not assumed.
• The isomorphism is with the full automorphism group $L \simeq_{\mathrm{alg}[K]} L$, not with a quotient or a subgroup of it.
• The carrier $L$ of a realization is required to live in the same universe as $K$. This costs no generality for the statements of the mission — for finite $G$ a realization is a finite extension of $K$ — and keeps every statement universe-monomorphic.
• $\mathrm{Sym}(S)$ is Equiv.Perm S for a finite type $S$, and $A_n$ is alternatingGroup (Fin n); degenerate small cases are included rather than excluded.
• Solvability is Group.IsSolvable.

The statements cannot be satisfied vacuously: IsRealizable K G asserts the existence of data, so a solver must exhibit an extension; and the hypotheses of the milestones (cyclic, abelian, solvable, or none at all) are all satisfiable, so no milestone is empty. The one conditional milestone, Hilbert descent, is stated with realizability over $\mathbb{Q}(t)$ as an explicit hypothesis.

Infrastructure a complete development needs, most of it reusable well beyond this mission: transport of a Galois realization along an isomorphism of groups and along an isomorphism of base fields; the fixed-field construction and the fundamental theorem in the form "$\mathrm{Gal}(L/L^H) \cong H$"; Galois groups of cyclotomic fields; Dirichlet's theorem on primes in arithmetic progressions (already in Mathlib); Hilbert's irreducibility theorem (not in Mathlib). Contributions of any of these as reusable platform definitions or lemmas are welcome, as are decompositions of the harder milestones into sketches.

Selected references

• Inverse Galois problem, Wikipedia. https://en.wikipedia.org/wiki/Inverse_Galois_problem
• I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219.
• C. U. Jensen, A. Ledet, N. Yui, Generic Polynomials: Constructive Aspects of the Inverse Galois Problem, MSRI Publications 45, Cambridge University Press, 2002. http://library.msri.org/books/Book45/files/book45.pdf
• G. Malle, B. H. Matzat, Inverse Galois Theory, Springer Monographs in Mathematics, 1999.
• R. van Bommel, E. Costa, N. D. Elkies, T. Keller, S. Schiavone, J. Voight, 17T7 is a Galois group over the rationals, arXiv:2411.07857, 2024. https://arxiv.org/abs/2411.07857

Motivation

The Riemann hypothesis concerns the zeros of a complex analytic function, yet it admits an equivalent formulation involving only positive integers, finite sums, the real exponential, and the natural logarithm. Jeffrey C. Lagarias established this formulation in An Elementary Problem Equivalent to the Riemann Hypothesis (Theorem 1.1). It connects the distribution of divisors of an integer with the analytic behavior of the zeta function. For number theorists and formalizers, the interest lies in making that connection precise without confusing an elementary statement with an elementary proof.

The objective is the known equivalence selected by LeanEval v1, not a resolution of RH. Lagarias's paper builds on results of Guy Robin concerning large values of the divisor-sum function; those results remain substantial parts of the formalization workload (Lagarias, §3).

Setting

For a positive integer $n$, its divisor sum is

$$\sigma(n)=\sum_{d\mid n}d,$$

where the sum runs over positive divisors, including $1$ and $n$. Its harmonic number is

$$H_n=\sum_{j=1}^{n}\frac1j.$$

All inequalities below are inequalities of real numbers. The symbols $\exp$ and $\log$ denote the real exponential and natural logarithm. The Euler–Mascheroni constant is $\gamma=\lim_{n\to\infty}(H_n-\log n)$.

The Riemann zeta function is obtained by analytic continuation of $\sum_{m=1}^{\infty}m^{-s}$ from $\operatorname{Re}(s)>1$. RH asserts that its nontrivial zeros have real part $1/2$. The Lagarias elementary criterion in this mission is the assertion that $\sigma(n)\le H_n+\exp(H_n)\log(H_n)$ for every positive integer $n$. These conventions agree with the arithmetic quantities in Lagarias, Problem E, with the precise equality-clause distinction stated below.

Formalization targets

Main goal: the exact LeanEval equivalence

$$\mathrm{RH}\quad\Longleftrightarrow\quad \forall n\in\mathbb N,\;n>0\Longrightarrow \sigma(n)\le H_n+\exp(H_n)\log(H_n).$$

There are no hypotheses on the goal theorem. The quantifier ranges over all positive integers, not a bounded test set or an unspecified tail. The benchmark uses a non-strict inequality and does not include an equality characterization. Lagarias's Problem E additionally requires equality only at $n=1$; the proof of the reverse implication in Theorem 1.1, p. 8 uses the non-strict inequality alone. The stronger source formulation is therefore not silently substituted for the benchmark.

Supporting targets from the paper

The milestone list records the following source statements, with their thresholds unchanged:

• Lemma 3.1: for $n\ge3$,

$$e^\gamma n\log\log n\le\exp(H_n)\log(H_n).$$

• Lemma 3.2: for $n\ge20$,

$$H_n+\exp(H_n)\log(H_n)\le e^\gamma n\log\log n+\frac{7n}{\log n}.$$

• The finite check in the proof of Theorem 1.1: the criterion holds for $1\le n\le5040$, with equality exactly at $n=1$.
• Proposition 3.1, attributed to Robin: assuming RH, for $n\ge5041$,

$$\sigma(n)\le e^\gamma n\log\log n.$$

• Proposition 3.2, attributed to Robin: if RH is false, some fixed $0<\beta<1/2$ and $C>0$ satisfy

$$\sigma(n)\ge e^\gamma n\log\log n+ \frac{Cn\log\log n}{(\log n)^\beta}$$

for arbitrarily large integers $n$.

All five are taken from Lagarias, §3, pp. 6–8; the finite check is explicitly an unnumbered step, not a newly attributed lemma.

Significance

The result identifies an exact arithmetic reformulation of RH. It does not make either side unconditional. A proof of the equivalence gives a bridge between statements in different mathematical languages; it does not certify the universal inequality merely because many instances can be checked. This distinction is central to the interpretation of Lagarias's theorem.

The formalization would connect existing Mathlib definitions of the zeta function, divisor sums, harmonic numbers, and Euler's constant through a machine-checked argument. Reusable outputs include explicit harmonic/exponential comparisons, certified finite real inequalities, and formal versions of Robin's conditional and oscillation results. The mathematical results are known; this proposal supplies open formalization targets, not completed proofs. No accepted LeanEval result is claimed by creating or launching the mission.

Difficulty

The elementary appearance of the criterion hides its main analytic requirements. Bounding the divisor sum crudely, or checking any finite number of integers, cannot establish the universal equivalence. The conditional upper bound and especially the quantitative oscillation theorem connect zeta zeros with unusually large divisor sums. They must be proved, not packaged as definitions or presumed available because the paper cites them (Lagarias, Propositions 3.1–3.2).

The oscillation statement requires uniform positive constants and arbitrarily large indices. Replacing it with one counterexample loses essential information. The bounded computation also requires rigorous control of exponential and logarithmic values: an ordinary floating-point loop is not a Lean proof. Beyond the listed milestones, completion still requires standard growth comparisons, threshold bookkeeping, and assembly of the two implications. The short length of the source's final argument should not be read as an estimate of total formalization effort.

Formalization scope

The goal is LeanEval.NumberTheory.riemann_hypothesis_iff_lagarias_elementary_criterion, with type RiemannHypothesis ↔ LagariasElementaryCriterion. The criterion definition is copied from the benchmark. σ 1 n is natural-valued and cast to the reals; harmonic n is rational-valued and cast to the reals. RH remains Mathlib's predicate on riemannZeta, excluding negative even trivial zeros and the point $s=1$. No replacement axiom, hidden RH assumption, altered zeta function, or circular child restatement is permitted.

The goal excludes $n=0$ and includes $n=1$. Thresholds ensure positive logarithm arguments in the analytic milestones. The oscillation milestone expresses an infinite subset of the naturals as an unbounded set, retaining $n\ge3$; deletion of the finitely many smaller indices does not change the source's infinitude claim. Its real exponent is represented by Real.rpow, not natural exponentiation. Constants are chosen before the arbitrary cutoff.

The benchmark pins Lean 4.33.0 and Mathlib 6f1ef4e5dd604a435bddba4747b13970cd65d2a1. The proposal targets Prove2me's supported Lean 4.33.1 environment, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. These environments are distinct; eventual benchmark credit requires the benchmark's own validation. Contributions to analytic infrastructure, source-faithful supporting results, and certified finite inequalities are welcome. The five milestones are an initial source-backed structure, not a claim that all required infrastructure is already present.

Selected references

• Jeffrey C. Lagarias, An Elementary Problem Equivalent to the Riemann Hypothesis, American Mathematical Monthly 109 (2002), 534–543. arXiv:math/0008177v2, posted 6 May 2001. The theorem, proposition, equation, and page numbers in this proposal refer to this nine-page arXiv version.
• Guy Robin, Grandes valeurs de la fonction somme des diviseurs et hypothèse de Riemann, Journal de Mathématiques Pures et Appliquées 63 (1984), 187–213. Bibliography entry [18] in Lagarias. The milestone formulations are those explicitly reproduced and attributed in Lagarias's Propositions 3.1 and 3.2.

Motivation

In the last of the twenty-four questions that closed his 1982 survey Three-dimensional manifolds, Kleinian groups and hyperbolic geometry (Bull. Amer. Math. Soc. 6 (1982), 357–381), Thurston asked to "show that volumes of hyperbolic $3$-manifolds are not all rationally related" (p. 380). Twenty-two of the twenty-four have since been answered — geometrization by Perelman, tameness by Agol and by Calegari–Gabai, the ending lamination conjecture by Brock–Canary–Minsky, virtual fibering by Agol — and this one is among the two that remain open.

Some rational relations are forced, and for a trivial reason: a degree $n$ cover of a hyperbolic $3$-manifold has $n$ times its volume, so any two commensurable manifolds have rationally related volumes. The question, which remains open, is whether every rational relation arises that way — equivalently, whether some two hyperbolic $3$-manifolds have irrational volume ratio. Remarkably, not a single such pair is known.

Setting

The bundle fixes the meaning of every term. Hyperbolic $3$-space is the upper half-space $\{(x,y,z) : z > 0\}$. Its volume is Lebesgue measure with density $z^{-3}$ — the Riemannian volume of the metric $(dx^2+dy^2+dz^2)/z^2$ written out, so that no Riemannian machinery is required. The hyperbolic distance is given by its closed formula

$$\cosh d(p,q) \;=\; 1 + \frac{|p-q|^2}{2\,p_3\,q_3}.$$

A Kleinian action is a free, properly discontinuous action by hyperbolic isometries; the quotient is a complete hyperbolic $3$-manifold, discreteness and torsion freeness being consequences rather than hypotheses. The volume of the quotient is the measure of a fundamental domain, in the sense of Mathlib's MeasureTheory.IsFundamentalDomain, and the set of volumes collects those that are finite and positive.

Two conventions are stated rather than derived, and are worth flagging. Isometries are not required to preserve orientation, so the set of volumes also contains those of non-orientable quotients; this enlarges the set but not its $\mathbb{Q}$-span, so neither goal is affected. And preservation of the hyperbolic volume is a field of the structure rather than a consequence of preserving the distance: it holds for every hyperbolic isometry, but deriving it amounts to classifying $\mathrm{Isom}(\mathbb{H}^3)$, which is not the subject of this mission.

Formalization targets

The goal is that the volumes are not all rationally related: there are two of them, $v$ and $w$, with $v \neq q w$ for every rational $q$.

Two milestones support it. The first is that passing to a subgroup of index $n$ multiplies the volume by $n$, a fundamental domain for the subgroup being the union of $n$ translates of one for the whole group; this is the source of every known rational relation, and it is why the question is phrased as it is. The second is that the set of volumes is nonempty — that some finite-volume hyperbolic $3$-manifold exists at all — without which the goal would be vacuously false rather than open.

A stronger form of the question, that the $\mathbb{Q}$-span of the set of volumes is infinite dimensional, is also stated.

Significance

The question is a geometric statement whose difficulty is arithmetic. For the Bianchi groups of an imaginary quadratic field $F$, Humbert's formula gives the covolume as $|\delta_F|^{3/2}\zeta_F(2)/4\pi^2$, so the ratio of two such volumes is, up to explicit algebraic factors, a ratio of Dedekind zeta values at $2$; and Neumann and Yang showed that the Bloch invariant of a hyperbolic $3$-manifold lies in a subgroup of finite $\mathbb{Q}$-rank determined by its invariant trace field, so that manifolds sharing an invariant trace field with a single complex place, such as an imaginary quadratic one, have rationally related volumes. Producing one irrational ratio therefore means separating two such transcendentals — a statement of the same order of difficulty as the irrationality of $\zeta(5)$. The value of formalizing the question is not that it will be closed, but that its statement, and the elementary relations that make its naive form false, are pinned down exactly.

Motivation

The joint replenishment problem (JRP) is one of the basic models of multi-item inventory control. Each item follows the economic order quantity (EOQ) model of Harris (1913): ordering costs a fixed amount, holding stock costs a rate proportional to the stock, and the classical trade-off between the two determines how often to reorder. In a JRP, items replenished together share part of the fixed cost, so the reorder cycles of the items should be coordinated. The problem has been studied for decades, with a large literature of heuristics and approximation algorithms (see the survey of Khouja and Goyal 2008; Porras and Dekker 2008 compare the two ways of charging joint costs), yet its exact complexity remained unclear even for very few items.

Schulz and Telha (arXiv:2007.09045, 2020; Operations Research, 2024) give a striking answer for the smallest non-trivial case, two items. They show that solving the two-item problem exactly is at least as hard as integer factorization (their Theorem 1), and, assuming the Riemann hypothesis, that the two-item periodic JRP is NP-hard under randomized reductions (Theorem 2). This mission formalizes the mathematical core of Theorem 1(a), for the aperiodic JRP: the paper's Lemma 1.

Timeline. The complexity of both JRP variants was open for a long time. Schulz and Telha announced the reduction from integer factorization to the two-item aperiodic JRP (Theorem 1(a)) in 2011. Cohen-Hillel and Yedidsion (2018) then proved that the aperiodic JRP with an arbitrary number of items is strongly NP-hard (they call it the periodic JRP). The 2020 preprint adds the reduction for the two-item periodic JRP (Theorem 1(b)) and, under the Riemann hypothesis, a randomized reduction from Partition to it (Theorem 2).

Setting

For an item with fixed ordering cost $K$ and holding cost rate $H$, replenished every $q$ time units, the long-run cost per unit time is

$$\mathrm{EOQ}_{K,H}(q) = \frac{K}{q} + Hq .$$

Reorder cycles are positive integers $q \in \mathbb Z^+$. In the aperiodic two-item JRP (objective (1) of the paper) items 1 and 2 have data $(K_1,H_1)$ and $(K_2,H_2)$, and every joint replenishment earns a discount $K_0 \le K_1, K_2$. With cycles $q_1, q_2$, joint replenishments happen every $\mathrm{lcm}(q_1,q_2)$ time units, so the discount per unit time is $\mathrm{DC}(q_1,q_2;K_0) = K_0/\mathrm{lcm}(q_1,q_2)$ and the problem is

$$\min\left\{\mathrm{JRP}(q_1,q_2) = \mathrm{EOQ}_{K_1,H_1}(q_1) + \mathrm{EOQ}_{K_2,H_2}(q_2) - \frac{K_0}{\mathrm{lcm}(q_1,q_2)} \ :\ q_1,q_2 \in \mathbb Z^+\right\}.$$

For an integer $M$, the instance of Lemma 1 has

$$K_1 = K_0 = M(M-1),\qquad H_1 = 4,\qquad K_2 = M^3(M^2-1),\qquad H_2 = M(M^2-1).$$

Item 2's own EOQ optimum is $q_2 = M$. Fixing $q_2 = M$ leaves the one-variable problem (2) with objective

$$\mathrm{JRP}^{\mathrm{red}}(q_1) = M(M-1)\left(\frac{1}{q_1} - \frac{1}{\mathrm{lcm}(q_1,M)}\right) + 4q_1 .$$

In Lean these are eoq, aperiodicCost, lemma1Cost, eoq2 (item 2's cost) and jrpRed, and an optimal solution (IsOptimal) is a pair of positive integers whose value is no larger than that of any other pair of positive integers.

Formalization targets

Goal: Lemma 1

For every odd composite number $M$, the instance above satisfies $K_0 \le K_1$, $K_0 \le K_2$, has all coefficients at most $M^5$, has an optimal solution, and

$$\text{every optimal } (q_1,q_2) \text{ satisfies } \quad q_2 = M \quad\text{and}\quad 1 < \gcd(q_1,M) < M .$$

So $\gcd(q_1, M)$ is a non-trivial divisor of $M$.

Milestones (the steps of the paper's proof, pp. 9–10)

1. $\mathrm{EOQ}_{K_2,H_2}(M\pm1) = \mathrm{EOQ}_{K_2,H_2}(M) + H_2/(M\pm1) \ge \mathrm{EOQ}_{K_2,H_2}(M) + K_0$.
2. For $q_2 \ne M$: $\mathrm{JRP}(q_1,q_2) \ge \mathrm{EOQ}_{K_2,H_2}(M) + K_0 + 4 > \mathrm{JRP}(1,M)$.
3. $\mathrm{JRP}(q_1, M) = \mathrm{EOQ}_{K_2,H_2}(M) + \mathrm{JRP}^{\mathrm{red}}(q_1)$.
4. For $q_1$ coprime with $M$: $\mathrm{JRP}^{\mathrm{red}}(q_1) \ge 4(M-1)$.
5. For a divisor $p$ of $M$ with $3 \le p < M$ and a multiple $q$ of $p$: $\mathrm{JRP}^{\mathrm{red}}(q) \le (M-1)(M-p)/q + 4q$.
6. Some multiple $q$ of $p$ in $\left[\frac{M-1}{2} - \frac{p-1}{2}, \frac{M-1}{2} + \frac{p-1}{2}\right]$ has $\mathrm{JRP}^{\mathrm{red}}(q) < 4(M-1)$.
7. Multiples $q_1$ of $M$ have $\mathrm{JRP}^{\mathrm{red}}(q_1) = 4q_1 \ge 4M$, while $\mathrm{JRP}^{\mathrm{red}}((M-1)/2) \le 4(M-1)$.

Significance

The result. Lemma 1 turns any exact algorithm for the two-item aperiodic JRP into a factoring algorithm: solve the instance, read off $\gcd(q_1, M)$, and recurse on the two factors. Since the instance's coefficients have size $O(\log M)$, a polynomial-time JRP algorithm would factor integers in polynomial time (Theorem 1(a)). This explains, in a precise sense, why the many exact and approximation methods for the JRP never produced a provably polynomial exact algorithm even for two items, and why the problem's difficulty is number-theoretic rather than combinatorial.

Formalizing it. The lemma has a complete, elementary proof in the paper; it has not been machine-checked. The formalization pins down every quantifier the prose leaves loose: that optimal solutions exist, that the claim is about every optimum, which coefficients are used, and that periods range over positive integers only. The proof steps (the item-2 pin, the coprime bound, the interval argument) are stated as separate milestones so they can be checked individually.

Difficulty

Each step is elementary, but the argument mixes discrete and continuous reasoning. The objective is not convex in $q_1$: the term $-K_0/\mathrm{lcm}(q_1,M)$ jumps down at every period sharing a factor with $M$. The obvious approach, comparing against the continuous EOQ minimizer, gives the right threshold $4(M-1)$ for coprime periods but says nothing about where a cheaper non-coprime period sits. The interval step needs the exact size of a window of integers around $(M-1)/2$, that $p$ consecutive integers contain a multiple of $p$, and a strict inequality between a quadratic's roots and that window. The existence of an optimum is not stated in the paper and needs a coercivity argument over $\mathbb Z^+ \times \mathbb Z^+$.

Formalization scope

This mission formalizes the correctness of the reduction behind Theorem 1(a); polynomial running time is not formalized, and neither are Theorem 1 as a statement about algorithms, the recursion to a full factorization, nor primality testing.

Conventions: periods are natural numbers, and every quantification over a period requires it to be positive, because Lean evaluates $K/0 = 0$, $\mathrm{lcm}(0,M) = 0$ and $\gcd(0,M) = M$. Costs are real numbers. Coefficients are natural numbers cast to $\mathbb R$. "Odd composite" is Odd M ∧ 1 < M ∧ ¬ M.Prime. "Size at most $5\log M$" is stated as "every coefficient is at most $M^5$", equivalent in any logarithm base.

Two additions relative to the printed statement are disclosed in the goal's Formalization Note. The goal states the explicit instance of the proof (p. 9) rather than "there is an instance", since an existential instance could be chosen to make the claim easy and loses the polynomial-size construction the reduction needs. The goal also asserts that an optimal solution exists, so that "every optimal solution satisfies …" is not vacuously true. Neither periods equal to zero nor junk values of division can satisfy the optimality predicate.

All objects are defined in one file, JRPHard.Aperiodic.Setting; nothing beyond Mathlib's Nat.gcd, Nat.lcm, Nat.Prime and real arithmetic is needed. Proofs of any milestone, or alternative proofs of the goal, are welcome.

Selected references

• A. S. Schulz and C. Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, 2020; published as Integer Factorization: Why Two-Item Joint Replenishment Is Hard, Operations Research, 2024. https://arxiv.org/abs/2007.09045
• F. W. Harris, How many parts to make at once, Factory, The Magazine of Management 10(2), 1913; reprinted in Operations Research 38(6), 1990. https://doi.org/10.1287/opre.38.6.947
• E. Porras and R. Dekker, A solution method for the joint replenishment problem with correction factor, International Journal of Production Economics 113(2), 834–851, 2008. https://doi.org/10.1016/j.ijpe.2007.11.008
• M. Khouja and S. Goyal, A review of the joint replenishment problem literature: 1989–2005, European Journal of Operational Research 186(1), 2008. https://doi.org/10.1016/j.ejor.2007.03.007
• M. Cohen-Hillel and L. Yedidsion, The periodic joint replenishment problem is strongly NP-hard, Mathematics of Operations Research 43(4), 2018. https://doi.org/10.1287/moor.2017.0904

Motivation

Counting solutions of polynomial equations over finite fields is one of the oldest themes of number theory, going back to Gauss's count of points on $x^3 + 1 = y^3$ modulo a prime. In 1949 André Weil proposed a precise description of how these counts behave when the field is enlarged: for a smooth projective variety over $\mathbb F_q$, the generating function of its point counts — the zeta function — should be a rational function with integer polynomial factors, satisfy a functional equation, and have its zeros on prescribed "critical lines", in exact analogy with the Riemann hypothesis. These Weil conjectures organized several decades of work in algebraic geometry and directly motivated the construction of étale cohomology.

Timeline (as recorded in the source article, Wikipedia: Weil conjectures):

• 1924 — Artin conjectures the statements for curves.
• 1930s — Hasse proves the case of elliptic curves: $\#E(\mathbb F_{q^m}) = 1 - \alpha^m - \beta^m + q^m$ with $|\alpha| = |\beta| = \sqrt q$.
• 1948–49 — Weil proves the conjectures for curves and formulates them in all dimensions (Weil 1949).
• 1960 — Dwork proves rationality by $p$-adic methods (Dwork 1960).
• 1965 — Grothendieck, with M. Artin and Verdier, proves rationality, the functional equation and the Betti-number statement via the Lefschetz trace formula in $\ell$-adic cohomology.
• 1974 — Deligne proves the Riemann hypothesis part (Deligne 1974); in 1980 he proves a generalization for pushforwards of sheaves (Deligne 1980).

Setting

Let $k = \mathbb F_q$ be a finite field with $q$ elements and characteristic $p$. Let $X$ be a smooth projective variety of dimension $n$ over $k$: a scheme $X$ with a structure morphism $f : X \to \operatorname{Spec} k$ that is smooth of relative dimension $n$, geometrically irreducible, and admits a closed immersion into some projective space $\mathbb P^N_k$ over $k$.

For $m \ge 1$ let $\mathbb F_{q^m}$ be the extension of $k$ of degree $m$, and let

$$N_m = \#X(\mathbb F_{q^m})$$

be the number of $k$-morphisms $\operatorname{Spec}\mathbb F_{q^m} \to X$. The zeta function of $X$ is the formal power series

$$Z(X,T) = \exp\Big(\sum_{m\ge1} \frac{N_m}{m} T^m\Big) \in \mathbb Q[[T]],$$

so that $\zeta(X,s) = Z(X, q^{-s})$.

Formalization targets

Goal: the Weil conjectures (parts 1–3)

There exist integer polynomials $P_0, \dots, P_{2n}$ and multisets of nonzero complex numbers $\{\alpha_{ij}\}_j$ such that

1. Rationality.

$$Z(X,T) = \frac{P_1(T)\,P_3(T)\cdots P_{2n-1}(T)}{P_0(T)\,P_2(T)\cdots P_{2n}(T)},$$

with $P_0(T) = 1-T$, $P_{2n}(T) = 1 - q^nT$, and $P_i(T) = \prod_j (1-\alpha_{ij}T)$ over $\mathbb C$ for $1 \le i \le 2n-1$. 2. Functional equation.

$$Z\big(X, q^{-n}T^{-1}\big) = \pm\, q^{nE/2}\, T^{E}\, Z(X,T),$$

where $E = \sum_i (-1)^i \deg P_i$ is the Euler characteristic; moreover $\{\alpha_{2n-i,j}\}_j = \{q^n/\alpha_{i,j}\}_j$ as multisets. 3. Riemann hypothesis. $|\alpha_{ij}| = q^{i/2}$ for all $1 \le i \le 2n-1$ and all $j$.

Milestones

The historical partial results (Weil's theorem for curves; Dwork's rationality; Grothendieck's rationality and functional equation; Deligne's Riemann hypothesis) and the worked examples of the source (projective line, projective space, elliptic curves, the genus-2 curve $y^2 + y = x^5$ over $\mathbb F_{41}$ and the Weil polynomials of its Jacobian).

Significance

The Weil conjectures give sharp estimates $|N_m - q^{nm} - \cdots| = O(q^{m(2n-1)/2})$ for point counts, and through them bounds on exponential sums (Kloosterman sums, character sums), the Ramanujan–Petersson conjecture for holomorphic modular forms (Deligne 1971), and the hard Lefschetz theorem over finite fields. They are a standard input in analytic number theory, coding theory and cryptography.

All four statements have been proved since 1974. None of them has a machine-checked proof in Lean/Mathlib at present; Mathlib does not yet contain étale cohomology, Jacobians of curves, or the Hasse bound for elliptic curves over finite fields. This mission records faithful, compiling statements so that partial formalizations — the elementary examples, Hasse's theorem, Weil's theorem for curves via Riemann–Roch or Stepanov–Bombieri, Dwork's $p$-adic rationality proof, and eventually the cohomological proofs — can be attached to a common target.

Difficulty

The examples with a cell decomposition (projective spaces, Grassmannians) reduce to counting points in affine spaces. Beyond them, even rationality is a theorem of substance: there is no elementary formula for $N_m$, and the counts must be shown to satisfy a linear recurrence. The functional equation and the precise shape of the $P_i$ require a cohomology theory with Poincaré duality and a Lefschetz trace formula; the Riemann hypothesis requires, in addition, control of the absolute values of Frobenius eigenvalues, which in Deligne's proof uses Lefschetz pencils, monodromy and the "tensor power trick". For curves, Riemann–Roch and the Hasse–Weil bound (or Stepanov–Bombieri) suffice, but these too are absent from Mathlib.

Formalization scope

• The finite field is any k : Type with [Field k] [Finite k] [CharP k p], p prime; q = Nat.card k. Schemes live in Scheme.{0}.
• $\mathbb P^N_k$ is Proj of $k[x_0,\dots,x_N]$ graded by total degree; "projective" means a closed immersion into some $\mathbb P^N_k$ commuting with the structure maps. "Non-singular of dimension $n$" is SmoothOfRelativeDimension n f; "variety" is GeometricallyIrreducible f.
• $N_m$ counts $k$-morphisms $\operatorname{Spec} \mathbb F_{q^m} \to X$ with $\mathbb F_{q^m}$ = FiniteField.Extension k p m; $Z(X,T)$ is PowerSeries.subst of $\sum_{m\ge1} N_m T^m/m$ into PowerSeries.exp ℚ.
• Rationality is stated as an identity of power series after clearing denominators; the functional equation is stated pointwise for complex $t \neq 0$ away from the poles of both sides; $q^{nE/2}$ is a real power.
• The Euler characteristic $E$ is encoded as $\sum_i (-1)^i \deg P_i$ (the alternating sum of the Betti numbers), since Mathlib has no étale cohomology from which to define it independently.
• Part 4 (Betti numbers of a lift to characteristic zero) is not formalized: stating it requires the complex-analytic space of a variety over a number field and its singular cohomology, which Mathlib does not provide.
• The $\alpha_{ij}$ are required to be nonzero, which excludes junk factors $1 - 0\cdot T$ and junk values of $q^n/0$.

Contributions welcome: the zeta function of projective space, Hasse's theorem, point counts and Weil polynomials for the $\mathbb F_{41}$ examples, rationality for curves, and general infrastructure (Riemann–Roch for curves, Jacobians, étale cohomology).

Selected references

• Wikipedia, Weil conjectures. https://en.wikipedia.org/wiki/Weil_conjectures
• A. Weil, Numbers of solutions of equations in finite fields, Bull. Amer. Math. Soc. 55 (1949), 497–508. https://doi.org/10.1090/S0002-9904-1949-09219-4
• B. Dwork, On the rationality of the zeta function of an algebraic variety, Amer. J. Math. 82 (1960), 631–648. https://doi.org/10.2307/2372974
• P. Deligne, La conjecture de Weil. I, Publ. Math. IHÉS 43 (1974), 273–307. https://doi.org/10.1007/BF02684373
• P. Deligne, La conjecture de Weil. II, Publ. Math. IHÉS 52 (1980), 137–252. https://doi.org/10.1007/BF02684780

Motivation

The Fourier coefficients of modular forms are among the most studied arithmetic functions in number theory. In 1916 Srinivasa Ramanujan studied the coefficients $\tau(n)$ of the discriminant modular form $\Delta$ and conjectured three properties: multiplicativity, a three-term recursion on prime powers, and the bound $|\tau(p)|\le 2p^{11/2}$ for primes $p$ (Ramanujan 1916). Hans Petersson extended the size bound to the coefficients of holomorphic cusp forms for congruence subgroups (Petersson 1930). The resulting Ramanujan–Petersson conjecture for holomorphic cusp forms is now a theorem of Deligne (weight $k\ge 2$) and Deligne–Serre (weight $k=1$). Its analogues for Maass forms and for general automorphic representations remain open.

Timeline (as recorded in the source article, Wikipedia: Ramanujan–Petersson conjecture):

• 1916: Ramanujan conjectures that $\tau$ is multiplicative, that it satisfies the prime-power recursion, and that $|\tau(p)|\le 2p^{11/2}$.
• 1917: Mordell proves the first two statements, using what are now called Hecke operators.
• 1930: Petersson formulates the coefficient bound for holomorphic cusp forms for congruence subgroups.
• 1937: Hecke extends Mordell's method to holomorphic cusp forms in general.
• 1971: Deligne, building on Kuga, Sato, Shimura and Ihara, reduces the conjecture for weight $k\ge 2$ to the Weil conjectures via the Eichler–Shimura isomorphism (Deligne 1971).
• 1974: Deligne proves the Riemann hypothesis part of the Weil conjectures, which settles the case $k\ge 2$ and in particular $|\tau(p)|\le 2p^{11/2}$ (Deligne 1974). Deligne and Serre treat weight $k=1$ (Deligne–Serre 1974).

Setting

Let $\mathbb H=\{z\in\mathbb C:\operatorname{Im}z>0\}$ and $q=e^{2\pi i z}$. The Dedekind eta function is $\eta(z)=q^{1/24}\prod_{n\ge1}(1-q^n)$. The discriminant modular form is

$$\Delta(z)=q\prod_{n>0}(1-q^n)^{24}=\eta(z)^{24}.$$

It is a holomorphic cusp form of weight $12$ and level $1$. Ramanujan's tau function $\tau:\mathbb N\to\mathbb C$ is defined by the Fourier expansion

$$\Delta(z)=\sum_{n\ge1}\tau(n)q^n=q-24q^2+252q^3-1472q^4+4830q^5-\cdots.$$

Its Ramanujan $L$-function is the Dirichlet series $L(s,\tau)=\sum_{n\ge1}\tau(n)n^{-s}$.

More generally, let $\Gamma\subseteq SL(2,\mathbb Z)$ be a congruence subgroup, meaning that $\Gamma$ contains the principal congruence subgroup $\Gamma(N)$ for some $N\ge1$. A holomorphic cusp form of weight $k$ for $\Gamma$ is a holomorphic function $f:\mathbb H\to\mathbb C$ with $f(\gamma z)=(cz+d)^k f(z)$ for every $\gamma=\begin{pmatrix}a&b\\c&d\end{pmatrix}\in\Gamma$, which vanishes at every cusp. Such an $f$ is periodic with some least period $h>0$, and it has a Fourier expansion $f(z)=\sum_{n\ge1}a_n q_h^n$ with $q_h=e^{2\pi i z/h}$. When $\Gamma$ contains $z\mapsto z+1$ (for example $\Gamma_0(N)$, $\Gamma_1(N)$, or $SL(2,\mathbb Z)$ itself), $h=1$ and $q_h=q$.

Formalization targets

Goal: the Ramanujan–Petersson conjecture for holomorphic cusp forms

For every congruence subgroup $\Gamma$, every weight $k\ge1$, every cusp form $f$ of weight $k$ for $\Gamma$ with coefficients $a_n$, and every $\varepsilon>0$,

$$a_n=O_\varepsilon\!\left(n^{(k-1)/2+\varepsilon}\right).$$

The goal splits by weight into Deligne's theorem ($k\ge2$) and the Deligne–Serre theorem ($k=1$), both listed as milestones.

The tau function

1. Values: $\tau(1)=1$, $\tau(2)=-24$, $\tau(3)=252$, $\tau(4)=-1472$, $\tau(5)=4830$.
2. Multiplicativity (Mordell): $\tau(mn)=\tau(m)\tau(n)$ whenever $\gcd(m,n)=1$.
3. Recursion (Mordell): $\tau$ is not completely multiplicative, and $\tau(p^{j+1})=\tau(p)\tau(p^j)-p^{11}\tau(p^{j-1})$ for primes $p$ and $j\ge2$.
4. Ramanujan's bound (Deligne): $|\tau(p)|\le 2p^{11/2}$ for all primes $p$.
5. Consequences: $|\tau(n)|\le d(n)n^{11/2}$ for all $n\ge1$, where $d(n)$ is the number of divisors, and hence $\tau(n)=O(n^{11/2+\varepsilon})$.

The Ramanujan $L$-function

6. $\sum_{k\le n}\tau(k)=O(n^{13/2+\varepsilon})$, and $L(s,\tau)$ converges absolutely for $\operatorname{Re}s>13/2$.
7. $L(s,\tau)$ continues to an entire function satisfying $\dfrac{\Gamma(s)L(s,\tau)}{(2\pi)^s}=\dfrac{\Gamma(12-s)L(12-s,\tau)}{(2\pi)^{12-s}}$.
8. Euler product: $L(s,\tau)=\prod_p\sum_{n\ge0}\tau(p^n)p^{-ns}=\prod_p\big(1-\tau(p)p^{-s}+p^{11-2s}\big)^{-1}$ for $\operatorname{Re}s>13/2$.

Significance

The bound $|\tau(p)|\le 2p^{11/2}$ says that the roots of $1-\tau(p)u+p^{11}u^2$ have equal absolute value $p^{-11/2}$, an analogue of the Riemann hypothesis for the local factors of $L(s,\tau)$. The bounds for general cusp forms are used throughout analytic number theory to control sums of Fourier coefficients. They are also used in the explicit construction of Ramanujan graphs by Lubotzky, Phillips and Sarnak, which are optimal expander graphs. The generalized conjecture for $GL(n)$ implies Selberg's $1/4$ conjecture on Laplace eigenvalues.

All targets in this mission are proved theorems in the literature. At the pinned Mathlib revision, none of them is formalized except the identity $\tau(1)=1$. Mathlib does contain the definitions they need: $\eta$, $\Delta$ as a cusp form of weight 12 and level 1, $q$-expansions, congruence subgroups, and the $L$-function of a cusp form. Mathlib also proves the analytic continuation of that $L$-function. The remaining work is to formalize Hecke theory for $\Delta$, the elementary consequences of Deligne's bound, the $L$-function statements, and ultimately Deligne's and Deligne–Serre's theorems.

Difficulty

The algebraic statements about $\tau$ (multiplicativity, the recursion, the Euler product) and the functional equation are classical, but formalizing them needs infrastructure that Mathlib does not yet have, such as Hecke operators on cusp forms. The size bounds are of a different kind. Estimates from the Petersson inner product or from Hecke's method give only the exponent $k/2$ (Hecke's bound). That exponent is attainable by complex analysis alone, but the improvement to $(k-1)/2$ is not. In the literature it depends on arithmetic geometry: Deligne's proof of the Weil conjectures for $k\ge2$, and Galois representations for $k=1$. The analytically similar statement for Maass forms is still open.

Formalization scope

• $\tau(n)$ is defined as the $n$-th coefficient of Mathlib's $q$-expansion of ModularForm.discriminant with period $1$, as a complex number. The source's description of $\tau$ is taken as the definition, and integrality is not assumed.
• Absolute values are complex norms. $n^{11/2}$ and similar powers are real powers of nonnegative reals.
• $O(\cdot)$ is Mathlib's big-O along atTop on $\mathbb N$, with the constant allowed to depend on $\varepsilon$.
• In the general goal, the coefficients are taken with respect to $q_h=e^{2\pi i z/h}$, where $h$ is the strict width of the cusp $\infty$ for $\Gamma$ (Subgroup.strictWidthInfty). This equals $1$ whenever $z\mapsto z+1$ lies in $\Gamma$. A congruence subgroup is CongruenceSubgroup.IsCongruenceSubgroup.
• The functional equation is stated only at points $s$ where neither $s$ nor $12-s$ is a pole of $\Gamma$. This avoids Mathlib's convention that $\Gamma$ is $0$ at its poles.
• The recursion is stated for $j\ge2$, exactly as in the source.
• The Maass-form and automorphic-representation versions, the function-field results and the bounds towards Ramanujan over number fields are outside this mission's scope. Mathlib lacks the definitions they need.

Selected references

• S. Ramanujan, On certain arithmetical functions, Trans. Cambridge Philos. Soc. 22 (1916), 159–184. http://ramanujan.sirinudi.org/Volumes/published/ram18.pdf
• H. Petersson, Theorie der automorphen Formen beliebiger reeller Dimension …, Math. Ann. 103 (1930), 369–436. https://doi.org/10.1007/BF01455702
• P. Deligne, Formes modulaires et représentations l-adiques, Sém. Bourbaki 1968/69, LNM 179 (1971). https://doi.org/10.1007/BFb0058801
• P. Deligne, La conjecture de Weil. I, Publ. Math. IHÉS 43 (1974), 273–307. https://doi.org/10.1007/BF02684373
• P. Deligne, J.-P. Serre, Formes modulaires de poids 1, Ann. Sci. ÉNS 7 (1974), 507–530. https://doi.org/10.24033/asens.1277
• P. Sarnak, Notes on the generalized Ramanujan conjectures, Clay Math. Proc. 4 (2005). http://www.claymath.org/publications/Harmonic_Analysis/chapter9.pdf

Motivation

How large can the order of a single permutation of $n$ objects be? The answer, Landau's function $g(n)$, is a basic invariant of the symmetric group $S_n$: it is the maximum number of times a permutation can be iterated before it returns to the identity. Because the order of a permutation is the least common multiple of its cycle lengths, $g(n)$ is also the largest least common multiple of the parts of a partition of $n$, which ties the question to the distribution of prime numbers.

Timeline.

• 1902–1903. E. Landau proved that $\ln g(n)\sim\sqrt{n\ln n}$.
• 1968. J.-L. Nicolas showed that $g$ is constant on arbitrarily long runs of consecutive integers.
• 1984. J.-P. Massias proved the explicit bound $\ln g(n)\le 1.05313836\sqrt{n\ln n}$ for all $n\ge 1$.
• 1988. Massias, Nicolas and Robin obtained a three-term asymptotic expansion of $\ln g(n)$, its expression through the inverse logarithmic integral, and the equivalence of a one-sided inequality with the Riemann hypothesis.
• 2002. K. Ford's bounds for the Riemann zeta function give the error term $x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})$ in the prime number theorem, which can be fed into the 1988 result.

Setting

For a natural number $n$, let $S_n$ be the group of all permutations of an $n$-element set. The order of $\sigma\in S_n$ is the least $k\ge 1$ with $\sigma^k=\mathrm{id}$. Landau's function is

$$g(n)=\max_{\sigma\in S_n}\operatorname{ord}(\sigma).$$

A partition of $n$ is a multiset of positive integers summing to $n$. The prime counting function $\pi(x)$ is the number of primes $p\le x$, the (offset) logarithmic integral is $\mathrm{Li}(x)=\int_2^x\frac{dt}{\ln t}$, and $\mathrm{Li}^{-1}$ is its inverse on $[2,\infty)$. Throughout, $\ln$ is the natural logarithm.

Formalization targets

Goal: Landau's theorem (1902)

$$\lim_{n\to\infty}\frac{\ln g(n)}{\sqrt{n\ln n}}=1.$$

Supporting milestones

1. Partition characterization: $g(n)=\max\{\operatorname{lcm}(\lambda):\lambda\vdash n\}$.
2. Initial values $g(0),\dots,g(8)=1,1,2,3,4,6,6,12,15$.
3. Nicolas (1968): for every $m$ there is $n$ with $g(n)=g(n+1)=\dots=g(n+m)$.
4. Massias–Nicolas–Robin (1988): $\ln g(n)=\sqrt{n\ln n}\Bigl(1+\frac{\ln\ln n-1}{2\ln n}-\frac{(\ln\ln n)^2-6\ln\ln n+9}{8(\ln n)^2}+O\bigl((\tfrac{\ln\ln n}{\ln n})^3\bigr)\Bigr)$.
5. Ford (2002): $\pi(x)-\mathrm{Li}(x)=O\bigl(x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})\bigr)$ for some $c>0$.
6. Massias–Nicolas–Robin (1988): if $\pi(x)-\mathrm{Li}(x)=O(R(x))$ with $R(x)=x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})$, then $\ln g(n)=\sqrt{\mathrm{Li}^{-1}(n)}+O\bigl(R(\sqrt{n\ln n})\ln n\bigr)$.
7. Riemann hypothesis criterion: $\ln g(n)<\sqrt{\mathrm{Li}^{-1}(n)}$ for all large $n$ $\iff$ RH.
8. $g(n)\le e^{n/e}$ for all $n$, with equality only at $n=0$.
9. Massias (1984): $g(n)\le\exp(1.05314\sqrt{n\ln n})$.

Significance

Landau's theorem pins down the growth rate of the largest element order in $S_n$, which bounds, for example, how long any fixed shuffle of $n$ cards can be repeated before the deck returns to its starting order. The refined statements quantify the second-order behaviour and connect it to the error term in the prime number theorem; the criterion in milestone 7 is one of the known elementary reformulations of the Riemann hypothesis, and is included as a faithful statement of the source, not as an expected deliverable. The other results are proved in the literature; formalizing them requires building the partition/lcm description of element orders in $S_n$ and quantitative prime-counting estimates on top of Mathlib.

Difficulty

The order of a permutation is easy to compute from its cycle type, but maximizing an lcm over all partitions is a non-linear optimization: the optimum uses prime powers whose sizes are dictated by the distribution of primes, so even the leading-order asymptotics need Chebyshev-type or prime number theorem estimates, and the refined milestones need the prime number theorem with an explicit error term.

Formalization scope

• $S_n$ is Equiv.Perm (Fin n); $g(n)$ is the supremum of orderOf σ over the finite group (a natural number; $g(0)=1$).
• Partitions are Mathlib's Nat.Partition n; the lcm of a partition is the Multiset.lcm of its parts.
• Real logarithms use Real.log (which returns $0$ at $0$ and is defined for negative input); all asymptotic statements are about $n\to\infty$, so the values at small $n$ are irrelevant there. The bounds in milestones 8–9 are stated for every $n$ and are true at $n=0,1$.
• $\pi(x)$ for real $x$ is Nat.primeCounting ⌊x⌋₊; $\mathrm{Li}$ is the offset logarithmic integral $\int_2^x dt/\ln t$; $\mathrm{Li}^{-1}(y)$ is the least $x\ge2$ with $\mathrm{Li}(x)\ge y$, which for $y\ge0$ is the inverse function value. Replacing $\mathrm{Li}$ by the full integral $\mathrm{li}$ changes the inverse by $O(\ln n)$ and does not affect any of the asymptotic statements.
• The Riemann hypothesis is Mathlib's RiemannHypothesis.

Contributions of reusable infrastructure (cycle-type lcm, prime-counting error terms, the logarithmic integral) are welcome.

Selected references

• E. Landau, Über die Maximalordnung der Permutationen gegebenen Grades, Arch. Math. Phys. Ser. 3, vol. 5, 1903.
• J.-L. Nicolas, Sur l'ordre maximum d'un élément dans le groupe $S_n$ des permutations, Acta Arithmetica 14 (1968), 315–332.
• J.-P. Massias, Majoration explicite de l'ordre maximum d'un élément du groupe symétrique, Ann. Fac. Sci. Toulouse Math. (5) 6 (1984), 269–281.
• J.-P. Massias, J.-L. Nicolas, G. Robin, Évaluation asymptotique de l'ordre maximum d'un élément du groupe symétrique, Acta Arithmetica 50 (1988), 221–242.
• K. Ford, Vinogradov's integral and bounds for the Riemann zeta function, Proc. London Math. Soc. 85 (2002), 565–633. https://doi.org/10.1112/S0024611502013655
• W. Miller, The maximum order of an element of a finite symmetric group, Amer. Math. Monthly 94 (1987), 497–506.
• OEIS A000793. https://oeis.org/A000793

Why an arithmetic lower bound is needed

The Riemann hypothesis asks whether every nontrivial zero of the actual Riemann zeta function has real part one half. The Connes formalization has a certified implication from positivity of the Weil distribution to RH. That implication supplies a criterion; its positivity hypothesis still needs a proof. The Green realization formalization supplies an independently certified physical carrier, actual-zero columns and bounded synthesis operators. Their construction does not establish the arithmetic inequality.

This open problem isolates a finite-certificate formulation of that inequality. The goal is new research within the existing formal development, not a theorem asserted by the cited papers. It is an RH-equivalent target. A proof of the reductions below is already available; a proof of the target itself is not.

The relevant historical distinction is explicit: Riemann stated the zero-location hypothesis in 1859; Connes' 1999 paper relates trace-formula and positivity questions to the zeros; the present Lean development certifies the conditional positivity criterion and the Green realization. None of these citations is offered as an unconditional proof of the new arithmetic certificate bound.

Actual zeros and the fixed physical carrier

Let $Z$ be the subtype of complex numbers $\rho$ satisfying $\zeta(\rho)=0$ and $0<\operatorname{Re}\rho<1$. Multiplicities are the existing natural analytic multiplicities. Reflection is $\rho\mapsto1-\overline\rho$, and conjugation is $\rho\mapsto\overline\rho$. For each actual zero, let $S_\rho$ be its finite reflection/conjugation orbit, called its quartet. Repeated orbit elements are removed by the finite-set construction, so the term does not assert four distinct zeros.

At a positive support radius $T$, the physical carrier $H_T$ is the existing closed Dirichlet energy-image completion on $[-T,T]$. Its energy convention is the integral of $|u'|^2+|u|^2/4$. Source lifts, Green columns and their pair normalization retain their published definitions. The original admissible tests are smooth compactly supported functions; the carrier is not defined from an arbitrary replacement zero family.

Write $p_{T,\tau}$ for the original positive column of an actual zero $\tau$, with the original reflected-pair and multiplicity normalization. Their complete squared-norm sum is certified summable at each positive radius. For a finite set $F\subset Z$, $P_F$ is the published synthesis of exactly these positive columns into $H_T$. Let $N_S$ be the original selected negative synthesis on the coefficient space for the unchanged quartet $S=S_\rho$.

Formalization target

For a positive accuracy $\delta$, define the already-published operators

$$B_F=P_F^*P_F+\delta I_F,\qquad C_{F,S}=P_F^*N_S,$$

and the selected coefficient correction

$$D_S(T,F,\delta)=\delta I_S-N_S^*N_S+C_{F,S}^*B_F^{-1}C_{F,S}.$$

The positive regularization makes $B_F$ strictly positive, including dependent or repeated columns. Its ring inverse is certified to be a genuine inverse for positive $\delta$.

The goal is

$$\forall\rho\in Z\;\forall b\in\mathbb R\;\exists T>\max(b,0)\;\forall\delta>0\;\exists F\subset Z\text{ finite}:$$ $$S_\rho\subseteq F,\quad F\text{ is reflection-closed},\quad \sum_{\tau\notin F}\|p_{T,\tau}\|^2<\delta,\quad D_{S_\rho}(T,F,\delta)\succeq0.$$

Here $T>\max(b,0)$ abbreviates the two strict inequalities in the Lean statement. The window is chosen before accuracy. The finite cutoff can depend on accuracy, but the selected negative quartet remains unchanged. The same accuracy occurs in the complete omitted tail and the correction operator.

What this target would establish

The certified fixed-window theorem identifies all-accuracy finite certificates with the original Picard marker being at least half the identity. The certified cofinal quartet criterion identifies arbitrarily large such quartet windows with Mathlib's Riemann hypothesis. Their composition has also been checked independently in the native Lean environment against the exact goal statement.

These two reductions are the principal milestones, alongside the existing literature-form positivity implication. Shared definitions and supporting theorems remain reusable library nodes. Certification of a reduction is distinct from establishing the nonnegative correction demanded by the goal. The goal is currently unproved and carries no RH or desired-positivity hypothesis.

The remaining difficulty

Finite tail cutoffs exist by summability, and regularized coefficient inverses exist by strict positivity. Those facts leave the sign of $D_S$ undetermined. An arithmetic representation of the full Weil operator alone also leaves that sign undetermined. The selected negative packet and the unselected negative background are different parts of the original signed operator; replacing one by the other changes the obligation.

The arithmetic transfer audit ZP-WEIL-MARKER-TRANSFER / RH-ZERO-PROV-2 records this distinction. Endpoint estimates or neutral-shell arguments contribute only when they supply the original lower bound with the required window and accuracy quantifiers. A bound at one boundary, an accuracy-dependent choice of window, or an estimate with a positive residual error floor does not supply the displayed target. No easier status is implied by its finite coefficient representation.

Formalization scope

The proposal uses Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474, with the published original quartet and selected-correction definitions. A separate native audit uses the existing Lean 4.34.0 repository environment. Complex Hilbert inner products are conjugate-linear in the first argument. Operator nonnegativity uses the existing continuous-linear-map order. Infinite tails are unordered sums on the actual-zero complement.

No simple-zero assumption, independence of columns, unregularized Gram inverse, replacement carrier, changed coefficient metric or silently restricted zero family is permitted. Quartets include zeros on the critical line; an empty actual-zero subtype would make the universal target vacuous, exactly as specified by the existing actual-zero indexing. New auxiliary definitions belong in shared definition bundles, and reusable algebraic lemmas belong in the library. The existing Green milestone history and dependency graph are retained.

Selected references

• B. Riemann, Ueber die Anzahl der Primzahlen unter einer gegebenen Grösse, Monatsberichte der Berliner Akademie, 1859. Original paper and translations.
• A. Connes, Trace formula in noncommutative Geometry and the zeros of the Riemann zeta function, Selecta Mathematica 5, 1999. arXiv:math/9811068. Source of the conditional positivity/RH context, not the new certificate inequality.
• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Springer, 2011. DOI. Functional-analytic background for the certified carrier.
• Published Lean results: cofinal quartet criterion, fixed-window selected certificates, and selected-correction definitions.
• monocap-tech/provenance, RH-ZERO-PROV-2 arithmetic-transfer checkpoint, 2026. Its stated status is representation complete, lower-bound theorem open, RH not proved.

Literature and source audit

The exact cofinal-quartet finite-certificate goal remains open. An independent Lean audit verifies its equivalence to Mathlib RiemannHypothesis by composing the two certified milestone reductions. The window is chosen before every positive regularization parameter; the selected actual-zero quartet is fixed, and the same parameter controls the full positive tail and selected correction. Tail summability and existence of inverses alone do not establish the required sign.

The foreign graph export ConnesRZ.weil_positivity_implies_RH matches the native ConnesRZClosed.weil_positivity_implies_RH: the older native ConnesRZ theorem takes explicitFormula as an input, discharged in Closed. The foreign record has a staged source qualification; it has not been edited.

Arithmetic transfer checkpoint: monocap-tech/provenance 178c83225b2300506ff622899d08ec3c987137d5, rh/checkpoints/RH_ZERO_PROV_2_EULER_WEIL_MARKER_TRANSFER_20260920.md, SHA256 0bb48b950f09220f7b2f193c16b45b15add0333906f919f8b50ca915f77a1a0d. Retained local Git bytes were verified; public availability is unverified. Critical-window location, the prescribed ordered-limit interface, and arithmetic endpoint/neutral-shell control remain open. RH is not established.