Number Theory

Motivation

Birational anabelian geometry studies how much of a function field is determined by a small quotient of its absolute Galois group. This mission isolates uniqueness in the reconstruction correspondence. The source manuscript presents the surrounding research claim.

Setting

Fix a prime ℓ. The fields K/k and L/l are essentially finite type extensions of algebraically closed constant fields, have transcendence degree at least two, and have characteristic different from ℓ. The abelian-by-central datum records the pro-ℓ abelian quotient and the commutator pairing. IsomF consists of constant-preserving perfect-closure isomorphisms modulo Frobenius; IsomCUnits quotients bracket-compatible Galois isomorphisms by the encoded ℓ-adic unit relation.

Formalization target

For field-isomorphism classes a and a′ and a Galois-isomorphism class b, prove

$$\operatorname{PhiGraph}(a,b)\;\land\;\operatorname{PhiGraph}(a^{\prime},b)\quad\Longrightarrow\quad a=a^{\prime}.$$

PhiGraph is the relation induced by representatives and a compatible extension to algebraic closures.

The selected formal target is OAI.BogomolovPop.main_graph_injective.

Significance and status

This establishes uniqueness of the field class whenever two representatives produce the same Galois class. The manuscript states a full reconstruction bijection; the selected published Lean target is its graph-injectivity assertion. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Equality is required after two different quotient constructions, one generated by Frobenius and one by ℓ-adic scalar limits. Recovering equality of classes must respect both ambiguities and the contravariant Galois action.

Formalization scope

The definition block constructs topological pro-ℓ quotients, closed commutator subgroups, perfect closures and the pullback graph. The theorem quantifies over arbitrary field types with the stated algebraic instances. It does not assert existence, surjectivity or functionality of PhiGraph, and those broader manuscript conclusions are not attached as proved results. Only the existing injectivity target and its definition block are referenced.

Selected references

• OpenAI, The Bogomolov-Pop reconstruction theorem, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Compatibility between reassociation and braiding imposes equations on formal Lie expressions. The question is whether those equations leave precisely the free family of odd-weight generators predicted by the Deligne–Drinfeld conjecture. The source manuscript presents the surrounding research claim.

Setting

Let L be the free Lie algebra over ℚ on x and y, each of weight one. The solution space W satisfies antisymmetry, the three-term relation, and the pentagon equation in the four-strand infinitesimal braid algebra. Its operation is the Ihara bracket {p,q}=Dₚq−D_qp+[p,q]. The free algebra F has generators indexed by k ≥ 0 with weights 2k+3.

Formalization target

Establish a graded bracket-preserving linear equivalence

$$F=\operatorname{Lie}_{\mathbb Q}\langle e_3,e_5,e_7,\ldots\rangle\;\cong\;W,$$

together with mutually inverse continuous maps on the products of weight pieces. The completed maps must preserve the bracket degree by degree, including the finite convolution sum defining its weight-n component.

The selected formal target is OAI.DeligneDrinfeld.main.

Significance and status

The target simultaneously expresses freeness and exhaustion of the full equation space. Finding a free subalgebra alone leaves the exhaustion assertion unresolved. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The pentagon relation couples substitutions in the braid Lie algebra. Constructing odd-weight solutions does not by itself show that all solutions are generated by them, nor that the completed bracket has the required compatibility.

Formalization scope

The published definition block specifies the braid quotient, tangent construction of D, weighted Lie words, rational submodules and product completions. Generator k has weight 2k+3. The factor spaces carry the explicitly supplied discrete topology. The goal is exactly MainStatement, including its inverse, continuity and completed-bracket clauses. The available reference set supplies the definition block and one target, so no unsupported paper lemmas are attached as milestones.

Selected references

• OpenAI, The Deligne-Drinfeld conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation: how short can an Egyptian fraction be?

An Egyptian-fraction expansion writes a positive rational number as a sum of distinct unit fractions $1/n$. Every fraction $a/b$ with $1\le a<b$ has one, by the greedy algorithm, but greedy expansions can be long. The basic quantitative question is how many terms are needed in the worst case for a fixed denominator $b$. Let $N(a,b)$ be the least length of an expansion of $a/b$ with denominators $\ge2$, and $N(b)=\max_{1\le a<b}N(a,b)$. Erdős proved in 1950 that $N(b)\ll\log b/\log\log b$, showed that $N(b)\gg\log\log b$ (already for $a=b-1$), and conjectured that the double-logarithmic order is correct. The question appears in Erdős–Graham's 1980 problem book and as Erdős Problem 304. The same circle of questions asks how many expansions of $1$ with exactly $k$ terms exist, and which integers can appear as denominators in them (Erdős Problem 293).

Timeline

• 1940 — Nakayama studies $N(a,b)$ through arithmetic criteria for expansions with few terms (Tohoku Math. J. 46).
• 1950 — Erdős reports de Bruijn's bound $N(b)\ll\log b/\log\log\log b$, improves it to $N(b)\ll\log b/\log\log b$, proves the lower bound $N(b)\gg\log\log b$, and conjectures the matching upper bound (Mat. Lapok 1950).
• 1980 — Erdős and Graham restate the problem and ask for estimates of the number of $k$-term expansions of $1$ and for the least missing denominator (Old and New Problems…).
• 1985 — Vose proves $N(b)\ll\sqrt{\log b}$ (Bull. LMS 17).
• 1990 — Tenenbaum and Yokota give length $(1+\varepsilon)\log b/\log\log b$ with denominators $O(b(\log b)^2\log\log b)$ (J. Number Theory).
• 2014–2021 — Konyagin proves a lower bound for the number $F(k)$ of $k$-term expansions of $1$ with $\log\log F(k)\gg k/\log k$ (Mat. Zametki); Elsholtz extends it to restricted denominators (Q. J. Math.); Elsholtz and Planitzer prove $\log\log F(k)=O(k)$ (Bull. LMS).
• 2026 — van Doorn and Tang prove $v(k)\ge\exp(ck^2)$ for the least missing denominator (Math. Proc. Cambridge Philos. Soc.).
• 2026 — An OpenAI preprint, Short Egyptian fractions (OpenAI Math Release, September 25, 2026), claims $N(b)\asymp\log\log b$, settling Erdős's conjecture, together with $\log\log F(k)\asymp k$ and $\log\log v(k)\asymp k$. It has not been peer reviewed, and its proofs are not formally verified.

Setting

For integers $1\le a<b$, an expansion of $a/b$ is a finite list $2\le n_1<\dots<n_k$ of integers with

$$\frac ab=\frac1{n_1}+\dots+\frac1{n_k}.$$

The fraction need not be in lowest terms and the denominators are unbounded. $N(a,b)$ is the least such $k$, and

$$N(b)=\max_{1\le a<b}N(a,b).$$

For $k\ge1$, $F(k)$ is the number of tuples $1\le n_1<\dots<n_k$ with $\sum 1/n_i=1$; $D_k$ is the set of integers $m\ge2$ occurring as some $n_i$ in such a tuple; and $v(k)=\min(\{2,3,\dots\}\setminus D_k)$.

