Number Theory

Motivation

The security of the RSA cryptosystem rests on the assumed difficulty of factoring large integers, and the best known classical algorithms for factoring run in super-polynomial time. In 1994 Peter Shor showed that a quantum computer can factor an $n$-digit integer in time polynomial in $n$ (Shor, SIAM J. Comput. 1997; conference version FOCS 1994). The algorithm has two parts. A classical reduction, due to Miller (1976), turns factoring into order finding: given $x$ coprime to $n$, find the least $r \ge 1$ with $x^r \equiv 1 \pmod n$. The quantum part solves order finding.

This mission formalizes the quantum part as Shor analyzes it in §5 of the journal paper: the construction of the quantum state, the probability of each measurement outcome, and the classical post-processing that reads $r$ off the measured value. The paper's claim is that one run of this procedure returns $r$ with probability at least $\varphi(r)/3r$.

Timeline:

• 1976: Miller reduces factoring to order finding (with randomization).
• 1985–1994: Deutsch, Bernstein–Vazirani and Simon give the quantum Fourier sampling ideas the algorithm builds on.
• 1994: Shor's FOCS paper introduces the factoring and discrete logarithm algorithms.
• 1997: the SIAM J. Comput. version gives the analysis formalized here, with $q$ the power of $2$ in $[n^2, 2n^2)$.

Setting

Fix an integer $n \ge 2$ and an integer $x$ coprime to $n$. Its order $r$ is the least $r \ge 1$ with $x^r \equiv 1 \pmod n$; since $x$ is a unit, $r \le \varphi(n) < n$. Let $q = 2^l$ be the power of $2$ with $n^2 \le q < 2n^2$.

A quantum state on two registers, the first holding $0 \le a < q$ and the second a residue $y \in \mathbb{Z}/n$, is a complex vector $\psi(a, y)$ indexed by the basis states $|a, y\rangle$. Measuring it returns $|a, y\rangle$ with probability $|\psi(a, y)|^2$.

The Fourier matrix $A_q$ is the $q \times q$ matrix with entries $(A_q)_{a,c} = q^{-1/2}\exp(2\pi i a c/q)$, with rows indexing inputs and columns outputs. The algorithm

1. prepares $\frac{1}{q^{1/2}}\sum_{a=0}^{q-1}|a\rangle|x^a \bmod n\rangle$ (eq. (5.2)),
2. applies $A_q$ to the first register, obtaining $\frac1q\sum_{a,c}\exp(2\pi iac/q)|c\rangle|x^a \bmod n\rangle$ (eq. (5.4)),
3. measures, obtaining some $|c, y\rangle$,
4. rounds $c/q$ to the nearest fraction with denominator smaller than $n$.

The observed $c$ gives us $r$ if some fraction with lowest-terms denominator below $n$ is within $1/2q$ of $c/q$, and every such fraction has lowest-terms denominator exactly $r$. In the Lean development these objects are preFourierState, finalState, outcomeProb and yieldsOrder, in the namespace ShorAlgorithms.OrderFinding, and the shared definition ShorAlgorithms.Shared.fourierMatrix.

Formalization targets

Goal: success probability at least $\varphi(r)/3r$

For all sufficiently large $n$, with $x$, $r$ and $q$ as above,

where $\Psi$ is the state (5.4). The threshold on $n$ is uniform in $x$ and $q$; it is the paper's "for sufficiently large $n$" from the per-state bound.

Milestones

1. Eqs. (5.5)–(5.6). For $0 \le k < r$, the probability of $|c, x^k\rangle$ equals $\left|\frac1q\sum_{b=0}^{\lfloor (q-k-1)/r\rfloor}\exp(2\pi i(br+k)c/q)\right|^2$.
2. Eq. (5.11). For $n$ past a threshold, every $|c, x^k\rangle$ with $-r/2 \le rc - dq \le r/2$ for some integer $d$ has probability at least $1/3r^2$.
3. Eq. (5.13). If $n^2 \le q$, at most one fraction with denominator below $n$ lies within $1/2q$ of $c/q$.
4. p. 1500. Such a fraction is a convergent of the continued fraction of $c/q$.
5. p. 1501. At least $\varphi(r)$ values of $c$ are within $1/2q$ of some $d/r$ with $\gcd(d, r) = 1$; with the $r$ distinct values of $x^k$ this gives at least $r\varphi(r)$ states $|c, x^k\rangle$, and each such $c$ gives us $r$.

Significance

The goal is the quantitative statement behind "order finding is in bounded-error quantum polynomial time": since $\varphi(r)/r \ge \delta/\log\log r$ for a constant $\delta$ (Hardy and Wright, Thm. 328), $O(\log\log r)$ repetitions find $r$ with high probability, and Miller's reduction then factors $n$. Without the bound, the algorithm is a procedure with no guarantee.

The result is proved, in the paper and in textbooks (Nielsen and Chuang, 2000, §5.3), usually with a phase-estimation analysis rather than Shor's direct count. What this mission adds is a machine-checked proof of Shor's own argument, with his choice of $q$ and his constants, starting from the state built by applying $A_q$ to (5.2). Formal proofs of idealized versions exist elsewhere, for instance in the exact-period model where $r$ divides $q$ and the output is uniform on $r$ peaks, but that model removes the approximation that the $1/3r^2$ bound is about. Legendre's theorem on continued fractions is already on the platform (FamousTheorems.legendre_continued_fraction_theorem) and is included as a reference item.

Difficulty

The obvious route is to compute the output distribution in closed form. That works only when $r$ divides $q$; here $q$ is a power of $2$ and $r$ is arbitrary, so the amplitudes are geometric sums of $\lfloor (q-k-1)/r\rfloor + 1$ terms whose phases do not cancel exactly. The per-state bound $1/3r^2$ requires a lower bound on such a sum that is uniform in $r$, $c$ and $k$, with error terms of order $1/q$ controlled against a main term of order $1/r^2$. The constant $1/3$ leaves only a small margin below the limiting value $4/\pi^2 \approx 0.405$, so the errors must be bounded explicitly, not merely shown to vanish.

The second difficulty is the counting: distinct coprime numerators $d$ must give distinct outcomes $c$ in $[0, q)$, and each good $c$ must determine $r$ uniquely, which uses $r < n$ and $n^2 \le q$.

Formalization scope

Conventions the statements commit to:

