Number Theory

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Salikhov's bound.

Formalization target

The campaign template with the value $7.606309$ filled in: PiIrrationality.UpperBound (7.606309 : ℝ), i.e. $\mu(\pi) \le 7.606309$.

Value. The bound is quoted as $7.606308\ldots$ (e.g. by Zeilberger–Zudilin), a truncation. This entry rounds the last digit up to $7.606309$.

How the bound arises

Salikhov uses integrals of rational functions that are symmetric under a group of transformations (in the spirit of Rhin–Viola), which gives larger arithmetic savings in the common denominators than Hata's construction.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $7.606309$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• V. Kh. Salikhov, On the irrationality measure of $\pi$, Russian Math. Surveys 63 (2008), no. 3, 570–572.
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Hata's bound.

Formalization target

The campaign template with the value $8.016046$ filled in: PiIrrationality.UpperBound (8.016046 : ℝ), i.e. $\mu(\pi) \le 8.016046$.

Value. The paper computes the exponent as $7.016045\ldots + 1$ and states the rounded bound $8.0161$. This entry rounds the computed value's last digit up to $8.016046$, which is still below the paper's $8.0161$ and above $8.016045\ldots$.

How the bound arises

Hata obtains simultaneous approximations to $1, \pi, \log 2$ from complex contour integrals of Legendre type, with extra arithmetic savings from primes that divide the coefficients to a predictable extent. His linear-form measure is $7.016045\ldots$, giving $\mu(\pi) \le 8.016045\ldots$ (stated in the paper as $8.0161$). It stood as the record for about fifteen years.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $8.016046$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• M. Hata, Rational approximations to $\pi$ and some other numbers, Acta Arith. 63 (1993), no. 4, 335–349. http://matwbn.icm.edu.pl/ksiazki/aa/aa63/aa6344.pdf
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

Integer programming asks whether a system of linear inequalities $Ax\le b$ has a solution $x\in\mathbb Z^n$. In fixed dimension $n$ it is solvable in polynomial time: Lenstra (1983) proved this by showing that a convex body without integer points is "flat" in some integral direction, so that the search splits into few lower-dimensional subproblems. Kannan's 1987 paper in Mathematics of Operations Research sharpened this approach. It computes a Korkine–Zolotarev ("reduced") basis of a lattice, solves the shortest and closest vector problems exactly in $n^{O(n)}$ operations, and runs integer programming in $O(n^{9n/2}s)$ arithmetic operations. Underneath the algorithm sits a purely geometric statement, Theorem (5.5): a lattice-free convex body meets only boundedly many integer translates of some integral subspace.

Timeline.

• Korkine and Zolotareff (1873): the reduced bases used here.
• Minkowski (1896): a symmetric convex body of volume greater than $2^n$ contains a nonzero integer point.
• Khinchine (1948): lattice-free convex bodies have lattice width bounded by a function of $n$ alone (the flatness theorem).
• Lenstra (1983): integer programming in fixed dimension is polynomial, via a flat direction.
• Kannan (1987, this paper): Theorem (5.5), with subspaces $V$ of any dimension between $1$ and $n-1$ and an explicit bound $n^{2(n-\dim V)}$.
• Kannan and Lovász (1988), Banaszczyk et al. (1999), and later work: polynomial bounds on the flatness constant.

Setting

$\mathcal R^n$ is Euclidean space with dot product $(a,b)$ and length $|a|$, and $\mathbb Z^n$ is the set of integer vectors. For linearly independent $b_1,\dots,b_m\in\mathcal R^k$, the lattice $L(b_1,\dots,b_m)$ is the set of integer combinations $\sum_j\lambda_jb_j$, $\lambda_j\in\mathbb Z$, and $b_1,\dots,b_m$ is a basis. Gram–Schmidt orthogonalisation gives $b_1^*,\dots,b_m^*$ and unit vectors $u_j=b_j^*/|b_j^*|$, and $b_i(j)=(b_i,u_j)$, so $b_i=\sum_jb_i(j)u_j$ and $b_j(j)=|b_j^*|$. The determinant is $d(L)=\prod_j|b_j^*|$. $\Lambda_1(L)$ is the length of a shortest nonzero vector of $L$. The projected lattice $L_j(b_1,\dots,b_m)$ is the image of $L$ under orthogonal projection onto the complement of $\operatorname{span}(b_1,\dots,b_{j-1})$. A basis is reduced (Definition 2.6) if $b_j(j)=\Lambda_1(L_j)$ for every $j$ and $|b_i(j)|\le b_j(j)/2$ for $i>j$.