Formalization targets

Goal: the optimal order of the shortest expansions (Theorem 1.1)

Every $a/b$ with $1\le a<b$ has an expansion, and there are absolute constants $c_1,c_2>0$ and $b_0$ such that for every $b\ge b_0$

$$c_1\log\log b\;\le\;N(b)\;\le\;c_2\log\log b .$$

No values of the constants are fixed. The goal statement is published on the platform with status Open.

Milestones

• Theorem 1.1, second formulation, stated with the definitions shared by the corollaries below.
• Corollary 1.2: there are $c,C>0$ and $k_0$ with $ck\le\log\log F(k)\le Ck$ for every $k\ge k_0$.
• Lemma 7.2: for $r\ge3$, any exact $r$-term expansion of $1$ containing the denominator $m$ can be lengthened to an exact $(r+1)$-term expansion still containing $m$; hence $D_r\subseteq D_{r+1}$.
• Proposition 8.1: for every $\varepsilon>0$, every sufficiently large $m$ is a denominator in an expansion of $1$ with at most $(257/\log2+\varepsilon)\log\log m$ terms.
• Corollary 1.3: eventually $\exp(\exp(k/600))\le v(k)\le1+k^{2^{k-1}}$, and $\log2/257\le\liminf_k \log\log v(k)/k\le\limsup_k\log\log v(k)/k\le\log2$.

Significance

The result itself. Theorem 1.1 answers Erdős's 1950 conjecture (Erdős Problem 304) affirmatively. The lower bound is classical; the content is the uniform upper bound for every numerator. As consequences, the paper determines the double-logarithmic order of the number of representations of $1$ (Corollary 1.2) and of the least integer absent from all $k$-term expansions of $1$ (Corollary 1.3), improving van Doorn–Tang's $\exp(ck^2)$ lower bound to a double exponential.

Formalizing it. All statements are elementary, with no analytic objects beyond logarithms, so a formal proof would give a complete machine-checked account of a problem from Erdős's list. The proof uses residue distribution of divisors, uniform divisor moments and a probabilistic construction, none of which is machine-checked. The elementary pieces — finiteness of $F(k)$, the denominator bound $n_i\le k^{2^{i-1}}$, and the padding lemma — are independently checkable and useful for other unit-fraction problems.

Difficulty

The greedy algorithm and divisor methods (Erdős; Tenenbaum–Yokota) lose a factor $\log b/(\log\log b)^2$ because they treat each numerator individually. The proof instead builds an auxiliary denominator $M$ for which almost every numerator in a large range has a short expansion, and descends through $O(\log\log b)$ ranges. The obstacle is that the exceptional numerators at each level could accumulate during the descent; controlling them requires a uniform moment bound for small divisors in shifted intervals. For Corollary 1.3, an additional difficulty is that the exact term $1/m$ must survive every operation that lengthens the expansion.

Formalization scope

• The goal uses OAI.ShortEgyptian: expansions are List ℕ that are strictly increasing (Pairwise (· < ·)), with entries $\ge2$ and rational sum $a/b$; minLength a b is an sInf and maxMinLength b the maximum over $1\le a<b$. The existence conjunct guarantees that sInf is taken over a nonempty set, so the bounds cannot hold through a junk value.
• The Problem337 milestones use Fin k → ℕ tuples (StrictMono, entries $\ge2$ for $a/b$ and $\ge1$ for expansions of $1$); $F(k)$ is Set.ncard, and $v(k)$ is sInf of the missing denominators. Finiteness of $D_k$ and of the expansion sets, which make these values meaningful, are separate statements in the proposal. In Corollary 1.3 the slopes are real liminf/limsup, accompanied by the explicit eventual bounds.
• Logarithms are Real.log; all constants are existential, apart from the explicit $600$, $257/\log 2$ and $\log2$ of the source.
• Needed infrastructure: divisor-counting and residue-distribution estimates, elementary prime-number bounds (the counting corollary uses the prime number theorem), and finite probabilistic constructions. Contributions proving the elementary pieces are welcome.

Selected references

• M. Nakayama, On the decomposition of a rational number into "Stammbrüche", Tohoku Math. J. 46 (1940). https://www.jstage.jst.go.jp/article/tmj1911/46/0/46_0_1/_article/-char/en
• P. Erdős, Az $1/x_1+1/x_2+\dots+1/x_n=a/b$ egyenlet egész számú megoldásairól, Mat. Lapok (1950). https://users.renyi.hu/~p_erdos/1950-02.pdf
• P. Erdős and R. L. Graham, Old and New Problems and Results in Combinatorial Number Theory, 1980. https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf
• T. F. Bloom, Erdős Problem 304. https://www.erdosproblems.com/304
• M. D. Vose, Egyptian fractions, Bull. London Math. Soc. 17 (1985). https://doi.org/10.1112/blms/17.1.21
• G. Tenenbaum and H. Yokota, Length and denominators of Egyptian fractions, III, J. Number Theory (1990). https://doi.org/10.1016/0022-314X(90)90109-5
• S. V. Konyagin, Double exponential lower bound for the number of representations of unity by Egyptian fractions, Mat. Zametki (2014). https://doi.org/10.4213/mzm10417
• C. Elsholtz and S. Planitzer, Sums of four and more unit fractions and approximate parametrizations, Bull. London Math. Soc. (2021). https://doi.org/10.1112/blms.12452
• W. van Doorn and Q. Tang, The smallest denominator not contained in a unit fraction decomposition of 1 with fixed length, Math. Proc. Cambridge Philos. Soc. (2026). https://doi.org/10.1017/S0305004126102102
• OpenAI, Short Egyptian fractions, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2; Corollaries 1.2–1.3, p. 3; Lemma 7.2, p. 26; Proposition 8.1, p. 27). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Short-Egyptian-fractions-September-25-2026/Short-Egyptian-fractions-September-25-2026.pdf

Motivation

Let $\Omega(n)$ count the prime factors of $n$ with multiplicity and let $\lambda(n)=(-1)^{\Omega(n)}$ be the Liouville function. Chowla's conjecture (1965) predicts that $\lambda$ behaves like a random sign sequence: its correlations along any fixed collection of distinct shifts have average tending to zero. The two-point case asks whether $n$ and $n+h$ have the same parity of prime-factor count as often as different parity. It is the multiplicative analogue of the twin prime problem and a central test case for the parity barrier in sieve theory. Elliott's conjecture extends the question to bounded multiplicative functions; Matomäki, Radziwiłł and Tao showed that for complex functions it needs a correction, uniform nonpretentiousness against all twists $\chi(n)n^{it}$.

There are two natural averages: the ordinary average $\frac1X\sum_{n\le X}a(n)$ and the logarithmic average $\frac1{\log X}\sum_{n\le X}a(n)/n$. Logarithmic averaging blends many scales; an ordinary estimate must control the terminal scale itself.

Background