• States are functions Fin q × ZMod n → ℂ; the matrix convention is row = input, so applying $A_q$ to the first register gives the amplitude $\sum_a \psi(a, y)(A_q)_{a,c}$ at $(c, y)$.
• The final state is built by applying $A_q$ to the state (5.2); the closed forms (5.5) and (5.6) are theorems, not definitions. No normalization hypothesis is assumed.
• Probabilities are squared moduli; the probability of the event "$c$ gives us $r$" sums over all $y \in \mathbb{Z}/n$, which is exact because $y$ that are not powers of $x$ have probability zero.
• $x$ is a natural number with $\gcd(x, n) = 1$; $r$ is orderOf (x : ZMod n). $q$ enters through the three hypotheses $q = 2^l$, $n^2 \le q$, $q < 2n^2$, not through a function of $n$.
• Fractions are rationals, and "in lowest terms" is Rat.den.
• Thresholds "for sufficiently large $n$" are $\exists N,\ \forall n \ge N$, with $N$ quantified before $x$, $q$, $c$ and $k$.
• Condition (5.11) is stated in its equivalent form (5.12), with an integer $d$.
• Printed slip. Eq. (5.13)'s justification says "Because $q > n^2$", but $q$ was chosen with $n^2 \le q$, and $q = n^2$ when $n$ is a power of $2$. The uniqueness claim holds under $n^2 \le q$, and that is what is stated.

Typing the closed form (5.4)–(5.6) in as the definition of the final state would make milestone 1 trivial and hide whether the probability model is the paper's; the definitions exclude this by construction.

Not stated: the polynomial running time of any step, the $O(\log\log r)$ repetition count (no explicit constant), the reversible modular exponentiation of §3, and the post-processing heuristics on p. 1501. Needed infrastructure: bounds on geometric exponential sums, Euler's totient, Diophantine approximation by fractions with bounded denominator, and Mathlib's continued fractions. Lemmas on geometric sums of roots of unity and on the order of units mod $n$ are reusable in the companion discrete logarithm mission.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172
• P. W. Shor, Algorithms for quantum computation: discrete logarithms and factoring, Proc. 35th FOCS, 1994. https://doi.org/10.1109/SFCS.1994.365700
• G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13(3):300–317, 1976. https://doi.org/10.1016/S0022-0000(76)80043-8
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 5th ed., Oxford, 1979 (Ch. X, continued fractions; Thm. 328).
• M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge, 2000. https://doi.org/10.1017/CBO9780511976667

Motivation

Cutting planes for mixed-integer linear programs are often derived from convex sets that contain no integer point in their interior. Balas observed in 1971 that every such lattice-free convex set containing the current fractional LP solution in its interior yields a valid inequality, the intersection cut (Balas, Intersection cuts, Oper. Res. 19, 1971). The strongest cuts come from sets that are inclusionwise maximal, so the shape of maximal lattice-free convex sets matters to multi-row cut generation.

The case where the set lives in a subspace arises in practice. Taking $q$ rows of an optimal simplex tableau restricts the integer points to an affine subspace $f+W$ of $\mathbb R^q$ spanned by the tableau columns. When $W$ is irrational, its integer points span only a proper subspace $V\subsetneq W$. The classical theory does not cover this case, and it is the case that the second mission of this series (minimal valid inequalities of the relaxation $R_f(W)$) needs.

Timeline.

• Lovász (Geometry of numbers and integer programming, 1989) stated the characterization for rational subspaces (Proposition 3.1) and gave only a sketch of the proof. The irrational-hyperplane case is not visible in that sketch.
• Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543v1; Math. Oper. Res. 35(3), 2010, doi:10.1287/moor.1100.0461) gave a complete proof of Lovász's theorem for an arbitrary lattice of a linear space (Theorem 10). They also extended it to a space $W$ strictly larger than the span $V$ of the lattice (Theorem 9, equivalently Theorem 1 for $\mathbb Z^n$).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product and the open balls $B_\varepsilon(x)$. For $X\subseteq\mathbb R^n$, $\langle X\rangle$ denotes its linear span.

A lattice of a linear space $V$ is an additive group $\Lambda=\{\lambda_1a_1+\dots+\lambda_ma_m\mid\lambda_i\in\mathbb Z\}$ generated by linearly independent vectors $a_1,\dots,a_m$ with $\langle a_1,\dots,a_m\rangle=V$ (Definition 6, IsLatticeOf Λ V). A linear subspace $L\subseteq V$ is a $\Lambda$-subspace if it has a basis contained in $\Lambda$ (Definition 7, IsLambdaSubspace Λ V L). For $\mathbb Z^2$, the line $x_2=2x_1$ is a $\Lambda$-subspace and the line $x_2=\sqrt2x_1$ is not.

For sets $W,S$ the interior relative to $W$ is $\mathbf{int}_W(S)=\{x\in S\mid B_\varepsilon(x)\cap W\subseteq S\text{ for some }\varepsilon>0\}$ (intW W S). The relative interior is $\mathbf{relint}(S)=\mathbf{int}_{\operatorname{aff}(S)}(S)$.

Let $W\supseteq V$ be a linear space. A set $S$ is a $\Lambda$-free convex set of $W$ if $S\subseteq W$, $S$ is convex and $\Lambda\cap\mathbf{int}_W(S)=\emptyset$. It is maximal if no other $\Lambda$-free convex set of $W$ properly contains it (Definition 8, IsLambdaFree, IsMaxLambdaFree).

The statements also use a polyhedron in $W$ ($W$ intersected with finitely many closed half-spaces), a polytope (convex hull of a finite set), the dimension $\dim(S)$ of the affine hull with $\dim\emptyset=-1$ (affDim), and a facet: a nonempty face $S\cap\{\langle a,x\rangle=b\}$ of a valid inequality with $\dim F=\dim S-1$. The recession cone is $\operatorname{rec}(S)=\{r\mid x+tr\in S\ \forall x\in S,\ t\ge0\}$ and the lineality space is $\operatorname{rec}(S)\cap-\operatorname{rec}(S)$.

Formalization targets

Goal: Theorem 9 (p. 8)

For a lattice $\Lambda$ of $V$ and a linear space $W\supseteq V$ with $\dim W\ge1$, a set $S$ is a maximal $\Lambda$-free convex set of $W$ if and only if

Main milestone: Theorem 10 (p. 8)

For $\dim V\ge1$, $S$ is a maximal $\Lambda$-free convex set of $V$ if and only if either $S=P+L$ is a polyhedron with $P$ a polytope, $L$ a $\Lambda$-subspace and $\dim S=\dim P+\dim L=\dim V$, with no lattice point in $\mathbf{int}_V(S)$ and a lattice point in the relative interior of every facet; or $S=v+L$ is an affine hyperplane of $V$ whose direction $L$ is not a $\Lambda$-subspace.

Supporting milestones