A convex body is a convex set of positive volume, which for a convex set means nonempty interior. A subspace $V$ has a basis of integer vectors if it is the real span of integer vectors. Its integer translates are the sets $z+V$ with $z\in\mathbb Z^n$.

In Lean, $\mathcal R^k$ is EuclideanSpace ℝ (Fin k), a basis is b : Fin m → EuclideanSpace ℝ (Fin k), the lattice is lattice b = Submodule.span ℤ (Set.range b), $|b_j^*|$ is gsLen b j, $b_i(j)$ is gsCoeff b i j, $d(L)$ is latticeDet b, $\Lambda_1$ is lambdaOne, $L_{j+1}$ is projLattice b j, and a reduced basis is IsReduced b.

Formalization targets

Goal: Theorem (5.5), corrected reading

For $n\ge2$ and every bounded convex set $K\subseteq\mathcal R^n$ with nonempty interior and $K\cap\mathbb Z^n=\emptyset$ there is a subspace $V$ spanned by integer vectors with $1\le\dim V\le n-1$ and

The printed theorem allows "an $i$ dimensional space $V$" with $1\le i\le n$ and bound $n^{2(n-i+1)}$. Taken literally that is trivial ($V=\mathcal R^n$, one translate). The proof on the same page takes $V=\operatorname{span}(b_1,\dots,b_{i-1})$, of dimension $i-1$, and remarks that this "ensures that the subspace $V$ is always of dimension at least 1". The goal states that reading.

Milestones

1. Theorem (1.11), Minkowski's convex body theorem (referenced from the platform, in Mathlib's general form).
2. Theorem (1.12): every $m$-dimensional lattice has a nonzero vector with $|v|\le\sqrt m\,d(L)^{1/m}$.
3. Proposition 1.9: a primitive lattice vector belongs to some basis.
4. Proposition 2.16, existence form: every lattice has a reduced basis.
5. Proposition 4.2: for any $b_0$ with projection $\bar b_0$ onto the span, some $b\in L$ has $|b-\bar b_0|\le\frac12(\sum_jb_j(j)^2)^{1/2}\le\frac{\sqrt m}2\max_jb_j(j)$.
6. Proposition 4.3: for a reduced basis and $i$ maximising $b_i(i)$, the tail $(\lambda_i,\dots,\lambda_m)$ of every closest lattice point to $b_0$ lies in an explicit set of at most $m^{m-i+1}$ integer vectors.

Significance

Theorem (5.5) is a structural form of the flatness theorem. For $\dim V=n-1$ it says that a lattice-free convex body meets fewer than $n^2$ consecutive integer hyperplanes of some integral direction. For smaller $\dim V$ it gives a finer decomposition of $\mathbb Z^n$ into translates, each a lower-dimensional integer program. This is the recursion behind fixed-dimension integer programming, and statements of this form are used in lattice-point enumeration, in the geometry of numbers (covering minima), and in cutting-plane theory (lattice-free bodies define split and intersection cuts). Propositions 4.2 and 4.3 are the correctness core of exact closest-vector enumeration.

The results are proved in the literature, though Theorem (5.5) is proved "albeit sketchily" in the paper itself. As far as is known, none of them is formalized: Mathlib has Minkowski's convex body theorem and the ZLattice API, but not Gram–Schmidt lattice invariants, Korkine–Zolotarev bases, Hermite-type bounds, nearest-plane rounding, or any flatness theorem. This mission produces the first machine-checked versions. It also corrects three statements that are wrong as printed (below), so the formal statements are the ones that can be relied on.

Difficulty