• 1965. Chowla formulates his conjecture. 1971. Halász's mean-value theorem isolates the twists $n^{it}$ as the obstruction for one-point means.
• 1992. Elliott extends the correlation problem to bounded multiplicative functions.
• 2007. Granville and Soundararajan develop the pretentious distance $\mathbb D$ (doi:10.1090/S0894-0347-06-00536-4).
• 2015–2016. Matomäki and Radziwiłł prove short-interval mean-value theorems and a nontrivial bound $1-\delta(h)$ for each two-point Liouville correlation (doi:10.4007/annals.2016.183.3.6); Matomäki, Radziwiłł and Tao prove an averaged form of Chowla and formulate the corrected Elliott condition (doi:10.2140/ant.2015.9.2167).
• 2016. Tao proves the logarithmically averaged two-point Chowla and corrected Elliott conjectures, including affine forms (doi:10.1017/fmp.2016.6).
• 2019. Tao and Teräväinen obtain ordinary binary cancellation outside a set of scales of logarithmic density zero (doi:10.2140/ant.2019.13.2103).
• 2021, 2026. Helfgott and Radziwiłł obtain a quantitative logarithmic bound via divisibility-graph expansion (arXiv:2103.06853); Pilatte improves it to $(\log x)^{1-c_0}$ (doi:10.1090/jams/1084).
• 2023, 2026. Klurman, Mangerel and Teräväinen relax the nonpretentiousness hypothesis along a full-density set of scales (arXiv:2304.05344); Tao and Teräväinen obtain logarithmic savings for affine Liouville correlations outside a controlled exceptional set of scales (arXiv:2512.01739).

The source of this mission is an OpenAI preprint dated September 24, 2026, which treats ordinary averages at every cutoff.

Setting

• $\lambda(n)=(-1)^{\Omega(n)}$ for $n\ge1$.
• A function $f:\mathbb N\to\mathbb C$ is multiplicative if $f(mn)=f(m)f(n)$ for coprime positive $m,n$, and one-bounded if $|f(n)|\le1$.
• For a Dirichlet character $\chi$, $t\in\mathbb R$ and $X\ge2$, the pretentious distance is

$$\mathbb D(f,\chi n^{it};X)^2=\sum_{p\le X}\frac{1-\operatorname{Re}\bigl(f(p)\overline{\chi(p)}p^{-it}\bigr)}{p}.$$

• $f$ is uniformly nonpretentious if $\inf_{|t|\le N}\mathbb D(f,\chi n^{it};N)\to\infty$ as $N\to\infty$, for every fixed $\chi$.
• Two affine forms $a_1n+b_1$, $a_2n+b_2$ with $a_i\ge1$, $b_i\ge0$ are nonproportional if $a_1b_2\ne a_2b_1$.

Formalization targets

Goal: Theorem 1.1 (logarithmic saving for affine Liouville correlations)

There is an absolute $c>0$ such that for all nonproportional affine forms there is $C=C_{a_1,a_2,b_1,b_2}$ with

$$\Bigl|\sum_{1\le n\le X}\lambda(a_1n+b_1)\lambda(a_2n+b_2)\Bigr|\le C\,\frac{X}{(\log X)^c}\qquad(X\ge3).$$

With $a_1=a_2=1$, $b_1=0$, $b_2=h>0$ this is the ordinary two-point Chowla conjecture with a logarithmic saving.

Milestones

• Theorem 1.2. If $f_1,f_2$ are multiplicative and one-bounded and one of them is uniformly nonpretentious, then $\frac1N\sum_{n=1}^Nf_1(n+h_1)f_2(n+h_2)\to0$ for distinct $h_1,h_2\ge0$.
• Corollary 1.3. The same conclusion for $f_1(a_1n+b_1)f_2(a_2n+b_2)$ along nonproportional affine forms.

The goal OAI.OrdinaryTwoPointCorrelations.liouville_log_saving is open on the platform.

Significance

Theorem 1.1 removes the logarithmic weight and the exceptional scales from earlier two-point results: the bound holds at every cutoff, with an exponent independent of the forms. Theorem 1.2 does the same qualitatively for all one-bounded multiplicative functions satisfying the Matomäki–Radziwiłł–Tao corrected condition, without complete multiplicativity, unimodularity or real values. The implied constants need not be effective, and no uniformity in growing coefficients is claimed.

The results are proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

Partial summation turns ordinary cancellation into logarithmic cancellation, but not conversely, so Tao's entropy-decrement method and its descendants do not reach ordinary averages: they need to average over scales. Short-interval estimates give cancellation for most shifts or most scales, not for a fixed shift at every scale. The proof works at the terminal scale through multiplicative dilations, which lead to a divisor graph with edge displacement $hd$; one must bound high traces of the associated operator (closed walks, nonbacktracking moments, prohibited paths, triangular arithmetic savings) with weights matched to ordinary averaging, and in Part I convert this into an explicit logarithmic saving using bounded independence for Boolean circuits.

Formalization scope

• liouville n is ArithmeticFunction.liouville n cast to ℂ; affineSum f g a₁ a₂ b₁ b₂ N sums over n ∈ Finset.Icc 1 N, and the bound is applied at N = ⌊X⌋₊ for real X ≥ 3, with (Real.log X) ^ c as Real.rpow.
• Multiplicative asks the identity only for coprime positive arguments; OneBounded only for positive arguments in this source group.
• UniformlyNonpretentious is stated as: for every q > 0, every χ : DirichletCharacter ℂ q and every K, eventually in N, every t with |t| ≤ N has squared distance at least K. This is equivalent to (1.2).
• The second formalization of Theorem 1.2 (namespace OrdinaryCorrelations) uses the sInf form of (1.2) and is included as a reference item.

A complete development needs prime sums and Mertens-type estimates, Dirichlet characters, short-interval mean-value theorems (Matomäki–Radziwiłł–Tao, Theorem 4.3 here), Fourier bounds for rough integers, and the graph-trace machinery. Contributions formalizing Proposition 2.1 (quantitative correlations in every progression), Theorem 5.4 (the nonbacktracking moment), Proposition 10.1 (divisor graph estimate), Lemma 18.5 (uniform nonpretentiousness of Liouville) or the cited Theorem 4.3 are welcome.

Selected references

• OpenAI, Ordinary two-point correlations of multiplicative functions, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Ordinary-two-point-correlations-of-multiplicative-functions-September-24-2026/final.pdf
• K. Matomäki, M. Radziwiłł, T. Tao, An averaged form of Chowla's conjecture, Algebra Number Theory, 2015. https://doi.org/10.2140/ant.2015.9.2167
• K. Matomäki, M. Radziwiłł, Multiplicative functions in short intervals, Ann. of Math., 2016. https://doi.org/10.4007/annals.2016.183.3.6
• T. Tao, The logarithmically averaged Chowla and Elliott conjectures for two-point correlations, Forum Math. Pi, 2016. https://doi.org/10.1017/fmp.2016.6
• T. Tao, J. Teräväinen, The structure of correlations of multiplicative functions at almost all scales, Algebra Number Theory, 2019. https://doi.org/10.2140/ant.2019.13.2103
• H. A. Helfgott, M. Radziwiłł, Expansion, divisibility and parity, preprint, 2021. https://arxiv.org/abs/2103.06853
• C. Pilatte, Improved bounds for the two-point logarithmic Chowla conjecture, J. Amer. Math. Soc., 2026. https://doi.org/10.1090/jams/1084
• O. Klurman, A. P. Mangerel, J. Teräväinen, On Elliott's conjecture and applications, preprint, 2023. https://arxiv.org/abs/2304.05344
• A. Granville, K. Soundararajan, Large character sums: pretentious characters and the Pólya–Vinogradov theorem, J. Amer. Math. Soc., 2007. https://doi.org/10.1090/S0894-0347-06-00536-4