Lemma 13 (bounded full-dimensional case), Lemma 15 (lattice points near half-lines), Lemma 16 ($S+\langle\operatorname{rec}S\rangle$ stays $\Lambda$-free), Lemma 17 (projection along a $\Lambda$-subspace is a lattice), Lemma 18 (lattice points near non-lattice subspaces), Lemma 19 (maximal hyperplanes), Claims 1 and 2 in the proof of Theorem 10, and identity (6), $\mathbf{int}_W(S)\cap V=\mathbf{int}_V(S\cap V)$.

Significance

Theorem 10 says that maximal lattice-free sets are cylinders over polytopes with a lattice point on every facet, apart from the irrational hyperplanes. This is the structural fact behind the finiteness of facet counts (at most $2^{\dim P}$) and behind every classification of maximal lattice-free sets in low dimension, such as the triangles and quadrilaterals of the two-row relaxation. Theorem 9 extends it to irrational subspaces. There the new cases are the half-spaces of (iii), which have $V$ on their boundary, and the hyperplanes of (ii), whose trace on $V$ is a hyperplane of $V$ that is not a $\Lambda$-subspace. Theorem 9 is the geometric input to the paper's Theorem 3: every minimal valid inequality of $R_f(W)$ is the gauge of a maximal lattice-free convex set of $f+W$.

These results are proved on paper. No machine-checked version of Lovász's theorem, of Theorem 9, or of the lattice-approximation Lemmas 15 and 18 is known to exist. The mission produces the definitions of lattices of subspaces, relative interiors and lattice-free sets on which the second mission of the series builds.

Difficulty