The naive route to (5.5) is to take a flat direction directly: bound the lattice width of $K$ and count hyperplanes. That needs a flatness theorem with an explicit bound below $n^2$, which is itself the hard part. The paper's argument instead needs John's theorem (every convex body lies between an ellipsoid and its $n$-fold dilation), a reduced basis of the transformed lattice, and a counting argument across projected lattices that combines Minkowski's bound on each $L_i$ with the covering estimate of Proposition 4.2. None of John's theorem, reduced bases or the projected-lattice counting is in Mathlib.

Proposition 4.3 is also delicate as printed: the per-coordinate count on p. 24 undercounts the integers in a closed interval, so the printed arithmetic cannot be transcribed as it stands. Proposition 2.16 in the paper is the correctness of the algorithm SHORTEST. Here only the existence of a reduced basis is needed, which requires attainment of $\Lambda_1$ on every projected lattice and a lifting argument (Proposition 1.9).

Formalization scope

Conventions: indices are 0-based (Fin m), so the paper's $L_j$ is projLattice b (j-1) and its bound $n^{n-i+1}$ is m ^ (m - i). Gram–Schmidt is Mathlib's unnormalised gramSchmidt. Lattices are Submodule ℤs of a real Euclidean space generated by a linearly independent family, and $m\le k$ is allowed, because (1.12) and 4.2 are applied to projected lattices. The goal counts translates as sets with Set.encard, so the bound includes finiteness. $K$ is assumed convex, bounded and with nonempty interior, but not closed.

Three printed statements are corrected, and the corrections are recorded in each item's Formalization Note.

• (1.12)'s constant $\frac12\sqrt n$ is false for $n\le7$ (for example $L=\mathbb Z$, or the hexagonal lattice) and is replaced by $\sqrt n$, the constant the paper's own later proofs use.
• Proposition 4.2's second sentence is stated for $\bar b_0$ instead of $b_0$.
• Proposition 4.3 fails at $n=1$ and is stated for $m\ge2$ with the proof's explicit candidate set $T$, since an existential $T$ is satisfied by the set of tails of closest points and says nothing.

Trivializing formalizations are ruled out: the goal forbids $\dim V=n$, which gives one translate, and $\dim V=0$, where no translate meets $K$. It requires nonempty interior (the empty set would satisfy everything) and counts with encard (an infinite count cannot become $0$).

Out of scope: the paper's algorithms (SHORTEST, SELECT-BASIS, ENUMERATE, CLP, CLP′, ILP) and their operation and bit counts (Theorems 2.17, 3.9, 4.5, 5.4), because Mathlib has no cost model. Also out of scope is §6 (NP-completeness of the $L_2$ closest vector problem and Cook reductions), because Mathlib has no complexity classes. The definitions of this mission (lattice, gsLen, gsCoeff, latticeDet, lambdaOne, projLattice, IsReduced) are reusable for any later work on lattice reduction. Contributions are welcome at every level: John's theorem, Hermite-type bounds, Korkine–Zolotarev existence, and the counting lemmas.

Selected references

• R. Kannan, Minkowski's Convex Body Theorem and Integer Programming, Mathematics of Operations Research 12(3):415–440, 1987. https://doi.org/10.1287/moor.12.3.415
• 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. Kannan, L. Lovász, Covering minima and lattice-point-free convex bodies, Annals of Mathematics 128(3):577–602, 1988. https://doi.org/10.2307/1971436
• 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
• F. John, Extremum problems with inequalities as subsidiary conditions, Studies and Essays presented to R. Courant, 1948, 187–204.

Motivation

A set of integers is a Sidon set if all of its pairwise sums $a+b$ ($a\le b$) are different. Sidon, in connection with Fourier analysis, asked how dense such sets can be, and the question became one of the standard problems of additive combinatorics. Let