Motivation

Catalan's constant

$$G=\sum_{j=0}^{\infty}\frac{(-1)^j}{(2j+1)^2}=1-\frac1{9}+\frac1{25}-\frac1{49}+\cdots=0.9159655\ldots$$

is the value $\beta(2)=L(2,\chi_{-4})$ of the Dirichlet $L$-function of the odd quadratic character of conductor 4. It appears throughout analysis, combinatorics (dimer and spanning-tree constants), and geometry (volumes of hyperbolic 3-manifolds). For odd $s$, $\beta(s)$ is a rational multiple of $\pi^s$; the even values $\beta(2),\beta(4),\ldots$ are, like $\zeta(3),\zeta(5),\ldots$, among the basic special values whose arithmetic nature was unknown. Whether $G$ is irrational had long been a well-known question.

Timeline

• 1979. Apéry proves $\zeta(2)$ and $\zeta(3)$ irrational by recurrences whose integer linear forms tend to zero; Beukers gives integral proofs (doi:10.1112/blms/11.3.268).
• 2003. Rivoal and Zudilin prove that infinitely many even $\beta$-values are irrational, and that at least one of $\beta(2),\beta(4),\ldots,\beta(14)$ is (doi:10.1007/s00208-003-0420-2). Zudilin constructs Apéry-like recurrences, a continued fraction and integrals for $G$, and observes that their integer linear forms do not tend to zero (doi:10.37236/1707).
• 2006–2008. Rivoal connects Padé approximation to the hypergeometric construction and proves its denominator conjectures; Krattenthaler and Rivoal give a more direct proof (doi:10.1007/s11139-006-6507-0, arXiv:0810.1927).
• 2016. Nesterenko develops half-integer hypergeometric approximations and double Euler integrals for $G$ (doi:10.1134/S0081543816010107).
• 2017. Zudilin proposes a determinantal criterion for irrationality and explains why it does not yet apply to $G$ (doi:10.1007/s00365-016-9333-7).
• 2019–2022. Zudilin, then Lai and Zhou, shrink the finite list of even $\beta$-values known to contain an irrational one; Fischler proves quantitative results for families of Dirichlet $L$-values (doi:10.1112/jlms.12290); Viola reports improved approximation exponents (doi:10.4171/OWR/2022/21).
• 2005, 2024. Calegari proves irrationality of a 2-adic analogue of $G$ (doi:10.1155/IMRN.2005.1235); Calegari, Dimitrov and Tang prove linear independence of $1,\zeta(2),L(2,\chi_{-3})$, the conductor-3 analogue (arXiv:2408.15403).
• 2026. Eskandari constructs improved rational approximations (arXiv:2609.26354); Sun announces a proof of irrationality (arXiv:2609.04176).

The source of this mission is an OpenAI preprint dated September 24, 2026.

Setting

$G$ is the sum of the alternating series of reciprocals of odd squares displayed above. A real number $x$ is irrational if $x\neq p/q$ for all integers $p$ and $q\neq0$. No other definitions are involved.

Formalization targets

Goal: Theorem 1.1

$$G=\sum_{j\ge0}\frac{(-1)^j}{(2j+1)^2}\ \notin\ \mathbb Q.$$

The Lean statement OAI.InternalCatalan.catalan_irrational is open on the platform.

Significance

Theorem 1.1 settles the irrationality of an individual even Dirichlet $\beta$-value, which family results (Rivoal–Zudilin, Fischler) could not single out. The paper deduces (Section 8) irrationality of the minimal volume of an orientable complete finite-volume hyperbolic 3-manifold with exactly two cusps (Agol 2010 identified this volume as $4G$, doi:10.1090/S0002-9939-10-10364-5) and of certain arithmetic hyperbolic volumes. The argument is qualitative: it gives no irrationality measure.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. A formal proof would certify a long argument that combines exact finite certificates (rational matrices, rational trial coefficients) with analytic and $p$-adic estimates.

Difficulty

The standard route needs nonzero integer linear forms $A_mG-B_m\to0$. Many constructions give rational approximations $B_m/A_m\to G$ quickly, but clearing denominators destroys the decay: this is exactly the obstruction Zudilin identified for his Apéry-like recurrences, and approximation exponents below 1 (Viola–Marcovecchio, Eskandari) do not overcome it. The paper replaces linear forms by growing determinants $\Delta_N$ of size $48N$ built from moments that are rational combinations of $1$, $G$ and $\zeta(2)$; one must cancel the $\zeta(2)$ term exactly, bound denominators prime by prime (including two layers at large odd primes), prove nonvanishing along a sequence of primes via a finite certificate, and obtain a real-place upper bound sharp enough that the normalized limits $\liminf L_N>-2.29084$ and $\limsup L_N\le-2.290939875$ are incompatible. The margin between these constants is about $10^{-4}$.

Formalization scope

• The statement uses only Mathlib: Irrational and tsum over ℕ. The series is absolutely summable, so tsum agrees with the classical sum.
• The factor $2j+1$ is a natural number cast to ℝ; there are no partial operations.