The obvious argument separates each lattice point from $S$ by a half-space and intersects the half-spaces. It gives a polyhedron only when finitely many lattice points matter, that is, when $S$ is bounded. For unbounded $S$, the recession directions must be shown to be lineality directions and to be spanned by lattice vectors. Both steps rest on simultaneous Diophantine approximation (Dirichlet's theorem) applied in irrational directions, and on a density argument for the projected lattice when the lineality space is not a $\Lambda$-subspace. In the subspace setting of Theorem 9, one must also track the interiors relative to $W$ and to $V$ separately. Identity (6) holds only when $\mathbf{int}_W(S)$ meets $V$, and the half-space case (iii) is exactly the case where it does not.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), linear spaces are Submodule ℝ, and $\Lambda$ is an AddSubgroup. All declarations live in the namespace MaxLatticeFree.Geometry. Every interior is relative (intW, relint). With the ambient topological interior, every subset of a proper subspace would be trivially lattice-free, and the classification would collapse. A lattice must have a linearly independent generating family; a dense finitely generated subgroup such as $\mathbb Z+\sqrt2\mathbb Z$ is excluded. Dimensions are integers with $\dim\emptyset=-1$, and facets are nonempty, so no dimension equation holds through truncated subtraction.

Two readings of the page are fixed.

1. Theorem 9 assumes $\dim W\ge1$ and Theorem 10 assumes $\dim V\ge1$. For $W=V=\{0\}$ the only maximal set is $\emptyset$, which satisfies none of the listed cases, so the printed statements are false there.
2. Identity (6) is stated under the three hypotheses its proof uses, not inside the case analysis of Theorem 9.

The paper's Theorem 1 (the same result for $\mathbb Z^n$ and affine $W$) is not included, and neither are the cited results of Barvinok and Dirichlet (Theorems 11, 14, Corollary 12). They are welcome as supporting lemmas. Infrastructure that is useful beyond this mission includes Dirichlet's simultaneous approximation theorem in $\mathbb R^m$, discreteness of lattices of subspaces, and the relation between intW/relint and Mathlib's intrinsicInterior.

Selected references

• A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543
• L. Lovász, Geometry of numbers and integer programming, in: Mathematical Programming: Recent Developments and Applications, 1989, pp. 177–210.
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
• A. Barvinok, A Course in Convexity, Graduate Studies in Mathematics 54, AMS, 2002. https://doi.org/10.1090/gsm/054

Motivation

The nearest common ancestor (nca) problem asks, for a fixed rooted tree and a sequence of vertex pairs $(v, w)$, for the deepest vertex that is an ancestor of both. It is a basic step in suffix-tree string algorithms and is equivalent to range-minimum queries (Bender, Farach-Colton, 2000). Harel and Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13 (1984) 338–355, gave the first algorithm answering each query on a static tree in constant time on a random-access machine after linear preprocessing.

Their construction reduces the general problem to the case of a complete binary tree, where §3 of the paper shows that nca queries can be answered "by direct calculation" on vertex numbers: multiplication, division, powers of two, the base-two logarithm and bitwise exclusive or. The later simplification of Schieber and Vishkin (1988) is built on the same in-order numbering of a complete binary tree. This mission formalizes that arithmetic core.

Timeline, as reviewed in the paper's §1 (pp. 338–340):

• 1976: Aho, Hopcroft and Ullman (SIAM J. Comput. 5) give an $O(n + m\alpha(m+n, n))$-time off-line algorithm on a pointer machine, and for static trees a random-access algorithm with $O(n \log\log n)$ preprocessing and $O(\log\log n)$ time per query.
• 1976: van Leeuwen (unpublished report) gives an $O(n + m \log\log n)$-time algorithm for linking roots and static trees that runs on a pointer machine in $O(n)$ space.
• 1980: Harel (Proc. 21st FOCS) gives a preliminary version of the paper's results.
• 1984: Harel and Tarjan prove that pointer machines need $\Omega(\log\log n)$ time per query on static trees (Theorem 1), and give the $O(n)$-preprocessing, $O(1)$-query random-access algorithm whose base case is the subject of this mission.

Setting

Fix $d \ge 0$ and let $T$ be the complete binary tree of depth $d$. A vertex is identified with the path from the root to it, a word of at most $d$ left or right turns; the root is the empty word and $T$ has $n = 2^{d+1} - 1$ vertices. Following the paper's Appendix (pp. 354–355):

• $w$ is an ancestor of $v$ ($v$ a descendant of $w$) if the word $w$ is a prefix of the word $v$; every vertex is its own ancestor. $v$ and $w$ are unrelated if neither is an ancestor of the other.
• The depth of $v$ is its distance to the root; its height $h(v)$ is the length of the longest path from a leaf to $v$, which in $T$ is $d - \operatorname{depth}(v)$.
• $\operatorname{nca}(v, w)$ is the vertex of greatest depth that is an ancestor of both: the longest common prefix.

The vertices of $T$ are numbered from $1$ to $n$ in symmetric order (in-order): at every vertex, first the left subtree, then the vertex, then the right subtree. $\mathrm{sym}(v)$ is the number of $v$ and $\mathrm{sym}^{-1}(i)$ the vertex numbered $i$. For $d = 4$ (Fig. 1 of the paper) the root is $16$, its children $8$ and $24$, and the leaves $1, 3, 5, \dots, 31$. $i \oplus j$ denotes bitwise exclusive or and $\lg$ the base-two logarithm.

Two procedures of §3 use only numbers, heights and $d$:

• the nca depth algorithm: return $d - h(v)$ if $\mathrm{sym}(w) \in [\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$; else $d - h(w)$ if the same holds with $v, w$ exchanged; else $d - \lfloor \lg(\mathrm{sym}(v) \oplus \mathrm{sym}(w)) \rfloor$;
• the depth algorithm: given $v$ and a depth $d_2 \le \operatorname{depth}(v)$, with $h = d - d_2$, return $\mathrm{sym}^{-1}\bigl(2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h\bigr)$.

Formalization targets

Goal: the nca algorithm is correct

The algorithm to compute $\operatorname{nca}(v,w)$ (p. 342) runs the nca depth algorithm to obtain $d_0$ and then the depth algorithm on $(v, d_0)$. The goal states that it returns the nearest common ancestor: for all vertices $v, w$ of $T$, with $d_0$ the output of the nca depth algorithm and $h = d - d_0$,

Milestones

In the order the paper uses them:

1. Numbers at height $h$ (p. 341): the vertices of height $h$ are numbered $2^h, 3\cdot 2^h, 5\cdot 2^h, \dots$ from left to right.
2. Lemma 1: $h(v)$ is the largest $h$ with $2^h \mid \mathrm{sym}(v)$.
3. Lemma 2: the descendants of $v$ are the vertices numbered in $[\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$.
4. Lemma 3: for a height $h \ge h(v)$, the height-$h$ ancestor of $v$ has number $2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h$.
5. Lemma 4: for unrelated $v, w$,

6. The nca depth algorithm returns $\operatorname{depth}(\operatorname{nca}(v,w))$.
7. The depth algorithm returns the number of the depth-$d_2$ ancestor of $v$.

Two supporting statements pin the definitions to the paper: $\mathrm{sym}$ is a bijection onto $\{1, \dots, 2^{d+1} - 1\}$, and the longest common prefix is the deepest common ancestor.

Significance

The constant-time nca computation on complete binary trees is the base case of the whole paper: §§4–5 embed an arbitrary tree into a moderately sized complete binary tree through a compressed tree and a balanced binary tree, and every query ends with the arithmetic of §3. The same idea, that in-order numbers encode ancestry in their low-order bits, underlies the Schieber–Vishkin algorithm. Lemma 1 identifies the height with the 2-adic valuation of the number, and Lemma 4 identifies the nca height with the position of the highest differing bit.

The results are proved in the paper, with the proofs left as "easy to verify". No machine-checked version of this numbering or of these four lemmas is known to exist in Mathlib or on this platform. A formal development supplies proofs of the four lemmas and the two algorithms, and a reusable library connecting in-order ranks of a complete binary tree to binary arithmetic (Nat.log, bitwise xor, 2-adic valuation).

Difficulty

The numbering is defined by a traversal order, while the lemmas speak about divisibility, floor division and exclusive or. The work lies in connecting the rank of a vertex in symmetric order to its closed form $(2j+1)\cdot 2^{h(v)}$, where $j$ is its left-to-right position. That counting argument sums the sizes of the subtrees that precede $v$ and is where most of the effort goes. Lemma 4 then needs the observation that two unrelated numbers agree in all bits above the height of their nca and differ in the bit at that height. This is a statement about Nat.testBit of the exclusive or, and it fails for related vertices. The algorithm statements add a case analysis whose first two cases overlap when $v = w$.

Formalization scope

• A vertex of the tree of depth $d$ is a List Bool of length at most $d$ (false = left). Ancestry is the prefix relation, $\operatorname{nca}$ the longest common prefix, depth the length, and height $d - \text{length}$. None of these structural notions uses the numbering.
• $\mathrm{sym}(v)$ is the number of vertices whose in-order sort key is lexicographically at most that of $v$. The key is the path with left $\mapsto 0$, right $\mapsto 2$, followed by $1$. The numbering is not defined by the closed form or by a recursion on numbers: a definition of that kind would make the height-$h$ numbering and Lemma 1 immediate and move the content of the mission into an uncheckable definition.
• $\lfloor \lg x \rfloor$ is Nat.log 2 x, which agrees for $x \ge 1$. $\oplus$ is ^^^ on $\mathbb N$, and floor division is / on $\mathbb N$.
• Interval tests $a \in [b - c + 1, b + c - 1]$ are written additively as $b + 1 \le a + c$ and $a + 1 \le b + c$. The subtractions $d - h(v)$ and $d - d_2$ never truncate for heights and depths of vertices.
• Lemma 3 states explicitly that $h \le d$ ("$h$ is a height") and that the ancestor exists. The depth algorithm assumes $d_2 \le \operatorname{depth}(v)$, as printed.
• $\mathrm{sym}^{-1}$ is not defined as a function. The goal and the depth algorithm state that a vertex has the computed number if and only if it is the nearest common ancestor (respectively the ancestor at depth $d_2$), which says that $\mathrm{sym}^{-1}$ of that number is that vertex.
• The $O(1)$ time bounds are not formalized, since the random-access machine model is out of scope.

Proofs of any milestone are welcome.

Selected references

• D. Harel and R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2) (1984), 338–355. https://doi.org/10.1137/0213024
• A. V. Aho, J. E. Hopcroft and J. D. Ullman, On Finding Lowest Common Ancestors in Trees, SIAM J. Comput. 5(1) (1976), 115–132. https://doi.org/10.1137/0205011
• B. Schieber and U. Vishkin, On Finding Lowest Common Ancestors: Simplification and Parallelization, SIAM J. Comput. 17(6) (1988), 1253–1262. https://doi.org/10.1137/0217079
• M. A. Bender and M. Farach-Colton, The LCA Problem Revisited, LATIN 2000, LNCS 1776, 88–94. https://doi.org/10.1007/10719839_9

Motivation

At one loop, the worldsheet of a closed string is a torus, and the one-loop vacuum amplitude of the bosonic string is an integral over all conformally inequivalent tori. Two tori with modular parameters $\tau$ and $\tau'$ are equivalent exactly when $\tau'=(a\tau+b)/(c\tau+d)$ for an integer matrix of determinant one, so a consistent string amplitude must be built from $SL(2,\mathbb Z)$-invariant data. In David Tong's Cambridge Part III lecture notes (Section 6.4), the partition function of the bosonic string is computed in lightcone gauge and written in terms of the Dedekind eta function; the notes then observe that the measure and the integrand are individually modular invariant. This invariance is the mechanism by which string theory avoids the ultraviolet divergences of point-particle loops: the integration region is a fundamental domain that never reaches $\operatorname{Im}\tau\to0$ (Polchinski 1986).

Setting

Write $\mathbb H=\{\tau\in\mathbb C:\operatorname{Im}\tau>0\}$. A modular transformation is the map

generated by $T:\tau\mapsto\tau+1$ and $S:\tau\mapsto-1/\tau$. With $q=e^{2\pi i\tau}$ the Dedekind eta function is

convergent and non-vanishing on $\mathbb H$. The partition function of a single free scalar field on the torus is, up to constant factors, (6.20)

and the bosonic string partition function is

where $\mathcal F=\{|\tau|\ge1,\ |\operatorname{Re}\tau|\le\tfrac12\}$ is the standard fundamental domain.

Formalization targets

Goal: the string integrand is modular invariant

For every $\tau\in\mathbb H$ and all $a,b,c,d\in\mathbb Z$ with $ad-bc=1$,

Milestones (Section 6.4, in the order of the notes)

1. $S$ and $T$ generate $SL(2,\mathbb Z)$.
2. Every $\tau\in\mathbb H$ is mapped into $\mathcal F$ by some modular transformation.
3. $\operatorname{Im}(\gamma\tau)=\operatorname{Im}\tau/|c\tau+d|^2$ and $d(\gamma\tau)/d\tau=1/(c\tau+d)^2$ (so $d^2\tau\mapsto d^2\tau/|c\tau+d|^4$).
4. The measure $d^2\tau/(\operatorname{Im}\tau)^2$ on $\mathbb H$ is $SL(2,\mathbb Z)$-invariant.
5. $\eta(\tau+1)=e^{2\pi i/24}\eta(\tau)$.
6. $\eta(-1/\tau)=\sqrt{-i\tau}\,\eta(\tau)$.
7. $Z_{\text{scalar}}$ is modular invariant.

Significance

The result. Modular invariance of the integrand is what makes the one-loop string amplitude well defined as an integral over the moduli space of tori, rather than over the whole upper half-plane: restricting to $\mathcal F$ is only consistent because nothing depends on the representative. It is the first instance of a consistency condition that, in the superstring, constrains the allowed gauge groups and spectra.

Formalizing it. The eta transformation laws are classical (Apostol 1990, Ch. 3); Mathlib contains the definition of the eta function and results on $SL(2,\mathbb Z)$ and its fundamental domain, but, to the mission author's knowledge, not the $S$-transformation law of $\eta$. The mission produces a self-contained formal statement of the physics claim "both the measure and the integrand are individually modular invariant" and asks for its proof; milestones 1–2 are expected to follow from existing Mathlib results, milestone 6 is the analytic core.

Difficulty

The $T$-law is immediate from the product. The $S$-law $\eta(-1/\tau)=\sqrt{-i\tau}\,\eta(\tau)$ is not visible from the product formula at all: it requires either Poisson summation / the Jacobi triple product for theta functions, or a Mellin-transform / Eisenstein-series argument ($\log\eta$ is an Eichler integral of $E_2$), together with care about the branch of the square root. Passing from generators to all of $SL(2,\mathbb Z)$ requires an induction on words in $S$ and $T$ in which the multiplier $|c\tau+d|$ must be tracked.

Formalization scope

Points of $\mathbb H$ are represented as complex numbers $\tau$ with the hypothesis $0<\operatorname{Im}\tau$; a modular transformation is given by four integers with $ad-bc=1$ and acts by TongString.modularAction a b c d τ = (aτ+b)/(cτ+d). The eta function is defined directly by Tong's product formula as TongString.dedekindEta, using Mathlib's unconditional infinite product tprod. The square root in the $S$-law is the principal branch, $(-i\tau)^{1/2}$, which is the one intended since $\operatorname{Re}(-i\tau)>0$. The invariant measure is formalized as the measure on $\mathbb C$ with density $(\operatorname{Im}\tau)^{-2}$ with respect to Lebesgue measure restricted to $\mathbb H$, and invariance as equality of push-forward measures. Constant prefactors that Tong explicitly drops (powers of $\alpha'$, $4\pi^2$) are omitted. Because every statement is restricted to $\operatorname{Im}\tau>0$, where $\eta$ has no zeros, the reciprocal $1/|\eta|$ is never a division by zero, so no statement is vacuous.

Selected references

• D. Tong, String Theory, Cambridge Part III lecture notes, 2009, Sections 6.4.1–6.4.2. http://www.damtp.cam.ac.uk/user/tong/string.html (arXiv:0908.0333)
• J. Polchinski, Evaluation of the one loop string path integral, Commun. Math. Phys. 104 (1986) 37. https://doi.org/10.1007/BF01210927
• T. M. Apostol, Modular Functions and Dirichlet Series in Number Theory, 2nd ed., Springer GTM 41, 1990, Chapter 3. https://doi.org/10.1007/978-1-4612-0999-7
• J.-P. Serre, A Course in Arithmetic, Springer GTM 7, 1973, Chapter VII.

Motivation

The Riemann hypothesis (RH) asserts that every zero of the Riemann zeta function $\zeta$ in the strip $0 < \operatorname{Re} s < 1$ has $\operatorname{Re} s = \tfrac12$. One of the few reformulations that turns RH into a positivity statement, rather than a statement about the location of points, goes back to A. Weil (1952): the explicit formula expresses a sum over the zeros of $\zeta$ as a sum of local contributions over the places of $\mathbb{Q}$, and RH is equivalent to the resulting functional being positive on elements of the form $g \star g^{*}$.

Connes' 1999 programme paper Noncommutative geometry and the Riemann zeta function takes this reformulation as its endpoint. It builds a geometric framework — the adele class space $X = \mathbb{A}/k^{*}$ carrying an action of the idele class group $C_k$ — in which the explicit formula appears as a Lefschetz formula, the zeros of $L$-functions appear spectrally, and the paper's concluding assertion (§3, p. 22) is that the validity of the global trace formula implies, and is in fact equivalent to, positivity of the Weil distribution, i.e. RH for all $L$-functions with Grössencharakter.

This mission formalizes the arithmetic core of that endpoint in its simplest instance: the global field $k = \mathbb{Q}$ with trivial Grössencharakter, so that the $L$-function is $\zeta$ itself. Concretely it asks for (i) the Riemann–Weil explicit formula for $\zeta$ in the shape of Connes' equation (11), and (ii) both directions of the equivalence between positivity of the resulting Weil distribution and RH.

A rough timeline of the statements involved: Riemann (1859) gave the first explicit formula; von Mangoldt (1895) proved it rigorously; Weil (Sur les "formules explicites" de la théorie des nombres premiers, 1952) extended it to all global fields and isolated the positivity criterion; Bombieri (Remarks on Weil's quadratic functional in the theory of prime numbers, 2000) studied the associated quadratic functional in detail; Connes (1996–1999) gave the trace-formula interpretation formalized in part here.

Setting

All objects live on the group $\mathbb{R}^{*}_{+}$, the module of the idele class group of $\mathbb{Q}$, written additively through $u = e^{t}$, $d^{*}u = dt$.

A test function is a map $g : \mathbb{R} \to \mathbb{C}$ that is $C^{\infty}$ and has compact support (IsTest).

Its transform is

which is Connes' $\widehat h(z) = \int_{C_k} h(u)\,|u|^{z}\,d^{*}u$ in the coordinate $u = e^{t}$, shifted by $\tfrac12$ so that $z$ is the variable of $\zeta$ (mellinHat). On the critical line, $\widehat{g}(\tfrac12 + i r) = \int_{\mathbb{R}} g(t) e^{irt}\,dt$ is the ordinary Fourier transform.

The involution is $g^{*}(t) = \overline{g(-t)}$, i.e. $h^{*}(u) = \overline{h(u^{-1})}$ (starInv), and convolution is $(g_1 \star g_2)(t) = \int_{\mathbb{R}} g_1(s)\, g_2(t-s)\, ds$ (conv).

The Weil distribution of a test function $g$ collects the pole terms, the finite places and the archimedean place:

where $\Lambda$ is the von Mangoldt function and $\psi = \Gamma'/\Gamma$ (weilDistribution, with the three pieces named mellinHat, primeSum, archTerm). The middle sum is Weil's contribution of the finite places $v = p$, the last integral the contribution of the real place.

The spectral side is

the sum over the zeros $\rho$ of $\zeta$ with $0 < \operatorname{Re}\rho < 1$, each counted with its multiplicity $m_\rho$ (zeroSum, IsCriticalZero, zeroMult).

Formalization targets

Goal — positivity of the Weil distribution implies RH

This is the direction that yields RH, and it is the weakest form of the endpoint of the paper: it fixes no rate, no test-function normalization beyond $C_c^{\infty}$, and no numerical constant.

Milestone — the explicit formula (Connes (11))

with the sum over zeros asserted to be (unconditionally) summable.

Milestone — the converse direction

Together with the goal this is the equivalence asserted on p. 22 of the paper, in the case $k = \mathbb{Q}$, trivial Grössencharakter.

Supporting statements

The $*$-identity $\widehat{g \star g^{*}}\left(\tfrac12 + ir\right) = \bigl|\widehat g\left(\tfrac12+ir\right)\bigr|^{2}$ on the critical line, and the fact that $g \star g^{*}$ is again a test function.

Significance

Weil's positivity criterion is one of the standard equivalent forms of RH, and the only one in which the arithmetic input (the primes, through $\Lambda$) and the archimedean input (the $\Gamma$-factor) enter as separate, explicitly computable local terms. Formalizing it produces a machine-checked bridge between the zeros of $\zeta$ and prime sums: the explicit formula milestone is the reusable object here, since essentially every analytic application of zeta zeros — zero-density estimates, prime-counting error terms, pair-correlation statistics — is an instance of it.

Status honesty: neither RH nor the positivity statement is known; the explicit formula and both implications relating positivity to RH are classical theorems, proved but not, as far as the catalog shows, formalized in Lean. Mathlib currently provides $\zeta$, its functional equation, the von Mangoldt function and $\Gamma$, but no explicit formula of any kind. What this mission adds on top of the paper is therefore the formal proof of known results, not new mathematics.

Difficulty

The obvious route to the explicit formula — integrate $-\zeta'/\zeta(s)\widehat g(s)$ over a vertical line, move the contour to the reflected line, collect residues — fails to be routine at exactly two points. First, moving the contour requires control of $\zeta'/\zeta$ on horizontal segments between zeros, which is where the classical proof invests most of its work; Mathlib has bounds near $\operatorname{Re} s = 1$ but nothing of this shape inside the strip. Second, the sum over zeros must be shown to converge unconditionally, which needs a zero-counting bound of Riemann–von Mangoldt type ($N(T) \ll T\log T$) that is not in Mathlib either.

For the goal implication, the naive idea — pick a test function whose transform is supported near a hypothetical off-line zero — is unavailable: $\widehat g$ is entire whenever $g$ has compact support, so it cannot be localized. The classical argument instead exploits the symmetry $\rho \mapsto 1-\bar\rho$ of the zero set and makes the off-line quadruple contribute a negative amount in the limit along a family of test functions.

Formalization scope

Conventions the Lean statements commit to. Test functions are $\mathbb{C}$-valued on $\mathbb{R}$, ContDiff ℝ (⊤ : ℕ∞) (so $C^{\infty}$, not analytic) with HasCompactSupport; the multiplicative group $\mathbb{R}^{*}_{+}$ is always written additively. The transform carries the $\tfrac12$-shift shown above, so the critical line is $\operatorname{Re} z = \tfrac12$ and $\widehat{g}(0), \widehat{g}(1)$ are the two pole terms. Zeros are indexed by the subtype $\{s : 0 < \operatorname{Re} s < 1,\ \zeta(s) = 0\}$ and weighted by (analyticOrderAt riemannZeta s).toNat; the trivial zeros are excluded. Integrals are Bochner integrals and sums are tsum, so both take the junk value $0$ when the integrand is not integrable or the family is not summable — for that reason the explicit formula is stated as a HasSum, which carries summability, rather than as an equation between tsums. The archimedean term is written with $\operatorname{Re}\psi$, $\psi =$ logDeriv Complex.Gamma, rather than as a principal value, to avoid a second regularization convention.

The goal is not trivially satisfiable: its hypothesis quantifies over a nonempty class (smooth bump functions exist), and its conclusion is RH for $\zeta$, so no vacuous reading is available.

Infrastructure a complete development needs, all reusable beyond this mission: growth bounds for $\zeta'/\zeta$ inside the critical strip, a Riemann–von Mangoldt zero-counting bound, Fourier analysis of $C^\infty_c$ functions (Paley–Wiener style decay of $\widehat g$), and the Hadamard product / functional equation package for the completed zeta function.

Out of scope, and deliberately so: Connes' operator-theoretic trace formula (equations (41) and (45) of the paper) and the spectral realization theorem of p. 17. Both are statements about traces of operators on Hilbert space, and Mathlib presently has no trace-class operator theory to state them faithfully. The mission therefore formalizes the arithmetic side of the paper's endpoint; contributions that build the missing operator theory, or that extend the statements from $\zeta$ to Dirichlet $L$-functions and Hecke $L$-functions with Grössencharakter, are welcome.

Selected references

• A. Connes, Noncommutative geometry and the Riemann zeta function, in Mathematics: Frontiers and Perspectives, AMS (2000) — the source of this mission (§3, equations (11) and (45), and the concluding assertion on p. 22).
• A. Connes, Trace formula in noncommutative geometry and the zeros of the Riemann zeta function, Selecta Math. (N.S.) 5 (1999) — reference [9] of the source. https://arxiv.org/abs/math/9811068
• A. Weil, Sur les "formules explicites" de la théorie des nombres premiers, Comm. Sém. Math. Univ. Lund (1952) — reference [27] of the source.
• E. Bombieri, Remarks on Weil's quadratic functional in the theory of prime numbers, I (2000).
• H. Iwaniec and E. Kowalski, Analytic Number Theory, AMS Colloquium Publications 53 (2004), Chapter 5 (explicit formulas).

Motivation

The Riemann hypothesis asserts that all nontrivial zeros of the Riemann zeta function lie on the critical line. A classical way to measure how far the hypothesis is from failing runs through a one-parameter deformation of the Riemann $\xi$ function by the backward heat flow. De Bruijn (1950) introduced a family of entire functions $H_t$, $t \in \mathbb{R}$, with $H_0$ essentially the $\xi$ function, and showed that $H_t$ has only real zeros for $t \ge 1/2$. Newman (1976) proved that there is a finite constant $\Lambda$, now called the de Bruijn–Newman constant, such that $H_t$ has only real zeros precisely when $t \ge \Lambda$. The Riemann hypothesis is exactly the statement $\Lambda \le 0$, and Newman conjectured the complementary bound $\Lambda \ge 0$ — in his phrase, that if the Riemann hypothesis is true, then it is only barely so.

Timeline of lower bounds on $\Lambda$, all obtained before 2018 by exhibiting Lehmer pairs, that is, pairs of adjacent zeros of $\zeta$ that are unusually close together: $\Lambda > -\infty$ (Newman 1976), $\Lambda \ge -50$ (Csordas–Norfolk–Varga 1988), $\Lambda \ge -5$ (te Riele 1991), $\Lambda \ge -0.385$ (Norfolk–Ruttan–Varga 1992), $\Lambda \ge -0.0991$ (Csordas–Ruttan–Varga 1991), $\Lambda \ge -4.379 \times 10^{-6}$ (Csordas–Smith–Varga 1994), $\Lambda \ge -5.895 \times 10^{-9}$ (Csordas–Odlyzko–Smith–Varga 1993), $\Lambda \ge -2.63 \times 10^{-9}$ (Odlyzko 2000), $\Lambda \ge -1.15 \times 10^{-11}$ (Saouter–Gourdon–Demichel 2011). Rodgers and Tao closed the gap in 2020 by proving $\Lambda \ge 0$. In the other direction, de Bruijn's bound $\Lambda \le 1/2$ was sharpened to $\Lambda < 1/2$ by Ki–Kim–Lee (2009) and to $\Lambda \le 0.22$ by the Polymath 15 project (2019).

Setting

For a real number $u$ put

a function that decays super-exponentially as $|u| \to \infty$ and satisfies $\Phi(u) = \Phi(-u)$. For each $t \in \mathbb{R}$ define the entire function

Each $H_t$ is even and satisfies $H_t(\bar z) = \overline{H_t(z)}$; the function $H_0$ is $\tfrac18 \xi\bigl(\tfrac12 + \tfrac{iz}{2}\bigr)$, so the Riemann hypothesis says exactly that every zero of $H_0$ is real. Write

By Pólya and Newman, $S$ is the ray $[\Lambda, \infty)$ with $-\infty < \Lambda \le 1/2$.

When $\Lambda < t \le 0$ the zeros of $H_t$ are real, simple, symmetric about the origin and avoid the origin, so they can be listed as $(x_j(t))_{j \in \mathbb{Z}^*}$, indexed by the nonzero integers, with $0 < x_1(t) < x_2(t) < \cdots$ and $x_{-j}(t) = -x_j(t)$. The classical locations $\xi_j$ are defined for $j \ge 1$ by $\Psi(\xi_j) = j$ with

extended by $\xi_{-j} = -\xi_j$; they are the positions the zeros would occupy if the Riemann–von Mangoldt counting formula were exact. Throughout, $\log_+ x := \log(2 + |x|)$.

Formalization targets

Goal — Newman's conjecture

The goal is stated in both forms simultaneously, so that it does not depend on any convention for the infimum of a set that might be empty or unbounded below.

Milestones

The milestone list follows the architecture of Rodgers–Tao, which is a proof by contradiction: every milestone is stated under the standing hypothesis $\Lambda < 0$ of that paper, in the time ranges the paper uses ($\Lambda < t \le 0$, then $\Lambda/2 \le t \le 0$, then $\Lambda/4 \le t \le 0$). In order: an upper bound for $H_t$ near the real axis (Lemma 4); Riemann–von Mangoldt type counting formulae for the zeros of $H_t$ (Theorem 9); the resulting macroscopic description of the zeros (Corollary 10); the equations of motion $\partial_t x_k = 2\sum_{j \ne k} (x_k - x_j)^{-1}$ (Theorem 11); a quantitative lower bound on gaps between zeros (Proposition 13); a bound on the time-integrated renormalized energy (Theorem 17); and a bound on that energy at time $t = 0$ (Proposition 26). The last of these says that at time zero the zeros are, on average, locally in the equilibrium configuration of an arithmetic progression, which contradicts known results on the local distribution of zeros of $\zeta$.

Significance

$\Lambda \ge 0$ settles Newman's conjecture, and together with the Riemann hypothesis it would force $\Lambda = 0$. Unconditionally, it says that the zeros of $\xi$ are not in local equilibrium: infinitely often, gaps between consecutive zeros deviate from the mean spacing, which is what makes the pair correlation phenomenology of Montgomery and of Conrey–Ghosh–Goldston–Gonek–Heath-Brown incompatible with $\Lambda < 0$. Any proof of the Riemann hypothesis must therefore be compatible with the hypothesis being tight in this sense.

The theorem has a complete published proof (Rodgers–Tao, Forum of Mathematics, Pi, 2020); it is not an open problem. What is missing is a machine-checked proof. To the extent the material has been formalized at all, the underlying objects — the $\xi$ function, the heat flow $H_t$, the counting function for zeros, the zero dynamics, the renormalized energies — are not available in Mathlib, so the mission produces reusable analytic infrastructure: bounds for a Fourier–Laplace type integral by the saddle point method, a Riemann–von Mangoldt counting argument via the argument principle, and a gradient-flow monotonicity framework for an infinite particle system with logarithmic interaction.

Difficulty

The obvious route to $\Lambda \ge 0$ is the one used for every previous lower bound: exhibit Lehmer pairs of ever higher quality, since if $\Lambda$ were very negative the zeros of $H_0$ would repel each other and unusually close pairs of zeta zeros could not exist. Producing an infinite sequence of Lehmer pairs of arbitrarily high quality is possible under the GUE hypothesis, but the known unconditional upper bounds for small gaps between zeta zeros are too weak, even assuming the Riemann hypothesis. The proof instead upgrades repulsion to relaxation to local equilibrium: it must control the zeros of $H_t$ uniformly for $\Lambda < t \le 0$ at length scales as fine as $\log T$, with only the weaker counting formulae available for negative $t$ (an error term $O(\log_+^2 T)$ rather than $O(\log_+ T)$), and must make sense of a Hamiltonian and an energy that are given by divergent series, which requires truncation, renormalization, and careful control of all the resulting boundary terms.

Formalization scope

The Lean development commits to the following conventions. $\Phi$ is a tsum over the positive integers and $H_t(z)$ is the Bochner integral over $(0, \infty)$ of $e^{tu^2}\Phi(u)\cos(zu)$; no convergence or entireness statement is built into the definition. $\Lambda$ is sInf of the set of admissible times, and the goal theorem also states the quantifier form "every admissible $t$ is nonnegative", so it cannot be satisfied by a junk value of the infimum. The zero families $(x_j(t))$ and the classical locations $(\xi_j)$ are not defined by choice functions: they enter the milestones as universally quantified functions $\mathbb{Z} \to \mathbb{R}$ subject to explicit predicates saying exactly which sequences they are, so a milestone asserts something about every valid enumeration. Asymptotic notation is unfolded: $O(\cdot)$ becomes an explicit existential constant, $o_{T \to \infty}(\cdot)$ an explicit $\varepsilon$–$T_0$ statement, and a principal value sum a limit of symmetric partial sums. Where a statement asserts the value of a time integral, absolute integrability is part of the conclusion, so the statement cannot be satisfied by the convention that a non-integrable function has integral zero.

One degeneracy is inherent to the source and is stated here explicitly: since the paper argues by contradiction, each milestone carries the hypothesis $\Lambda < 0$ (directly, or through a time range such as $\Lambda < t \le 0$). Once the goal theorem is proved, those hypotheses are unsatisfiable and the milestones become vacuously true. They are the intended attack path on the goal, not independent targets, and a solver who derives one of them from the goal theorem contributes nothing.

Contributions welcome: the analytic estimates for $H_t$ (Lemma 4) and the counting formulae (Theorem 9) are independent of the dynamical part and are the natural entry points; Mathlib-level infrastructure on the argument principle, the saddle point method, and Stirling asymptotics for $\Gamma$ in vertical strips is reusable well beyond this mission.

Selected references

• B. Rodgers and T. Tao, The de Bruijn–Newman constant is non-negative, Forum of Mathematics, Pi 8 (2020), e6. https://doi.org/10.1017/fmp.2020.6
• N. G. de Bruijn, The roots of trigonometric integrals, Duke Math. J. 17 (1950), 197–226. https://doi.org/10.1215/S0012-7094-50-01720-0
• C. M. Newman, Fourier transforms with only real zeros, Proc. Amer. Math. Soc. 61 (1976), 246–251. https://doi.org/10.1090/S0002-9939-1976-0434982-5
• G. Csordas, W. Smith and R. S. Varga, Lehmer pairs of zeros, the de Bruijn–Newman constant $\Lambda$, and the Riemann hypothesis, Constr. Approx. 10 (1994), 107–129. https://doi.org/10.1007/BF01205170
• H. L. Montgomery, The pair correlation of zeros of the zeta function, Proc. Sympos. Pure Math. XXIV (1973), 181–193. https://doi.org/10.1090/pspum/024
• J. B. Conrey, A. Ghosh, D. Goldston, S. M. Gonek and D. R. Heath-Brown, On the distribution of gaps between zeros of the zeta-function, Q. J. Math. 36 (1985), 43–51. https://doi.org/10.1093/qmath/36.1.43
• D. H. J. Polymath, Effective approximation of heat flow evolution of the Riemann $\xi$ function, and a new upper bound for the de Bruijn–Newman constant, Res. Math. Sci. 6 (2019), 31. https://doi.org/10.1007/s40687-019-0193-1

A complete formal proof of Fermats Last Theorem for exponent 5: for all positive natural numbers a,b,c, a^5 + b^5 != c^5. The proof follows the classical Legendre-Dirichlet approach (1825-1830): Case 1 (5 does not divide a,b,c) is dispatched by congruences, and Case 2 (5 divides one of them) uses infinite descent through the ring Z[zeta_5]. The open hard leaf is the Z[zeta_5] PID step (flt5_zeta5_ring_witnesses).

Y. Bai (arXiv:2609.11276, September 2026) proves that the irrationality measure of π is at most 7.101862832357, improving the Zeilberger–Zudilin bound 7.103205334137 (2020). The proof keeps the Zeilberger–Zudilin integral but gives its numerator two independent exponents, specialised at A₁ = A₂ = 1857/2785; the resulting integer linear forms in 1 and π, combined with Hata's lemma, give μ(π) ≤ 7.101862832357. This entry is the campaign template with the value 7.101862832357. Source: https://arxiv.org/abs/2609.11276

Motivation

Shor's algorithm is a quantum algorithm that finds a nontrivial factor of an integer $N$ in time polynomial in $\log N$, and its variants compute discrete logarithms in finite cyclic groups. It was developed by Peter Shor in 1994 (Shor, FOCS 1994; Shor, SIAM J. Comput. 1997). No classical polynomial-time factoring algorithm is known; the best classical method, the general number field sieve, runs in sub-exponential time. Because the security of RSA and of finite-field and elliptic-curve Diffie–Hellman rests on the hardness of factoring and of discrete logarithms, Shor's algorithm is the main reason these schemes are considered breakable by a large fault-tolerant quantum computer, and the main motivation for post-quantum cryptography.