A counting argument shows $h(N)\le (1+o(1))\sqrt{2N}$, and the true order was settled early: $h(N)\sim\sqrt N$. What remains open is the size of the error term $h(N)-\sqrt N$. Erdős and Turán asked whether it is smaller than every power of $N$; Erdős offered $1000 for this problem (Erdős Problem #30), and it is also Problem 31 on Green's list of open problems and problem C9 in Guy's Unsolved Problems in Number Theory.

Timeline.

• 1938 — Singer constructs, for every prime power $q$, a set of $q+1$ residues modulo $q^2+q+1$ with all differences distinct. Combined with the density of primes this gives $h(N)\ge(1-o(1))\sqrt N$ (Singer 1938).
• 1941 — Erdős and Turán prove $h(N)\le N^{1/2}+O(N^{1/4})$ (Erdős–Turán 1941).
• 1969 — Lindström gives an alternative proof with the explicit bound $h(N)\le N^{1/2}+N^{1/4}+1$ (Lindström 1969).
• 2021 — Balogh, Füredi and Roy lower the constant: $h(N)\le N^{1/2}+0.998N^{1/4}$ for large $N$ (arXiv:2103.15850).
• 2022 — O'Bryant: $h(N)\le N^{1/2}+0.99703N^{1/4}$ for large $N$ (arXiv:2207.07800).
• 2023 — Carter, Hunter and O'Bryant: $h(N)\le N^{1/2}+0.98183N^{1/4}+O(1)$, with substantial computer assistance (arXiv:2310.20032).

No upper bound with an error exponent below $1/4$ is known, and no lower bound of the form $h(N)\ge\sqrt N-O(N^{\varepsilon})$ for every $\varepsilon>0$ is known either.

Setting

A set $A$ in an additive commutative monoid is Sidon if for all $i_1,j_1,i_2,j_2\in A$,

For a finite set $X$, $\operatorname{maxSidon}(X)$ is the largest size of a Sidon subset of $X$ (the empty set is Sidon, so this is well defined), and

The first values are $h(1),\dots,h(15)=1,2,2,3,3,3,4,4,4,4,4,5,5,5,5$ (OEIS A143824).

Formalization targets

Goal (Erdős Problem #30)

This is a two-sided statement: it asks both for an upper bound $h(N)\le\sqrt N+C_\varepsilon N^\varepsilon$ and for a matching lower bound $h(N)\ge\sqrt N-C_\varepsilon N^\varepsilon$ for large $N$. Erdős asked it as a yes/no question; the goal fixes the conjectured answer yes, so a disproof on the platform settles the question negatively.

Milestones (known results, weakest to strongest)

1. Singer's construction: $h(q^2+q+1)\ge q+1$ for every prime power $q$.
2. Singer's lower bound: $h(N)\ge(1-\varepsilon)\sqrt N$ for every $\varepsilon>0$ and all large $N$.
3. Erdős–Turán / Lindström: $h(N)\le\sqrt N+N^{1/4}+1$ for all $N$.
4. Balogh–Füredi–Roy: $h(N)\le\sqrt N+0.998N^{1/4}$ for all large $N$.
5. O'Bryant: $h(N)\le\sqrt N+0.99703N^{1/4}$ for all large $N$.
6. Carter–Hunter–O'Bryant: $h(N)\le\sqrt N+0.98183N^{1/4}+C$ for an absolute constant $C$.

Significance

The result itself. An affirmative answer would pin $h(N)$ down to $\sqrt N$ up to a sub-polynomial error, in both directions; Erdős even speculated that $h(N)=\sqrt N+O(1)$ might hold, while remarking that this is perhaps too optimistic. A negative answer would show that the Singer-type constructions or the counting upper bounds are off by a power of $N$. Either answer would be the first change in the exponent of the error term since 1941.

Formalizing it. The goal is open. All milestones are published theorems. The platform already contains weaker related results in other formalizations (for example the order-of-magnitude bounds $c\sqrt N\le \max|A|\le\sqrt{2N}+1$ for Sidon subsets of an initial segment, and the Erdős–Turán construction); the sharp bounds listed as milestones are not stated there for this $h$. The upper bounds of Balogh–Füredi–Roy and O'Bryant are elementary but delicate optimizations, and the Carter–Hunter–O'Bryant bound relies on a large computation, so formalizing it is a substantial verification task in its own right.

Difficulty

For the upper bound, every known argument counts differences $a-a'$ in short windows and loses at the scale $N^{1/4}$; improvements since 1941 only change the constant in front of $N^{1/4}$. For the lower bound, the constructions (Singer, Bose, Ruzsa) produce Sidon sets of size about $\sqrt p$ in a modulus $p$ of size about $N$, and the loss comes from the gap between $N$ and the nearest admissible modulus; bringing it below $N^\varepsilon$ requires either new constructions or information about primes in very short intervals that is far beyond current knowledge.

Formalization scope

Sidon sets are formalized for sets in an arbitrary additive commutative monoid, with the definition, the decidability instance and $\operatorname{maxSidon}$ transcribed from the formal-conjectures library (definitions IsSidon, Finset.maxSidonSubsetCard, and Erdos30.h in FormalConjectures/ErdosProblems/30.lean), placed in the namespace Erdos30. The value $h(N)$ is a natural number cast to $\mathbb R$; $\sqrt{\cdot}$ is the real square root and $N^{\varepsilon}$, $N^{1/4}$ are real powers of $N\ge 0$. The goal's $O(\cdot)$ is Mathlib's Asymptotics.IsBigO along atTop on $\mathbb N$. The goal is not trivialized by any junk value: $h$ is a genuine finite maximum, and the $O(\cdot)$ statement concerns all large $N$.

Useful infrastructure: basic lemmas on Sidon sets (hereditary under subsets, translation invariance, distinct differences), finite projective geometry or Bose's construction for the lower bounds, and prime gaps (Bertrand's postulate suffices for $h(N)\ge c\sqrt N$ with $c<1$; a prime number theorem in short intervals is needed for $1-o(1)$). Contributions of reusable Sidon-set lemmas are welcome.

Selected references

• J. Singer, A theorem in finite projective geometry and some applications to number theory, Trans. Amer. Math. Soc. 43 (1938), 377–385. https://doi.org/10.1090/S0002-9947-1938-1501951-4
• P. Erdős and P. Turán, On a problem of Sidon in additive number theory, and on some related problems, J. London Math. Soc. 16 (1941), 212–215. https://doi.org/10.1112/jlms/s1-16.4.212
• B. Lindström, An inequality for $B_2$-sequences, J. Combin. Theory 6 (1969), 211–212. https://doi.org/10.1016/S0021-9800(69)80124-9
• J. Balogh, Z. Füredi and S. Roy, An upper bound on the size of Sidon sets, Amer. Math. Monthly (2023). https://arxiv.org/abs/2103.15850
• K. O'Bryant, On the size of finite Sidon sets (2022). https://arxiv.org/abs/2207.07800
• D. Carter, Z. Hunter and K. O'Bryant, On the diameter of finite Sidon sets (2023). https://arxiv.org/abs/2310.20032
• K. O'Bryant, A complete annotated bibliography of work related to Sidon sequences, Electron. J. Combin. DS11 (2004). https://arxiv.org/abs/math/0407117
• T. F. Bloom, Erdős Problem #30, https://www.erdosproblems.com/30
• Google DeepMind, formal-conjectures, FormalConjectures/ErdosProblems/30.lean. https://github.com/google-deepmind/formal-conjectures

Motivation

Which sets of positive integers are forced to contain long arithmetic progressions? Van der Waerden (1927) showed that in any finite colouring of $\mathbb N$ some colour class does; Erdős and Turán (1936) asked for a density version, which became Szemerédi's theorem. Erdős then proposed the strongest natural size condition: divergence of the reciprocal sum. Erdős Problem #3 (erdosproblems.com/3) asks whether every $A\subseteq\mathbb N$ with $\sum_{n\in A}1/n=\infty$ contains arbitrarily long arithmetic progressions. Erdős attached one of his largest prizes to it. The primes are the motivating example: $\sum_p 1/p=\infty$, so a positive answer would contain the Green–Tao theorem.

Timeline.

• 1936 — Erdős and Turán conjecture that sets of positive density contain arbitrarily long progressions.
• 1953 — Roth proves the case $k=3$ of the density conjecture by Fourier analysis.
• 1975 — Szemerédi proves the density conjecture for all $k$.
• 2001 — Gowers gives the first quantitative bounds for all $k$: $r_k(N)\ll N/(\log\log N)^{c_k}$.
• 2008 — Green and Tao prove that the primes contain arbitrarily long progressions.
• 2020 — Bloom and Sisask prove $r_3(N)\ll N/(\log N)^{1+c}$, which settles the case $k=3$ of Erdős Problem #3.
• 2023 — Kelley and Meka prove $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
• 2024 — Leng, Sah and Sawhney prove $r_k(N)\le N\exp(-(\log\log N)^{c_k})$ for every $k\ge5$.

The problem is open for every $k\ge4$.

Setting

A set $S\subseteq\mathbb N$ is an arithmetic progression of length $k$ if $|S|=k$ and $S=\{a,a+d,\dots,a+(k-1)d\}$ for some $a,d\in\mathbb N$ (for $k\ge2$ the size condition forces $d>0$). For $k,N\in\mathbb N$, $r_k(N)$ denotes the largest size of a subset of $\{1,\dots,N\}$ containing no arithmetic progression of length $k$. A set $A$ has divergent reciprocal sum if $\sum_{n\in A}1/n=\infty$.

Formalization targets

Goal (Erdős Problem #3)

For every $A\subseteq\mathbb N$,

This is the formal-conjectures statement erdos_3 with its answer(sorry) instantiated to the conjectured answer yes. A disproof of the goal on the platform settles the problem negatively.

Milestones

• Szemerédi's theorem for sets of positive upper density (the density case), and the existing platform statement $r_k(N)=o(N)$.
• The Green–Tao theorem (the case $A=$ primes).
• The Bloom–Sisask bound on $r_3(N)$ and its corollary, the case $k=3$ of the goal; the Kelley–Meka bound (existing platform statement).
• The Leng–Sah–Sawhney bound for $k\ge5$.
• The partial-summation reduction: bounds $r_k(N)\le N/(\log N)^{1+c_k}$ for all $k\ge3$ imply the goal.

Significance

A positive answer would be a common strengthening of Szemerédi's theorem and the Green–Tao theorem, obtained from a single size condition with no arithmetic structure. Through the reduction milestone, it is closely tied to the quantitative theory of $r_k(N)$: bounds of the shape $N/(\log N)^{1+c}$ for every $k$ would suffice. Formalizing the milestones would also give reusable Lean statements of Szemerédi-type theorems in a common language.

Difficulty

Divergence of $\sum 1/n$ is a very weak condition: such sets can have density zero, and the natural approach through $r_k(N)$ requires bounds just past $N/\log N$. For $k=3$ this barrier was only broken in 2020. For $k\ge4$ the best known bounds (Leng–Sah–Sawhney) save only a power of $\log\log N$ in the exponent, far from what is needed. The Green–Tao method uses pseudorandom majorants specific to the primes and does not apply to arbitrary sets.

Formalization scope

All statements import the published definition file Erdos142Basic, which reproduces the formal-conjectures definitions IsAPOfLengthWith, IsAPOfLength and the counting function r k N (over $\{1,\dots,N\}$). The reciprocal-sum hypothesis is ¬ Summable (fun a : A ↦ 1 / (a : ℝ)); the element $0$, if present, contributes $1/0=0$. "Arbitrarily long" is written as ∃ᶠ k in atTop, which is equivalent to "every length" because sub-progressions of progressions are progressions. Bounds stated in the literature with $\ll$ are written without a multiplicative constant and with "for all sufficiently large $N$"; the constant can be absorbed into the exponent. Contributions formalizing partial summation over sets of naturals and the equivalence of the "frequently" and "for every $k$" forms are welcome.

Selected references

• P. Erdős and P. Turán, On some sequences of integers, J. London Math. Soc. 11 (1936).
• K. F. Roth, On certain sets of integers, J. London Math. Soc. 28 (1953).
• E. Szemerédi, On sets of integers containing no k elements in arithmetic progression, Acta Arith. 27 (1975).
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal. 11 (2001).
• B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Ann. of Math. 167 (2008).
• T. F. Bloom and O. Sisask, Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions, arXiv:2007.03528 (2020).
• Z. Kelley and R. Meka, Strong bounds for 3-progressions, FOCS 2023, arXiv:2302.05537.
• J. Leng, A. Sah and M. Sawhney, Improved bounds for Szemerédi's theorem, arXiv:2402.17995 (2024).
• T. F. Bloom, Erdős Problem #3, https://www.erdosproblems.com/3

Motivation

A set $A$ of positive integers is pairwise coprime if $\gcd(a,b)=1$ for all distinct $a,b\in A$. The primes are the model example, and a recurring theme in Erdős's combinatorial number theory is that pairwise coprime sets cannot do much better than the primes on natural additive or harmonic statistics. Erdős Problem 1210 asks for a sharp version of this principle for the harmonic weight $1/(n-a)$, which measures how densely a coprime set can crowd the point $n$ from below.

Timeline.

• 1977. In [Er77c, p.64] Erdős posed a question about the primes $q_1<\dots<q_k$ in an interval $(n,m]$: is $\sum_i 1/(q_i-n)<\sum_{p<m-n}1/p+O(1)$?
• 1980. In [Er80, p.112] he wrote that he had "not stated [this] quite correctly" in [Er77c] and posed the question for arbitrary pairwise coprime sets $A\subseteq[1,n)$, which is the form recorded as Problem 1210.
• 2026. On the erdosproblems.com forum, a reduction to a counting bound for $A\cap[n-x,n)$ was suggested; it was then observed that this counting bound would itself imply an open inequality of the type $\pi(x+y)\le\pi(x)+\pi(y)+O(y/(\log y)^2)$ (compare Problem 855). The problem remains open.

Setting

Fix a natural number $n$. Consider finite sets $A$ of integers with $1\le a<n$ for every $a\in A$, and with $\gcd(a,b)=1$ for all distinct $a,b\in A$. For such a set define the reciprocal gap sum

Every term is at most $1$, and the element $a=n-d$ contributes $1/d$. Write $\sum_{p<n}1/p$ for the sum of reciprocals of the primes below $n$; by Mertens' theorem it equals $\log\log n+O(1)$. Throughout, $\pi(x)$ denotes the number of primes $p\le x$.

Target

The goal of the mission is the affirmative answer to Problem 1210: there is an absolute constant $C$ such that

for every $n$ and every pairwise coprime $A\subseteq[1,n)$. A negative answer is equally welcome and is recorded by disproving the goal statement.

The milestones are:

1. Small prime factors. For pairwise coprime $A$, at most $\pi(x)$ elements of $A\cap[n-x,n)$ have a prime factor $\le x$.
2. Partial summation reduction. If $|A\cap[n-x,n)|\le\pi(x)+O(x/(\log x)^2)$ uniformly, then the goal holds.
3. The [Er77c] variant. For the primes $q_i$ in $(n,m]$, $\sum_i 1/(q_i-n)<\sum_{p<m-n}1/p+O(1)$.

Significance

The result itself. An affirmative answer would say that, for the weight $1/(n-a)$, no pairwise coprime set beats the primes by more than a constant, and would give a quantitative form of the heuristic that coprime sets behave like sets of primes near a point. A negative answer would exhibit coprime sets that concentrate near $n$ more efficiently than the primes do in the harmonic sense. The [Er77c] variant concerns only primes, and relates the distribution of primes just above $n$ to the primes below the interval length $m-n$.

Formalizing it. Neither the goal nor the [Er77c] variant is known. The mission produces Lean statements checked against the source, a reduction (milestone 2), to be verified in Lean, that isolates exactly which counting estimate would suffice, and the elementary coprimality lemma (milestone 1). These pin down what a proof or disproof must supply.

Difficulty

The natural first attempt splits $A\cap[n-x,n)$ into elements with a prime factor $\le x$, of which there are at most $\pi(x)$, and $x$-rough elements, and then hopes that sieve bounds make the rough part $O(x/(\log x)^2)$. The obstruction is that $A$ may contain many primes in $[n-x,n)$. Bounding the number of primes in a short interval $[n-x,n)$ by $\pi(x)+O(x/(\log x)^2)$ is a form of the second Hardy–Littlewood conjecture $\pi(x+y)\le\pi(x)+\pi(y)$, which is open and known to be incompatible, in its exact form, with the prime $k$-tuples conjecture. So the counting route in milestone 2 needs input on primes in short intervals beyond current knowledge, and any proof of the goal must either supply such input or avoid pointwise counting.