A complete development needs: Chebyshev polynomial rows and their moments; $p$-adic valuations of the determinant entries and the prime number theorem in the weighted form used (Mathlib's PNT development may be reused); a Frobenius reduction and verified finite certificates for nonvanishing; Andréief's identity, Hardy-space interpolation and Hadamard bounds for the real estimate; and certified rational arithmetic for the final constants. Contributions formalizing Proposition 2.2 (cancellation and rationality), Proposition 3.4 (finite-place bound), Proposition 4.1 (nonvanishing at prime scales), Propositions 5.2–5.3 (interpolation and Hadamard estimates) and Proposition 7.1 (real-place bound) are welcome.

Selected references

• OpenAI, Catalan's constant is irrational, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Catalans-constant-is-irrational-September-24-2026/paper.pdf
• T. Rivoal, W. Zudilin, Diophantine properties of numbers related to Catalan's constant, Math. Ann., 2003. https://doi.org/10.1007/s00208-003-0420-2
• W. Zudilin, An Apéry-like difference equation for Catalan's constant, Electron. J. Combin., 2003. https://doi.org/10.37236/1707
• W. Zudilin, A determinantal approach to irrationality, Constr. Approx., 2017. https://doi.org/10.1007/s00365-016-9333-7
• T. Rivoal, Nombres d'Euler, approximants de Padé et constante de Catalan, Ramanujan J., 2006. https://doi.org/10.1007/s11139-006-6507-0
• Yu. V. Nesterenko, On Catalan's constant, Proc. Steklov Inst. Math., 2016. https://doi.org/10.1134/S0081543816010107
• S. Fischler, Irrationality of values of L-functions of Dirichlet characters, J. London Math. Soc., 2020. https://doi.org/10.1112/jlms.12290
• F. Calegari, V. Dimitrov, Y. Tang, The linear independence of 1, ζ(2), and L(2,χ_{−3}), preprint, 2024. https://arxiv.org/abs/2408.15403
• F. Beukers, A note on the irrationality of ζ(2) and ζ(3), Bull. London Math. Soc., 1979. https://doi.org/10.1112/blms/11.3.268
• I. Agol, The minimal volume orientable hyperbolic 2-cusped 3-manifolds, Proc. Amer. Math. Soc., 2010. https://doi.org/10.1090/S0002-9939-10-10364-5

Motivation

The Riemann zeta function $\zeta(s) = \sum_{n\ge1} n^{-s}$ ($\Re s > 1$), continued meromorphically to $\mathbb{C}$, encodes the distribution of primes through its zeros. Riemann (1859) conjectured that all nontrivial zeros lie on $\Re s = 1/2$. Hadamard and de la Vallée Poussin (1896) proved there are no zeros on $\Re s = 1$, which gives the prime number theorem, but all classical zero-free regions shrink toward the line $\Re s = 1$ as the height grows. The quasi-Riemann hypothesis asks for a fixed $\sigma_0 < 1$ such that $\zeta(s) \ne 0$ for all $\Re s > \sigma_0$: one zero-free gap valid at every height. The uniform version for all Dirichlet $L$-functions is a standard formulation in analytic number theory (e.g. Friedlander–Goldston).

This preprint claims a proof with $\sigma_0 = 7/8$, for $\zeta$, for all Dirichlet $L$-functions, and for all finite-order Hecke $L$-functions over $\mathbb{Q}(\sqrt{-3})$.

Background

• 1837. Dirichlet introduces character $L$-series to prove infinitude of primes in arithmetic progressions.
• 1859. Riemann relates zeros of $\zeta$ to primes and formulates the Riemann hypothesis.
• 1896. Hadamard and de la Vallée Poussin prove $\zeta(s) \ne 0$ on $\Re s = 1$.
• 1918. Hecke develops $L$-functions of characters over number fields.
• 1969, 1977. Kubota's metaplectic theory and Patterson's cubic theta series supply the automorphic objects used here.
• 2000–2014. Heath-Brown's cubic large sieve; Goldmakher–Louvel's quadratic large sieve over number fields; Blomer–Goldmakher–Louvel's higher-order recursion.
• 2026. Guth and Maynard improve zero-density bounds for $\zeta$ (which bound the number of zeros but do not exclude them). The OpenAI preprint The Quasi-Riemann Hypothesis (dated September 30, 2026) claims the zero-free half-plane $\Re s > 7/8$. It has not been peer reviewed or independently verified; the Lean goal is open on this platform. The Riemann hypothesis itself is not claimed.

Setting

For a Dirichlet character $\chi$ modulo $q$ (extended by zero on non-units), $L(s,\chi) = \sum_{n \ge 1}\chi(n) n^{-s}$ for $\Re s > 1$, continued meromorphically; the character modulo $1$ gives $\zeta$. For $F = \mathbb{Q}(\sqrt{-3})$ with ring of integers $\mathcal{O}$, a finite-order Hecke character modulo a nonzero ideal $\mathfrak{f}$ is a character of the ray class group modulo $\mathfrak f$, extended by zero, and $L_F(s,\eta) = \sum_{\mathfrak a \ne 0}\eta(\mathfrak a)(N\mathfrak a)^{-s}$. Principal characters have a pole at $s = 1$.

In Lean, $\zeta$ is Mathlib's riemannZeta, Dirichlet $L$-functions are Mathlib's DirichletCharacter.LFunction, and the Hecke family is OAI.SevenEighths.HeckeFamily.LFunction: a Character is a multiplicative character of $\mathcal O/\mathfrak m$ trivial on units (for this class-number-one field these are exactly the ray class characters), and its $L$-function is a lattice sum over $\mathcal{O} = \mathbb{Z}[\omega]$ divided by the $6$ units, continued through a theta-type functional equation pair.

Formalization targets

Goal: Theorem 1.1 for $\zeta$ (quasi-Riemann hypothesis)

$$\Re s > 7/8 \implies \zeta(s) \ne 0 .$$

Milestone: Theorem 1.1 for Dirichlet $L$-functions

For every Dirichlet character $\chi$ modulo $q \ge 1$ and every $s$ with $\Re s > 7/8$, $L(s,\chi) \ne 0$, except at the pole $s = 1$ of a principal character.

Milestone: Theorem 1.1 for Hecke $L$-functions over $\mathbb{Q}(\sqrt{-3})$

For every finite-order Hecke character $\eta$ of $F = \mathbb{Q}(\sqrt{-3})$ and every $s$ with $\Re s > 7/8$, $L_F(s,\eta) \ne 0$, except at the pole $s = 1$ of a principal character.

The three statements are ordered from weakest to strongest; the proof in the preprint goes through the whole Hecke family even for $\zeta$, because Poisson summation introduces Hecke twists of the target.

Significance

The result. A fixed zero-free half-plane would give power-saving error terms in the prime number theorem and in prime counts in arithmetic progressions, uniformly in the modulus, and would exclude Siegel zeros beyond $7/8$. The preprint derives (Corollary 1.2) that the least quadratic nonresidue modulo $p$ is $O((\log p)^A)$, proving Vinogradov's conjecture, and a deterministic polynomial-time square-root algorithm modulo primes.

Formalizing it. This is a claimed resolution of a long-standing question in an unrefereed preprint; a machine-checked proof would be strong independent verification. The goal uses only Mathlib definitions, so it cannot be weakened by a definitional choice. The Hecke milestone uses a custom $L$-function definition that must also be checked against the source.

Difficulty

Classical zero-free regions come from positivity arguments (the $3 + 4\cos\theta + \cos 2\theta$ inequality) that give regions of width $c/\log(|t|+q)$ shrinking to the line $\Re s = 1$; they cannot produce a fixed half-plane. Zero-density estimates bound the number of zeros to the right of a line but do not exclude every zero. The preprint instead continues reciprocals $1/L$ across a uniform distance by comparing two exact representations of a completed cubic-theta sum, with exponent margins independent of the target character.

Formalization scope

• The goal: ∀ s : ℂ, 7/8 < s.re → riemannZeta s ≠ 0. Mathlib assigns $\zeta(1)$ a finite nonzero value, so no pole exclusion is needed.
• The Dirichlet milestone excludes exactly the case χ = 1 ∧ s = 1, where Mathlib's value is a junk value at the pole.
• The Hecke milestone excludes χ.residue = 1 ∧ s = 1.
• The boundary $\Re s = 7/8$ is not included.

The goal is not vacuous and cannot be satisfied by a convention: it is a statement about Mathlib's riemannZeta on an open half-plane.

Needed infrastructure: Hecke $L$-functions over imaginary quadratic fields and their functional equations, cubic and sextic residue symbols, Patterson's cubic theta coefficients, large sieve inequalities over $\mathbb{Z}[\omega]$, and Mellin inversion. Contributions toward the $11/12$ half-plane (Theorem 3.1) as an intermediate target are welcome.

Selected references

• OpenAI, The Quasi-Riemann Hypothesis, OpenAI Math Release preprint, September 30, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/paper.pdf
• B. Riemann, Ueber die Anzahl der Primzahlen unter einer gegebenen Grösse, Monatsber. Königl. Preuss. Akad. Wiss. Berlin (1859).
• J. Hadamard, Sur la distribution des zéros de la fonction ζ(s) et ses conséquences arithmétiques, Bull. Soc. Math. France 24 (1896).
• E. Hecke, Eine neue Art von Zetafunktionen und ihre Beziehungen zur Verteilung der Primzahlen, Math. Z. 1 (1918).
• J. B. Friedlander, D. A. Goldston, Sums of three or more primes, Trans. Amer. Math. Soc. 349 (1997).
• K. Billington, M. Cheng, J. Schettler, A. I. Suriajaya, The average number of Goldbach representations and zero-free regions of the Riemann zeta-function, Int. J. Number Theory 21 (2025).
• S. J. Patterson, A cubic analogue of the theta series, J. Reine Angew. Math. 296 (1977).
• D. R. Heath-Brown, Kummer's conjecture for cubic Gauss sums, Israel J. Math. 120 (2000). https://doi.org/10.1007/s11856-000-1273-y
• V. Blomer, L. Goldmakher, B. Louvel, L-functions with n-th-order twists, IMRN 2014.
• L. Guth, J. Maynard, New large value estimates for Dirichlet polynomials, Ann. of Math. 203 (2026). https://doi.org/10.4007/annals.2026.203.2.6
• T. Tao, The Elliott–Halberstam conjecture implies the Vinogradov least quadratic nonresidue conjecture, Algebra Number Theory 9 (2015).

Why add-with-carry generators

Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number generators (Ann. Appl. Probab. 1 (1991)), introduced the add-with-carry and subtract-with-borrow generators. They keep $r$ machine words plus one carry bit, use only additions or subtractions of words, and still reach periods such as $2^{640}$ when the base $b$ is near $2^{32}$ (p. 465). The paper's mechanism for this is number-theoretic: the generated digits are the base-$b$ digits of a fraction $k/m$ written backwards, so the period of the generator is the period of a repeating base-$b$ expansion, i.e. the multiplicative order of $b$ modulo $m$.

Generators of this family were used widely in the following decades (Lüscher's RANLUX generator in lattice field theory is built on subtract-with-borrow), and later work showed that they are equivalent to linear congruential generators with modulus $m$ (Tezuka, L'Ecuyer and Couture 1993). This mission treats the add-with-carry generator. A companion mission treats subtract-with-borrow.

Setting

Fix a base $b \ge 2$ and two lags $r$ and $s$ with $0 < s < r$. A state (or seed vector) is

$$x = (x_1, x_2, \dots, x_r, c),$$

where each $x_i \in \{0, 1, \dots, b-1\}$ is a base-$b$ digit and $c \in \{0, 1\}$ is the carry bit. The digit $x_1$ is the oldest one. The add-with-carry map $f$ (p. 465) is

$$f(x_1, \dots, x_r, c) = \begin{cases} (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c,\ 0) & \text{if } x_{r+1-s} + x_1 + c < b,\\ (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c - b,\ 1) & \text{if } x_{r+1-s} + x_1 + c \ge b, \end{cases}$$

and the generated sequence of a seed $x$ is $x, f(x), f^2(x), \dots$. Reading off the last digit of each state gives a digit stream $x_1, \dots, x_r, x_{r+1}, x_{r+2}, \dots$ obeying $x_n = x_{n-r} + x_{n-s} + c \bmod b$, with the carry updated at each step. The two trivial seeds are $(0, \dots, 0, 0)$ and $(b-1, \dots, b-1, 1)$. The modulus of the generator is

$$m = b^r + b^s - 1 .$$

For $0 \le k < m$ and $j \ge 1$, the $j$-th base-$b$ digit of $k/m$ after the point is $d_j(k/m) = \lfloor b \cdot (b^{j-1} k \bmod m) / m \rfloor$. The order $\operatorname{ord}_m(b)$ is the least $p \ge 1$ with $b^p \equiv 1 \pmod m$, and $b$ is a primitive root of a prime $m$ when $\operatorname{ord}_m(b) = m - 1$.

Formalization targets

Goal: the period is the order of $b$

Let $m = b^r + b^s - 1$ be prime, and let $x$ be any seed other than the two trivial seeds. Then $f^r(x)$ is a periodic point of $f$ and

$$\min\{p \ge 1 : f^{p}(f^{r}(x)) = f^{r}(x)\} = \operatorname{ord}_m(b).$$

This is the italic summary of p. 472 ("whatever the seed vector, except for the two trivial seeds, the add-with-carry and subtract-with-borrow sequences become periodic after a few iterations of the generating function, and the periods are the order of the base $b$ for the appropriate modulus"), with the claim of §4.2 (p. 467) and its proof (p. 468). The goal fixes no particular $b$, $r$, $s$ and does not assume that $b$ is a primitive root. When it is, the period is $b^r + b^s - 2$, the value announced in §2.

Milestones

1. §4.1 (p. 467): for $\gcd(k, m) = \gcd(b, m) = 1$, $p > 0$ is a period of the base-$b$ expansion of $k/m$ iff $\operatorname{ord}_m(b) \mid p$.
2. §4.1 (p. 467): if $b$ is a primitive root of the prime $m$, every proper fraction $k/m$ has least period $m - 1$.
3. p. 472: $f(x) = x$ iff $x$ is a trivial seed.
4. p. 472: $f^r(x)$ is periodic for every seed.
5. §4.2 (p. 468): for every seed other than $(b-1, \dots, b-1, 1)$ and every $C$, there is $0 \le k < m$, positive iff the seed is nonzero, with

$$x_n = d_{C+1-n}(k/m) \qquad (r + 1 \le n \le C).$$

6. p. 472, Method 3: $x$ is periodic iff $c = 0$ and $x_r \cdots x_{s+1} \ge x_{r-s} \cdots x_1$, or $c = 1$ and $x_r \cdots x_{s+1} \le x_{r-s} \cdots x_1$ (digit strings read as base-$b$ integers).
7. §2 (p. 465): the instance $b = 10$, $r = 2$, $s = 1$, period $108$.
8. §7 (p. 477): the instance $b = 6$, $r = 21$, $s = 2$, period $6^{21} + 6^2 - 2$.

Significance

The result. The goal reduces the period of the generator, a property of a dynamical system on $2b^r$ states, to the multiplicative order of one residue. That is the computation the paper performs in §6 to certify its recommended generators, and it is how one chooses $b, r, s$: search for primes $m = b^r + b^s - 1$ and check the order of $b$. Milestone 5 is stronger than the goal. It needs no primality and identifies the whole output stream, not only its period, with the expansion of a fraction. That identification is what later work used to relate carry generators to linear congruential generators with modulus $m$. Milestone 6 answers the paper's "periodic seed" puzzle: it says exactly which seeds lie on their own cycle.

Formalizing it. The results are proved in the paper, the general §4.1 facts are classical, and the method-specific rules of §4.5 (milestone 6) are stated there without proof. None of it is machine-checked on Prove2Me or, to our knowledge, in Mathlib, which has orderOf and ZMod but no theory of base-$b$ expansions of rationals. The mission produces a checked link from a concrete integer recurrence to modular arithmetic. That link can serve as a template for other carry-based and lagged generators.

Difficulty

The obvious argument says the digit recurrence is linear, so the period divides something like the order of a companion matrix. This fails because of the carry: $f$ is not linear over $\mathbb{Z}/b$, and the state $(x_1, \dots, x_r, c)$ does not live in a group in any evident way. The link to the order of $b$ modulo $m$ goes through an identity between a finite digit string and a fraction (milestone 5). Stating it with exact indices is itself delicate: the digits run in reverse order, the fraction depends on the string's length, and the trivial seed $(b-1, \dots, b-1, 1)$, whose digits are those of $m/m = 1$, has to be excluded.

A second difficulty is the preperiod. A seed need not lie on its own cycle (p. 472), so the period must be measured after the transient. Bounding that transient by $r$ (milestone 4) and characterising the periodic seeds (milestone 6) are separate combinatorial facts about the carry. The paper states the second without proof.

Formalization scope

• Representation. All declarations are in namespace CarryRNG.AWC. Lags are a structure Lags with fields r, s and proofs of $0 < s$ and $s < r$. A state is a structure with digits x : Fin r → Fin b and carry c : Fin 2, so $c \le 1$ holds by typing. Lean index $i$ is the paper's $x_{i+1}$: x 0 is $x_1$ (the digit the step drops), and the partner digit $x_{r+1-s}$ is index $r - s$. step is defined directly from the two-case formula of p. 465, not through $k/m$. The digit stream out is one-based: the seed digits for $n \le r$, then the last digit of $f^{\,n-r}(x)$. digit b m k j is the exact integer formula above, used for $j \ge 1$ only.
• Period. "The period" is Mathlib's Function.minimalPeriod. It is $0$ at non-periodic points, so the goal's equation with the positive $\operatorname{ord}_m(b)$ also asserts periodicity. A divisibility or inequality form would be vacuous and is not used. For digit sequences, "period $L$" is stated as "$p > 0$ is a period iff $L \mid p$".
• Quantifier readings. "With appropriately chosen base $b$, lags $r$ and $s$ and seed vector $x$" (p. 465) is read as: $m$ prime and $x$ not a trivial seed, following p. 468 ("Making $m$ a prime ensures this") and p. 472. "After a few iterations" is "after at most $r$", the paper's own bound (p. 472), so the goal is stated at $f^r(x)$. In milestone 5 the fraction $k$ depends on the length $C$ of the finite string, as in the paper's "arbitrarily long finite string". In milestone 8, "for any set of 21 seed digits" is stated at $f^{21}(x)$ for the same reason.
• Corrected misprints. p. 465 prints the second trivial seed as "(9, 9, 9)"; the last entry is the carry, so milestone 7 excludes $(9, 9, 1)$. p. 473, example (a), prints the Method 3 inequalities reversed; milestone 6 follows p. 472, which exhaustive checks on small parameters confirm. p. 478 repeats the die period with "− 1" for "− 2"; milestone 8 quotes p. 477.
• Ruled-out trivializations. The goal is not "some period divides $m - 1$" and not "every orbit is eventually periodic". Both hold for any self-map of a finite set or are vacuous. The trivial seeds are named states, not excluded by an assumption such as $f(x) \neq x$.
• Infrastructure and contributions. Needed: periods of base-$b$ expansions of rationals (milestones 1–2, reusable beyond this mission) and finite-dynamics facts about minimalPeriod along an orbit. Proofs of any milestone are welcome, as are primality and order certificates for milestone 8 as separate lemmas.

Selected references

• G. Marsaglia and A. Zaman, A new class of random number generators, Ann. Appl. Probab. 1(3) (1991), 462–480. https://doi.org/10.1214/aoap/1177005878
• S. Tezuka, P. L'Ecuyer and R. Couture, On the lattice structure of the add-with-carry and subtract-with-borrow random number generators, ACM Trans. Model. Comput. Simul. 3(4) (1993), 315–331. https://doi.org/10.1145/159737.159749
• R. Couture and P. L'Ecuyer, Distribution properties of multiply-with-carry random number generators, Math. Comp. 66 (1997), 591–607. https://doi.org/10.1090/S0025-5718-97-00827-2
• M. Lüscher, A portable high-quality random number generator for lattice field theory simulations, Comput. Phys. Commun. 79 (1994), 100–110. https://doi.org/10.1016/0010-4655(94)90232-1

Motivation

A lattice in $\mathbb R^n$ is the set of integer combinations of $n$ linearly independent vectors. Many problems in algorithmic number theory, cryptography and integer programming reduce to finding a short nonzero vector of a lattice, or a few short independent ones. Finding the shortest vector exactly is hard, but in 1982 A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász introduced a notion of reduced basis that can be computed in polynomial time and whose vectors are provably short up to a factor depending only on the dimension (Lenstra, Lenstra, Lovász 1982). Their paper used it to factor polynomials in $\mathbb Q[X]$ in polynomial time; the same reduction (now called LLL) became a standard tool for simultaneous Diophantine approximation (the paper's own (1.39)), for H. W. Lenstra's integer programming algorithm in fixed dimension (Lenstra 1983), and for cryptanalysis of knapsack and RSA variants.

What makes a reduced basis useful is a set of explicit inequalities proved in Section 1 of the paper, before any algorithm appears. They compare the lengths of the basis vectors with the lattice determinant and with arbitrary lattice vectors, with constants such as $2^{n-1}$ and $2^{n(n-1)/4}$. This mission formalizes those inequalities.

Setting

Let $n\ge1$ and let $(\,\cdot\,,\,\cdot\,)$ and $|\cdot|$ be the ordinary inner product and Euclidean length on $\mathbb R^n$. Vectors $b_1,\ldots,b_n\in\mathbb R^n$ form a basis for a lattice $L$ when they are linearly independent over $\mathbb R$ and $L=\sum_{i=1}^n\mathbb Z b_i$. The determinant of $L$ is

$$d(L)=|\det(b_1,b_2,\ldots,b_n)|,$$

the $b_i$ written as columns (1.1). The Gram–Schmidt vectors $b_i^*$ and coefficients $\mu_{ij}$ ($1\le j<i\le n$) are defined inductively by

$$b_i^*=b_i-\sum_{j=1}^{i-1}\mu_{ij}b_j^*,\qquad \mu_{ij}=\frac{(b_i,b_j^*)}{(b_j^*,b_j^*)}\qquad(1.2),(1.3);$$

the $b_i^*$ are pairwise orthogonal and not normalised. The basis is reduced if

$$|\mu_{ij}|\le\tfrac12\quad(1\le j<i\le n)\qquad(1.4)$$

and

$$|b_i^*+\mu_{i\,i-1}b_{i-1}^*|^2\ge\tfrac34|b_{i-1}^*|^2\quad(1<i\le n)\qquad(1.5).$$

The first condition is a size condition on the coefficients; the second (the Lovász condition) says that swapping $b_{i-1}$ and $b_i$ would not shrink the $(i-1)$-th Gram–Schmidt length by more than the factor $\frac34$ (pp. 516–517).

Formalization targets

Goal: Proposition (1.12), p. 518

Let $b_1,\ldots,b_n$ be a reduced basis for $L$ and let $x_1,\ldots,x_t\in L$ be linearly independent. Then

$$|b_j|^2\le 2^{n-1}\cdot\max\{|x_1|^2,|x_2|^2,\ldots,|x_t|^2\}\qquad (j=1,\ldots,t).$$

The statement quantifies over every reduced basis and every independent family of lattice vectors. Its case $t=1$ is Proposition (1.11).

Milestones

In the order of the paper's proofs (pp. 517–518):

1. $|b_i^*|^2\ge(\frac34-\mu_{i\,i-1}^2)|b_{i-1}^*|^2\ge\frac12|b_{i-1}^*|^2$ for $1<i\le n$ (proof of (1.6));
2. $|b_j^*|^2\le 2^{i-j}|b_i^*|^2$ for $1\le j\le i\le n$ (proof of (1.6));
3. $|b_i|^2=|b_i^*|^2+\sum_{j<i}\mu_{ij}^2|b_j^*|^2\le 2^{i-1}|b_i^*|^2$ (proof of (1.6));
4. (1.7): $|b_j|^2\le 2^{i-1}|b_i^*|^2$ for $1\le j\le i\le n$;
5. if $x=\sum_l r_lb_l$ with $r_l\in\mathbb Z$ and $i$ is the largest index with $r_i\ne0$, then $|x|^2\ge|b_i^*|^2$ (proof of (1.11), reused as (1.13));
6. (1.11): $|b_1|^2\le 2^{n-1}|x|^2$ for every nonzero $x\in L$.

Companion statements

The rest of Proposition (1.6) and the remark after it: $d(L)=\prod_i|b_i^*|$ (proof of (1.6)); (1.8) $d(L)\le\prod_i|b_i|\le 2^{n(n-1)/4}d(L)$; (1.9) $|b_1|\le 2^{(n-1)/4}d(L)^{1/n}$; and Hadamard's inequality (1.10) $d(L)\le\prod_i|b_i|$ for an arbitrary basis.

Significance

Proposition (1.11) says the first vector of a reduced basis approximates a shortest nonzero lattice vector within the factor $2^{(n-1)/2}$; (1.12) extends this to all of the first $t$ basis vectors, so that $|b_j|^2$ is within $2^{n-1}$ of the $j$-th successive minimum of $L$ (the remark after (1.12)). These are the guarantees on which the paper's factoring algorithm rests: in Section 2 a reduced basis of a lattice built from a $p$-adic factor yields, through (1.11) and (1.12), an irreducible factor of the polynomial. Inequality (1.9) gives simultaneous Diophantine approximation in polynomial time, and (1.8) bounds how far a reduced basis is from orthogonal.

All of these results are proved in the paper and in textbooks. Verified LLL developments exist in Isabelle/HOL (Bottesch et al., A verified LLL algorithm, AFP 2018), but Mathlib, the library this platform builds on, has neither the reduced-basis predicate of (1.4)–(1.5) nor these bounds. A Lean development produces a reusable definition layer for lattices with the paper's conventions, Gram–Schmidt length estimates, and Hadamard's inequality in determinant form, which the other missions of this series (the reduction algorithm and the factoring application) build on.

Difficulty

The estimates on Gram–Schmidt lengths are single-variable inductions once (1.5) has been rewritten using orthogonality. The step that does not follow from a direct estimate is (1.12): the vectors $x_1,\ldots,x_t$ are arbitrary independent lattice vectors with no relation to the basis order, so a bound on each $|x_j|$ by a single Gram–Schmidt length does not by itself say which $b_j$ it controls. A naive argument that pairs $x_j$ with $b_j$ fails. The determinant statements need the link between Mathlib's matrix determinant of the columns $b_i$ and the Gram–Schmidt lengths, which Mathlib does not state in this form.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) (abbreviated Vec n), a basis is a family b : Fin n → Vec n, the lattice is Submodule.span ℤ (Set.range b), and "basis for $L$" is linear independence over $\mathbb R$ together with equality of that span with $L$. The vectors $b_i^*$ are Mathlib's unnormalised InnerProductSpace.gramSchmidt, and $\mu_{ij}$ is (1.3) verbatim. $d(L)$ is the absolute determinant of the column matrix; it is not defined as $\prod|b_i^*|$, which would make the first companion statement true by definition. Section 1 begins "Let $n$ be a positive integer", so every statement carries $0<n$.

Lean indices run from $0$ to $n-1$: the paper's $b_i$ is Lean's b ⟨i-1, _⟩, an exponent $2^{i-1}$ at paper index $i$ is $2^i$ at Lean index $i$, and the pair $(i-1,i)$ of (1.5) is $(i,i+1)$. Exponents $n(n-1)/4$, $(n-1)/4$ and $1/n$ are real powers. The maximum in (1.12) is a Finset.sup' over the nonempty index set of the $x_j$, and the statement is empty at $t=0$, as on the page.

Every statement about a reduced basis also assumes linear independence: the reducedness inequalities alone hold for degenerate dependent families, whose Gram–Schmidt vectors vanish, and would make the targets trivial. The goal does not assume (1.7), (1.13) or any ordering of the $x_j$; those appear only as milestones. Proofs of the milestones and companions, and general lemmas on Gram–Schmidt and determinants that would belong in Mathlib, are welcome.

Selected references

• A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261, 515–534, 1982. https://doi.org/10.1007/BF01457454
• H. W. Lenstra, Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4), 538–548, 1983. https://doi.org/10.1287/moor.8.4.538
• R. Bottesch, J. Divasón, M. Haslbeck, S. Joosten, R. Thiemann, A. Yamada, A verified LLL algorithm, Archive of Formal Proofs, 2018. https://www.isa-afp.org/entries/LLL_Basis_Reduction.html