Number Theory

Motivation: how large can a set avoid square differences?

A set $A\subseteq\{1,\dots,N\}$ is square-difference-free if no two of its elements differ by a perfect square $m^2$ with $m\ge1$. The Furstenberg–Sárközy theorem says such sets have density tending to zero; the question is how fast. Writing $s(N)$ for the largest size of a square-difference-free subset of $\{1,\dots,N\}$, the problem is a prototype for polynomial patterns in dense sets: it is the simplest case of finding differences in the image of a polynomial, and it is the model problem on which Fourier-analytic, ergodic and density-increment methods for polynomial configurations are tested. A long-standing gap separates the upper bounds, which until recently saved only a power of $\log N$ (with a slowly growing exponent), from the lower bounds, which are powers $N^{0.73\ldots}$ and beyond. Whether a fixed power saving $s(N)\le CN^{1-c}$ holds was posed explicitly by Green and Sawhney.

Background and timeline

• 1977–1978 — Answering a question of Lovász, Furstenberg (J. Analyse Math. 1977, Theorem 1.2) and Sárközy (Acta Math. Hungar. 1978) independently prove $s(N)=o(N)$; Sárközy's bound is $N/(\log N)^{1/3+o(1)}$.
• 1984 — Ruzsa constructs square-difference-free sets of size $\gg N^{0.7330\ldots}$ (Period. Math. Hungar. 1984).
• 1988 — Pintz, Steiger and Szemerédi prove $s(N)\ll N/(\log N)^{c\log\log\log\log N}$ (J. LMS 1988).
• 2008/2015 — Beigel and Gasarch (arXiv:0804.4892) and Lewko (Electron. J. Combin. 2015) improve the lower exponent to $0.7334\ldots$.
• 2022 — Bloom and Maynard prove $s(N)\ll N/(\log N)^{c\log\log\log N}$ (Compos. Math. 2022).
• 2024/2025 — Green and Sawhney prove $s(N)\ll N\exp(-c\sqrt{\log N})$ and ask for a fixed power saving (arXiv:2411.17448, Theorem 1.1 and §1.1).
• 2026 — Adajar et al. extend the arithmetic level-$d$ approach to intersective polynomials (arXiv:2605.16216); Krachun pushes the lower exponent past $3/4$, to $0.7527\ldots$ (arXiv:2608.01325).
• 2026 — The OpenAI preprint A power saving for square-difference-free sets (OpenAI Math Release, September 24, 2026) claims $s(N)\le CN^{1-c}$ with absolute constants. It has not been peer reviewed and its theorem is not formally verified.

Setting

For a positive integer $N$ write $[N]=\{1,\dots,N\}$. A set $A\subseteq[N]$ is square-difference-free if

$$(A-A)\cap\{m^2 : m\in\mathbb N,\ m\ge1\}=\varnothing,$$

that is, $a-b\neq m^2$ for all $a,b\in A$ and all integers $m\ge1$. (Differences are taken in $\mathbb Z$; $a-b=0$ is allowed since $0$ is excluded from the squares.)

In Lean (namespace OAI.SquareDifference), sets are Finset ℤ contained in Finset.Icc 1 N, and IsSquareDifferenceFree A states a - b ≠ (m : ℤ)^2 for all a b ∈ A and m : ℕ with 1 ≤ m.

Formalization targets

Goal: a fixed power saving (Theorem 1.1)

There are absolute constants $c>0$ and $C<\infty$ such that for every integer $N\ge1$ and every square-difference-free $A\subseteq[N]$,

$$|A|\le C\,N^{1-c}.$$

Equivalently, every subset of $[N]$ with more than $CN^{1-c}$ elements contains two elements differing by a nonzero perfect square. The Lean goal is published on the platform with status Open. The statement fixes no numerical value of $c$, so any improvement of the exponent leaves the goal unchanged.

Significance

The result itself. Every earlier upper bound saved less than any fixed power of $N$; the best, due to Green and Sawhney, saved $\exp(-c\sqrt{\log N})$. A fixed power saving changes the nature of the problem: it shows that the extremal exponent $\limsup \log s(N)/\log N$ lies strictly below $1$, so both upper and lower bounds are now polynomial and the remaining question is the value of the exponent, now known to lie between $0.7527\ldots$ and $1-c$. As an immediate consequence (Remark 1.2 of the source), the graph on $[N]$ joining integers differing by a square has chromatic number at least $C^{-1}N^c$, a polynomial bound for the square-difference coloring problem.

Formalizing it. The statement is elementary and self-contained, involving only finite sets of integers. The proof combines a graph/tuple reformulation, reflection-positivity (chessboard) inequalities for a finite-field probability law, and an induction with fixed finite constructions. A formal proof would certify an argument whose constants are explicitly noted to be extremely small and not computed.

Difficulty

Density-increment arguments, starting from Sárközy's circle-method proof, gain a constant factor of density at each step but lose a power of the length of the progression on which they pass, so after the $\log(1/\alpha)$ increments needed the saving is only logarithmic or quasi-logarithmic. The Green–Sawhney level-$d$ approach controls the relevant rational Fourier coefficients through hypercontractivity but still gives only $\exp(-c\sqrt{\log N})$. A power saving requires an argument whose loss does not compound with the number of iterations — a single estimate that converts square-difference-freeness into a polynomial density loss.

Formalization scope

• Sets are Finset ℤ inside Finset.Icc 1 N and $N\ge1$ is a natural number; the bound is uniform in $N$.
• The constants are existentially quantified before $N$ and $A$; $c>0$ is required and $C$ is a real number. The power $N^{1-c}$ is the real power.
• Differences $a-b$ are in $\mathbb Z$ and the excluded squares are $m^2$ with $m\ge1$, so only nonzero squares are forbidden; differences in either order are covered because both $a-b$ and $b-a$ are tested.
• Needed infrastructure: Fourier analysis on $\mathbb Z/p\mathbb Z$ and on $[N]$, reflection-positivity/chessboard estimates, and graph-norm inequalities. Reusable pieces include a chessboard-estimate library and finite-field Fourier tools.

Selected references

• H. Furstenberg, Ergodic behavior of diagonal measures and a theorem of Szemerédi on arithmetic progressions, J. Analyse Math. 31 (1977). https://doi.org/10.1007/BF02813304
• A. Sárközy, On difference sets of sequences of integers. I, Acta Math. Acad. Sci. Hungar. 31 (1978). https://doi.org/10.1007/BF01896079
• I. Z. Ruzsa, Difference sets without squares, Period. Math. Hungar. 15 (1984). https://doi.org/10.1007/BF02454169
• J. Pintz, W. L. Steiger and E. Szemerédi, On sets of natural numbers whose difference set contains no squares, J. London Math. Soc. 37 (1988). https://doi.org/10.1112/jlms/s2-37.2.219
• R. Beigel and W. Gasarch, Square-difference-free sets of size $\Omega(n^{0.7334\ldots})$, arXiv:0804.4892 (2008). https://arxiv.org/abs/0804.4892v3
• M. Lewko, An improved lower bound related to the Furstenberg–Sárközy theorem, Electron. J. Combin. 22 (2015). https://doi.org/10.37236/4656
• T. F. Bloom and J. Maynard, A new upper bound for sets with no square differences, Compos. Math. 158 (2022). https://doi.org/10.1112/S0010437X22007679
• B. Green and M. Sawhney, New bounds for the Furstenberg–Sárközy theorem, arXiv:2411.17448 (2025). https://arxiv.org/abs/2411.17448v2
• D. Krachun, Square-difference-free sets beyond the three-quarter barrier, arXiv:2608.01325 (2026). https://arxiv.org/abs/2608.01325v1
• OpenAI, A power saving for square-difference-free sets, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-power-saving-for-square-difference-free-sets-September-24-2026/paper.pdf

Motivation

A Hadamard matrix of order $n$ is an $n\times n$ matrix with entries $\pm1$ whose rows are mutually orthogonal, $HH^{\mathsf T}=nI_n$. Such matrices are extremal for Hadamard's determinant bound and are used throughout coding theory, experimental design and signal processing. Imposing a circulant structure, where every row is a cyclic shift of the first, links the problem to cyclic difference sets and to binary sequences with ideal periodic autocorrelation. The order-4 example with first row $(-1,1,1,1)$ is easy to find; the circulant Hadamard conjecture, traditionally attributed to Ryser (1963), asserts that apart from the trivial order 1 there are no others.

The question is closely tied to Barker sequences, binary sequences with the smallest possible aperiodic autocorrelations, which are used as radar pulse-compression codes. Only lengths $2,3,4,5,7,11,13$ are known, and the long-standing Barker-sequence conjecture says there are no others.

Timeline

• 1961. Turyn and Storer prove that Barker sequences of odd length greater than 13 do not exist, and relate even-length Barker sequences to vanishing periodic autocorrelations (doi:10.1090/S0002-9939-1961-0125026-2).
• 1963. Ryser's monograph Combinatorial Mathematics records the circulant Hadamard problem (doi:10.5948/UPO9781614440147).
• 1965. Turyn, using cyclotomic character sums, shows that any order greater than four must be $4u^2$ with $u$ odd and not a prime power (doi:10.2140/pjm.1965.15.319).
• 1999–2016. B. Schmidt's field descent (doi:10.1090/S0894-0347-99-00298-2) and the work of Leung and Schmidt (2005, 2012, 2016) give much stronger arithmetic restrictions (doi:10.1007/s10623-011-9493-1, doi:10.1016/j.jcta.2015.11.005).
• 2016. Schmidt and Willms give a new proof of the odd-length Barker classification (doi:10.1007/s10623-015-0104-4).
• 2017. Logan and Mossinghoff exclude all but 4,489 candidate orders $4<n\le4\cdot10^{30}$ using double Wieferich prime pairs.
• 2024. Steinerberger shows that approximately orthogonal sign circulants exist in every order (doi:10.1007/s10623-024-01430-w), so the exact equality is essential.

Several complete proofs have been claimed (Oh-Hashi 2016, Orozco López 2019, Morris 2023, Gallardo 2024, Manjhi–Kumar 2025). The source of this mission is an OpenAI preprint dated September 23, 2026, which proves the conjecture by an argument with cyclotomic character values over the group ring $\mathbb Z[i][C_{u^2}]$.

Setting

A real $n\times n$ matrix $H$ is circulant if there is a function $h:\mathbb Z/n\mathbb Z\to\mathbb R$ with $H_{ij}=h(j-i)$, indices taken modulo $n$. It is a sign Hadamard matrix if every entry is $1$ or $-1$ and

$$HH^{\mathsf T}=n\,I_n.$$

For a circulant sign matrix with first row $h$, the periodic autocorrelations are $P_h(t)=\sum_{j}h_jh_{j+t}$; the Hadamard condition says $P_h(t)=0$ for $1\le t<n$.

A Barker sequence of length $n$ is $a\in\{-1,1\}^n$ with aperiodic autocorrelations

$$C_a(t)=\sum_{j=0}^{n-t-1}a_ja_{j+t},\qquad |C_a(t)|\le1\quad(1\le t<n).$$

Formalization targets

Goal: Theorem 1.1

$$\text{For } n\ge1:\quad \exists\ \text{a real circulant Hadamard matrix of order } n\iff n\in\{1,4\}.$$

The Lean statement OAI.CirculantHadamard.exists_iff_order_one_or_four is open on the platform.

Milestone: Corollary 1.2, even case

$$a\in\{-1,1\}^n\ \text{Barker},\ n\ge1\ \text{even}\ \Longrightarrow\ n\in\{2,4\}.$$

Combined with the classical odd-length classification, this gives the Barker length list $\{2,3,4,5,7,11,13\}$.

Significance

Theorem 1.1 closes a problem open since the early 1960s and, through the even-length reduction, completes the classification of Barker-sequence lengths. Equivalently, it shows that cyclic difference sets with parameters $(4u^2,\,2u^2-u,\,u^2-u)$ exist only for $u=1$. It also explains, in a single statement, the computational evidence of Logan and Mossinghoff and the arithmetic restrictions of Turyn and of Leung–Schmidt.

The result is proved in an OpenAI preprint that has not been peer reviewed; given the number of earlier claimed proofs, an independent machine-checked proof would be especially valuable. No formal proof of either statement exists; the formalization would also produce reusable group-ring and cyclotomic machinery.

Difficulty

The orthogonality condition is a norm equation $hh^*=n$ in the group ring $\mathbb Z[C_n]$, and every character sends $h$ to a cyclotomic integer of absolute value $\sqrt n$. Classical arguments use such character values one at a time, through factorization of ideals in cyclotomic fields, and stop at the case $n=4u^2$ with $u$ odd and divisible by several primes. The obstruction must combine information from all prime divisors of $u$ simultaneously and use the fact that the coefficients are signs, not arbitrary integers; norm equations alone do have solutions at these orders.

Formalization scope

• RealMatrix n := Matrix (Fin n) (Fin n) ℝ; IsCirculant H asks for h : Fin n → ℝ with H i j = h (j - i), where subtraction in Fin n is modular.
• IsSignHadamard H is entrywise IsSign (equal to $1$ or $-1$) together with H * H.transpose = (n : ℝ) • 1.
• The goal assumes 0 < n, matching the paper's "positive integer $n$".
• The Barker milestone uses integer sequences Fin n → ℤ with IsSign entries and aperiodic h k = Σ_{j<n-k} h_j h_{j+k}, bounded by $1$ in absolute value for $0<k<n$.

A complete development needs group rings of finite cyclic groups, characters and cyclotomic integers, localization at primes above $p$, and Kronecker's theorem that an algebraic integer all of whose conjugates have absolute value one is a root of unity. Contributions formalizing Proposition 2.2 (the order restriction $n=4u^2$, $u$ odd), Lemma 3.1 (character comparison) and Proposition 3.4 (alternating character products are roots of unity of odd order) are welcome.

Selected references

• OpenAI, The circulant Hadamard conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-circulant-Hadamard-conjecture-September-23-2026/paper.pdf
• H. J. Ryser, Combinatorial Mathematics, Carus Mathematical Monographs, 1963. https://doi.org/10.5948/UPO9781614440147
• R. J. Turyn, Character sums and difference sets, Pacific J. Math., 1965. https://doi.org/10.2140/pjm.1965.15.319
• R. Turyn, J. Storer, On binary sequences, Proc. Amer. Math. Soc., 1961. https://doi.org/10.1090/S0002-9939-1961-0125026-2
• B. Schmidt, Cyclotomic integers and finite geometry, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00298-2
• K. H. Leung, B. Schmidt, New restrictions on possible orders of circulant Hadamard matrices, Des. Codes Cryptogr., 2012. https://doi.org/10.1007/s10623-011-9493-1
• K.-U. Schmidt, J. Willms, Barker sequences of odd length, Des. Codes Cryptogr., 2016. https://doi.org/10.1007/s10623-015-0104-4
• B. Logan, M. J. Mossinghoff, Double Wieferich pairs and circulant Hadamard matrices, J. Combin. Math. Combin. Comput., 2017.
• S. Steinerberger, A note on approximate Hadamard matrices, Des. Codes Cryptogr., 2024. https://doi.org/10.1007/s10623-024-01430-w

Motivation

Van der Waerden's theorem (1927) says that for every number of colours $r$ and every length $k$, every $r$-colouring of a long enough interval of integers contains a monochromatic arithmetic progression of length $k$. The van der Waerden number $W_r(k)$ is the least such interval length. Its upper bounds were for a long time not even primitive recursive (Shelah 1988 gave the first primitive recursive bound; Gowers 2001 gave a tower-type bound), while lower bounds stayed close to exponential, $W_2(k)\gtrsim 2^k$. Erdős asked whether $W_2(k)^{1/k}\to\infty$, i.e. whether the growth is genuinely faster than any exponential. Lower bounds on $W_r(k)$ correspond to long colourings with no monochromatic progression and are a central quantitative question in Ramsey theory.

Timeline

• 1927. Van der Waerden proves finiteness of $W_r(k)$.
• 1952 and 1962. Erdős–Rado (doi:10.1112/plms/s3-2.1.417) and Schmidt (doi:10.1215/S0012-7094-62-02914-9) obtain early exponential-type lower bounds.
• 1968. Berlekamp proves $W_2(p+1)>p\,2^p$ for primes $p$ by an algebraic construction (doi:10.4153/CMB-1968-047-7).
• 1975. Erdős and Lovász introduce the local lemma, a standard tool for such colourings.
• 1980. Erdős asks for $\lim_k W_2(k)^{1/k}=\infty$ (doi:10.1016/S0167-5060(08)70697-6).
• 1990. Szabó proves $W_2(k)\ge 2^k/k^{\varepsilon}$ (doi:10.1002/rsa.3240010307).
• 2016. Kozik and Shabanov prove $W_r(k)\ge\beta r^{k-1}$ uniformly (doi:10.1016/j.jctb.2015.09.004).
• 2025. Hunter improves the exponential base for fixed $r\ge5$ (doi:10.1007/s11856-025-2735-0).
• 2026. Fox and Hunter prove superexponential growth for three colours, $W_3(k)>2^{k\log^*k/4}$ (arXiv:2606.02541); Campos, Fox and Schildkraut prove $W_2(k)\ge(1-o(1))k2^{k-1}$ (arXiv:2608.20824).

For two colours, superexponential growth had not been established. The source of this mission, an OpenAI preprint dated September 23, 2026, claims a bound of the form $k^{ck\log r}$ uniformly in $r\ge2$.

Setting

For positive integers $r,k$, $W_r(k)$ is the least positive integer $N$ such that every map $\{1,\dots,N\}\to\{1,\dots,r\}$ is constant on some progression

$$a,\ a+d,\ \dots,\ a+(k-1)d,\qquad a,d\ge1,\quad a+(k-1)d\le N.$$

Colourings may use fewer than $r$ colours.

Formalization targets

Goal: Theorem 1.1

There is an absolute $K_0$ such that for every $k\ge K_0$ and every $r\ge2$,

$$W_r(k)\ >\ k^{\,c\,k\lfloor\log_2 r\rfloor},\qquad c=10^{-5}.$$

In particular $W_r(k)^{1/k}\to\infty$ for each fixed $r\ge2$. The constant $c$ is the paper's and is not optimized. The Lean statement OAI.QuantitativeVanDerWaerden.uniform_lower_bound is open on the platform.

Significance

The theorem gives a quantitative positive answer to Erdős's superexponential-growth question for two colours, and is stronger than the statement $W_2(k)/2^k\to\infty$ settled by Campos–Fox–Schildkraut. It is uniform in the number of colours with a single threshold $K_0$, which complements the Fox–Hunter bounds that require many colours relative to $k$. The bound is still far from the best upper bounds, which are tower-type.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would certify an explicit colouring construction together with a probabilistic (local-lemma) argument.

Difficulty

Random colourings with the local lemma give only $W_r(k)\gtrsim r^{k}/\mathrm{poly}(k)$: the number of $k$-term progressions in $[N]$ is of order $N^2$, and each is monochromatic with probability $r^{1-k}$, which caps the length at exponential size. Algebraic constructions such as Berlekamp's gain only a factor $p$. A superexponential bound needs colourings with structure that kills most progressions deterministically, while the remaining progressions are few enough to be destroyed randomly, uniformly down to two colours.

Formalization scope

• MonoAP c k a d: the colour of $a+jd$ equals the colour of $a$ for $j<k$; HasMonoAP c k N: some $d>0$ with $a+(k-1)d<N$.
• IsRamsey α k N: every colouring ℕ → α has a monochromatic $k$-AP in $\{0,\dots,N-1\}$ (equivalent to the paper's $[N]$ after a shift).
• W r k is the sInf of positive Ramsey $N$ for colours Fin r. If no such $N$ existed this would be $0$ and the goal's strict inequality would fail, so the goal implicitly includes van der Waerden's theorem.
• The exponent uses Nat.log 2 r $=\lfloor\log_2 r\rfloor$ and the real constant 1/100000.

A complete development needs van der Waerden's theorem (or at least finiteness), a finite asymmetric local lemma, and the paper's explicit adaptive-mesh colourings and counting of affine signatures. Contributions formalizing Lemma 4.1 (finite asymmetric local lemma) or Theorem 6.3 (a cyclic two-colouring) are welcome.

Selected references

• OpenAI, Quantitative Superexponential Bounds for van der Waerden Numbers, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026/paper.pdf
• P. Erdős, A survey of problems in combinatorial number theory, Ann. Discrete Math., 1980. https://doi.org/10.1016/S0167-5060(08)70697-6
• E. R. Berlekamp, A construction for partitions which avoid long arithmetic progressions, Canad. Math. Bull., 1968. https://doi.org/10.4153/CMB-1968-047-7
• Z. Szabó, An application of Lovász' local lemma: a new lower bound for the van der Waerden number, Random Structures Algorithms, 1990. https://doi.org/10.1002/rsa.3240010307
• J. Kozik, D. Shabanov, Improved algorithms for colorings of simple hypergraphs and applications, J. Combin. Theory Ser. B, 2016. https://doi.org/10.1016/j.jctb.2015.09.004
• J. Fox, Z. Hunter, Three-color van der Waerden numbers grow super-exponentially, preprint, 2026. https://arxiv.org/abs/2606.02541
• M. Campos, J. Fox, C. Schildkraut, A new lower bound for two-color van der Waerden numbers, preprint, 2026. https://arxiv.org/abs/2608.20824
• S. Shelah, Primitive recursive bounds for van der Waerden numbers, J. Amer. Math. Soc., 1988. https://doi.org/10.1090/S0894-0347-1988-0929498-X
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal., 2001. https://doi.org/10.1007/s00039-001-0332-9

Motivation

Let $p_n$ be the $n$-th prime and $d_n=p_{n+1}-p_n$ the $n$-th gap. By the prime number theorem the average gap near $p$ is about $\log p$. A great deal is known about how large individual gaps can be, but much less about how often large gaps occur. A natural question is whether, for each fixed $C$, a positive proportion of all gaps exceed $C\log p_n$. Erdős and Prachar (1962) asked a closely related question about the sequence $p_n/n$: do the indices where it increases have positive lower density?

Background

• 1931. Westzynthius proves that $d_n/\log p_n$ is unbounded.
• 1935, 1938. Erdős and Rankin construct quantitatively larger gaps (doi:10.1093/qmath/os-6.1.124, doi:10.1112/jlms/s1-13.4.242).
• 1962. Erdős and Prachar ask whether the indices with $p_n/n<p_{n+1}/(n+1)$ have positive lower density (doi:10.1007/BF02992930).
• 1965. Bombieri and A. I. Vinogradov prove the distribution theorem for primes in progressions on average (doi:10.1112/S0025579300005313).
• 1976. Gallagher derives Poisson statistics for primes in short intervals from a uniform Hardy–Littlewood hypothesis (doi:10.1112/S0025579300016442).
• 2005, 2015. Goldston–Yıldırım's divisor-sum correlations and Maynard's multidimensional sieve give the weight technology later used for gaps (arXiv:math/0504336, doi:10.4007/annals.2015.181.1.7).
• 2010. Bazzanella, Languasco and Zaccagnini obtain positive proportions of prime-start intervals for thresholds below $0.579$, and distinguish counting gaps from counting interval starts (doi:10.1090/S0002-9947-09-05009-0).
• 2016, 2018. Ford, Green, Konyagin and Tao, and Maynard, independently improve the Erdős–Rankin bound; their joint work follows (doi:10.4007/annals.2016.183.3.4, doi:10.4007/annals.2016.183.3.3, doi:10.1090/jams/876).

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

Setting

• $p_1=2<p_2=3<\cdots$ are the primes in order, and $d_n=p_{n+1}-p_n$.
• For $A\subseteq\{1,2,\dots\}$, the lower asymptotic density is $\underline d(A)=\liminf_{N\to\infty}|A\cap[1,N]|/N$.
• All logarithms are natural.

Formalization targets

Goal: Theorem 1.1 and Corollary 1.2

For every fixed real $C>0$ there are $c(C)>0$ and $N_0(C)$ with

$$\#\{1\le n\le N:\ p_{n+1}-p_n>C\log p_n\}\ \ge\ c(C)\,N\qquad(N\ge N_0(C)),$$

and

$$\underline d\Bigl(\Bigl\{n\ge1:\ \frac{p_n}{n}<\frac{p_{n+1}}{n+1}\Bigr\}\Bigr)>0.$$

The Lean statement OAI.Problem344.large_gaps_and_ratio_density is the conjunction of these two claims and is open on the platform.

Significance

Theorem 1.1 says that gaps of size $C\log p$ are not rare for any fixed $C$: they occupy a positive proportion of the indices up to every large $N$. This is a statement about the frequency of large gaps, not about the size of the largest one, and it does not follow from the Erdős–Rankin or Ford–Green–Konyagin–Maynard–Tao constructions. Corollary 1.2 answers the Erdős–Prachar question: since $p_n/n<p_{n+1}/(n+1)$ is equivalent to $d_n>p_n/n\sim\log p_n$, it follows from Theorem 1.1 with $C=2$. The constants are not made explicit.

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

Difficulty

Counting gaps differs from counting empty intervals: a single very long gap contains many starting points of prime-free intervals, so a positive proportion of empty intervals can come from a sparse set of gaps. Results of the latter kind (Bazzanella–Languasco–Zaccagnini, Tao's empty-interval argument) therefore do not give gap counts. The proof needs a sieve weight that makes a prime in $(m,m+h]$ likely while making $(m+h,m+2h]$ almost surely prime-free, and then a multiplicity argument (the last prime before the empty interval is selected by at most $h$ values of $m$) to convert weighted interval mass into a count of distinct gaps. Making the second interval nearly empty requires an alternating family of divisor-sum squares whose adjacent dimensions nearly cancel.

Formalization scope

• prime n = Nat.nth Nat.Prime (n - 1), so prime 1 = 2; largeGapIndices C N filters Finset.Icc 1 N by C * log (prime n) < prime (n+1) - prime n in ℝ.
• lowerAsymptoticDensity A = sSup {d | ∃ N0, ∀ N ≥ N0, d ≤ initialCount A N / N}, which equals the liminf because the ratios lie in $[0,1]$.
• ratioIncreaseIndices = {n | 1 ≤ n ∧ prime n / n < prime (n+1) / (n+1)} in ℝ.
• The first clause quantifies over all real $C>0$, with $c$ and $N_0$ depending on $C$.

A complete development needs the prime number theorem, the Bombieri–Vinogradov theorem, smooth Goldston–Yıldırım/Maynard divisor-sum correlations, and averages of the Hardy–Littlewood singular series. These are widely reusable. Contributions formalizing Proposition 2.1 (weights for adjacent intervals), Proposition 3.1 (moment identities and a detector bound), Proposition 4.2 (cancellation between high dimensions), Proposition 5.1 (uniform mixed moments) and Lemma 5.4 (singular series in boxes) are welcome.

Selected references

• OpenAI, Positive lower density of large prime gaps, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Positive-lower-density-of-large-prime-gaps-September-25-2026/main.pdf
• P. Erdős, K. Prachar, Sätze und Probleme über $p_k/k$, Abh. Math. Sem. Univ. Hamburg, 1962. https://doi.org/10.1007/BF02992930
• D. Bazzanella, A. Languasco, A. Zaccagnini, Prime numbers in logarithmic intervals, Trans. Amer. Math. Soc., 2010. https://doi.org/10.1090/S0002-9947-09-05009-0
• J. Maynard, Small gaps between primes, Ann. of Math., 2015. https://doi.org/10.4007/annals.2015.181.1.7
• D. A. Goldston, C. Y. Yıldırım, Small gaps between primes I, preprint, 2005. https://arxiv.org/abs/math/0504336
• K. Ford, B. Green, S. Konyagin, J. Maynard, T. Tao, Long gaps between primes, J. Amer. Math. Soc., 2018. https://doi.org/10.1090/jams/876
• P. X. Gallagher, On the distribution of primes in short intervals, Mathematika, 1976. https://doi.org/10.1112/S0025579300016442
• E. Bombieri, On the large sieve, Mathematika, 1965. https://doi.org/10.1112/S0025579300005313
• R. A. Rankin, The difference between consecutive prime numbers, J. London Math. Soc., 1938. https://doi.org/10.1112/jlms/s1-13.4.242

Motivation

Euler's totient $\varphi(n)$ counts the integers in $\{1,\dots,n\}$ coprime to $n$. Many integers share a totient, and most integers are not totients at all, so counting the distinct values of $\varphi$ is much harder than counting integers with a given factorization. Let

$$\mathcal V=\{\varphi(n):n\ge1\},\qquad V(x)=\#\{v\in\mathcal V: v\le x\}.$$

The size of $V(x)$ was studied by Pillai, Erdős, Hall, Pomerance, Maier and Ford over most of the twentieth century; Ford's 1998 estimate determines $V(x)$ up to a bounded multiplicative factor but leaves open whether $V(x)$ has an asymptotic equivalent, and Erdős and Hall's question whether $V(cx)/V(x)\to c$.

This mission asks for a formal proof of the explicit asymptotic formula and the Erdős–Hall regular-variation property, as stated in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1929 — Pillai proves that totients have density zero (Bull. AMS 35, 1929).
• 1935 — Erdős shows $V(x)\ll_\varepsilon x/(\log x)^{1-\varepsilon}$ via the normal number of prime factors of $p-1$ (Q. J. Math. 1935); later lower bounds use semiprimes (1945).
• 1976 — Erdős and Hall obtain a lower factor $\exp\{a(\log_3x)^2\}$ and ask whether $V(cx)/V(x)\to c$ (Mathematika 1976).
• 1986–1988 — Pomerance brings the upper bound to the same scale (Acta Arith. 1986); Maier and Pomerance determine the leading constant $C_0=0.8178\ldots$ in $V(x)=\frac{x}{\log x}\exp\{(C_0+o(1))(\log_3x)^2\}$ (Acta Arith. 1988).
• 1998 — Ford determines $V(x)$ up to a bounded factor and proves $V(cx)-V(x)\asymp_cV(x)$ (Ramanujan J. 1998).
• September 2026 — The OpenAI preprint claims an explicit asymptotic equivalent and $V(cx)/V(x)\to c$ (Theorem 2.1, p. 4).

Setting

Logarithms are natural and $\log_j$ is the $j$-fold iterate. For $j\ge1$ let $a_j=(j+1)\log(j+1)-j\log j-1$, let $\rho\in(0,1)$ be the unique root of $\sum_{j\ge1}a_j\rho^j=1$, and set

$$\lambda=\log(1/\rho),\qquad \gamma=\Bigl(\sum_{j\ge1}ja_j\rho^j\Bigr)^{-1},\qquad g_0=1,\ \ g_j=\sum_{d=1}^ja_dg_{j-d}.$$

For large $x$ put $B=\log_2x$, $m=\lfloor(\log B-\log_2B)/\lambda\rfloor$, the phase $\theta=(\log B-\log_2B)/\lambda-m\in[0,1)$, and $G_m=B^m/(m!\prod_{i\le m}g_i)$; the factor $\frac{x}{\log x}G_m$ is Ford's counting scale.

For each $H$ the preprint defines an explicit arithmetic coefficient $A_H(f;s)$, $s\in[0,1)$, from a finite set of "tail witnesses" (tuples of primes $Q_h$, $P\le h<H$, and a cofactor $a$, subject to explicit size and recurrence constraints, $P=\lfloor\log\log H\rfloor$) by inclusion–exclusion over witnesses with a common totient $d$, weighted by $f(\ell(d)/d)/d$ (formula (2.8), p. 5). Here $\ell(v)=\min\{n\ge1:\varphi(n)=v\}$ is the least preimage, and $A(f;s)=\lim_{H\to\infty}A_H(f;s)$ when the limit exists. The coefficient is defined without reference to $V$.

Formalization targets

Milestone: nonnegativity of the approximants (Theorem 2.1, p. 4)

$A_H(1;s)\ge0$ for $s\in[0,1)$.

Goal: Theorem 2.1 (p. 4)

$A_H(1;\cdot)\to A(1;\cdot)$ uniformly on $[0,1)$, with $0<\inf_sA(1;s)\le\sup_sA(1;s)<\infty$, and

$$V(x)\sim\frac{x}{\log x}\,G_m\,A(1;\theta),\qquad \frac{V(cx)}{V(x)}\longrightarrow c\quad(c>0\ \text{fixed}).$$

Further milestones: least preimages (Theorem 2.2, p. 6)

For $k\ge1$ let $N_k(x)=\#\{v\in\mathcal V:v\le x,\ kx<\ell(v)\le(k+1)x\}$ and $f_k(r)=\min\{1,\tfrac{k+1}r\}-\min\{1,\tfrac kr\}$. Then $A_H(f_k;\cdot)$ converges uniformly and $N_k(x)=\frac{x}{\log x}G_m(A(f_k;\theta)+o(1))$; if some totient $d$ has $\ell(d)>kd$ then $\inf_sA(f_k;s)>0$ and $N_k(x)\asymp V(x)$, and otherwise $N_k\equiv0$ and $A(f_k;\cdot)\equiv0$. The positive alternative holds for $k=1,2$.

Significance

The result itself. The formula replaces Ford's bounded uncertainty by an explicit function of the phase $\theta$, built from finite arithmetic data, and answers the Erdős–Hall question: $V$ is regularly varying of index $1$. Theorem 2.2 answers, in weighted form, Erdős's question on how least preimages are distributed in intervals $(kx,(k+1)x]$, reducing it to the existence of a "seed" totient with $\ell(d)>kd$. Whether such seeds exist for every $k$ (equivalently, whether $\ell(d)/d$ is unbounded) is not settled by the preprint.

Formalizing it. This is analytic number theory at full strength: Ford's structure theorems for totient preimages, sieve bounds for two or three linear forms in shifted primes, simplex volume computations and an inclusion–exclusion limit. Mathlib has the totient and the prime number theorem in some forms but not these sieve and distribution results. The definitions in this mission (the renewal root $\rho$, the witnesses, $A_H$) are explicit and can be checked independently of any proof.

Difficulty

Counting integers $n$ with a typical factorization is a volume computation, but $V(x)$ counts values, and different $n$ can have the same totient. The preprint must show that, outside a negligible set, distinct long prime prefixes give distinct values (Proposition 5.1, p. 22, and Proposition 5.3, p. 27), which needs a uniform comparison estimate for products of shifted primes (Proposition 4.2, p. 17), while short discrete tails that may collide are kept exactly and handled by inclusion–exclusion (Lemma 6.4, p. 30). The limits are taken in a specific order ($x\to\infty$ with $H$ fixed, then $H\to\infty$), and no continuity of $s\mapsto A(1;s)$ is available, so all errors must be uniform in the phase.

Formalization scope

• IsTotient v means $v=\varphi(n)$ for some $n\ge1$; V x counts totients in $\{1,\dots,\lfloor x\rfloor\}$; ell v is Nat.find of the least preimage (junk value $0$ for non-totients, never used on them).
• rho is the sInf of roots in $(0,1)$ of $\sum_{j\ge0}a_{j+1}z^{j+1}=1$; the root is unique, so this is the source's $\rho$.
• AH H f s is formula (2.8) with finsum over totients $d$ and over nonempty finite sets $T$ of witnesses with $\varphi(w)=d$; the witness set is finite for each $H$, so the finsums are genuine finite sums. A f s is limUnder atTop; the goal asserts uniform convergence, so the junk value is never used.
• mainTerm x = x / log x * G x (m x) * A 1 (theta x); asymptotic equivalence is Tendsto (V x / mainTerm x) atTop (𝓝 1).
• The milestone coefficient_nonnegative is stated for every $H$, while the source states it for sufficiently large $H$; for small $H$ the witness set is empty or the inclusion–exclusion is still a probability, so this is a harmless strengthening.
• companion_zero_case restates alternative (ii) of Theorem 2.2 in a separate definition file (TotientCompanionZero) with identical definitions.

Selected references

• OpenAI, An asymptotic formula for the number of totients, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/An-asymptotic-formula-for-the-number-of-totients-September-25-2026.pdf
• S. S. Pillai, On some functions connected with φ(n), Bull. Amer. Math. Soc. 35 (1929), 832–836. https://www.ams.org/journals/bull/1929-35-06/S0002-9904-1929-04799-2/S0002-9904-1929-04799-2.pdf
• P. Erdős, On the normal number of prime factors of p−1 and some related problems concerning Euler's φ-function, Q. J. Math. 6 (1935). https://doi.org/10.1093/qmath/os-6.1.205
• P. Erdős, R. R. Hall, Distinct values of Euler's φ-function, Mathematika 23 (1976). https://doi.org/10.1112/S0025579300006100
• C. Pomerance, On the distribution of the values of Euler's function, Acta Arith. 47 (1986). https://doi.org/10.4064/aa-47-1-63-70
• H. Maier, C. Pomerance, On the number of distinct values of Euler's φ-function, Acta Arith. 49 (1988). https://doi.org/10.4064/aa-49-3-263-275
• K. Ford, The distribution of totients, Ramanujan J. 2 (1998), 67–151; revised arXiv:1104.3264. https://arxiv.org/abs/1104.3264v2

Motivation

For a positive integer $n$, Jacobsthal's function $j(n)$ is the least $m$ such that every run of $m$ consecutive integers contains an integer coprime to $n$. Equivalently, $j(n)-1$ is the longest interval that can be covered by choosing one residue class modulo each prime divisor of $n$ (the classes $0\bmod p$ shifted by the interval's start). Its maximum over integers with at most $k$ prime divisors,

$$h(k)=\max\{j(n):\ \omega(n)\le k\},$$

governs how long a stretch can be sieved out by $k$ primes. It is linked to gaps between consecutive primes (long covered intervals produce large prime gaps, as in the Erdős–Rankin and Ford–Green–Konyagin–Maynard–Tao constructions) and to the limits of the linear sieve. Jacobsthal asked, and Erdős recorded, whether $h(k)\ll k^2$.

Background

• 1960. Jacobsthal begins a series of papers on this function.
• 1962. Erdős records Jacobsthal's question $h(k)\ll k^2$ and notes Brun's bound $h(k)\ll k^{C_0}$ (doi:10.7146/math.scand.a-10523).
• 1971. Iwaniec's error-term estimate for the linear sieve gives order $k^2\log^2k$ for the first $k$ primes (doi:10.4064/aa-19-1-1-30).
• 1977. Vaughan proves the uniform bound $j(n)\ll\omega(n)^2\log(2\omega(n))$ and explains the exponent 2 by the linear sieve's square-root restriction (doi:10.1017/S0013091500026560).
• 1978. Iwaniec proves $h(k)\ll k^2\log^2k$ for arbitrary prime sets (doi:10.1515/dema-1978-0121).
• 2012. Hajdu and Saradha disprove Jacobsthal's primorial-extremality conjecture: $j(P_{24})=234<236=h(24)$ (doi:10.1090/S0025-5718-2012-02581-6).
• 2015, 2019. Costello–Watts and Ziller compute bounds and exact values for small $k$ (doi:10.1090/S0025-5718-2014-02896-2).
• 2018. Ford, Green, Konyagin, Maynard and Tao give the lower bound $j(P_k)\gg k(\log k)^2\frac{\log\log\log k}{\log\log k}$ (doi:10.1090/jams/876).

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

Setting

• $\omega(n)$ is the number of distinct prime divisors of $n$, with $\omega(1)=0$.
• For $n\ge1$, $j(n)$ is the least $m\ge1$ such that for every integer $a$, one of $a,a+1,\dots,a+m-1$ is coprime to $n$ (note $\gcd(0,n)=n$).
• $h(k)=\sup\{j(n):n\ge1,\ \omega(n)\le k\}$ for $k\ge1$. All logarithms are natural.

Formalization targets

Milestone: quadratic bound (Jacobsthal's question)

$$\exists C>0\ \forall k\ge1:\quad h(k)\le C\,k^2.$$

Goal: Theorem 1.1

$$\exists C>0\ \forall k\ge1:\quad h(k)\le C\,\frac{k^2}{(\log\log(3k))^2}.$$

Both are stated in Lean as the existence, for each $k$, of a length $m$ satisfying IsJacobsthalBound k m with the displayed size bound. The goal OAI.Erdos970.Erdos970Final.erdos_970_iterated_log is open on the platform.

Significance

Theorem 1.1 answers Jacobsthal's question affirmatively, uniformly over all prime sets and interval positions, and removes the logarithmic losses in the bounds of Vaughan and Iwaniec, going slightly below the quadratic scale. It shows that the linear sieve can be pushed to its limiting parameter $s=2$, where the lower sieve function vanishes, by retaining a boundary contribution. The gap to the best lower bound (roughly $k(\log k)^2$) remains large; Vaughan suggested $j(n)\ll_\varepsilon\omega(n)^{1+\varepsilon}$.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The constant $C$ is not made explicit.

Difficulty

The linear sieve gives a lower bound for the number of uncovered integers only when the sieving range is below the square root of the interval length, which is exactly where the exponent 2 comes from; at the critical parameter the main term of the lower-bound sieve vanishes, so the standard argument yields nothing and a $\log^2k$ loss appears. One must keep the boundary term that the leading linear-sieve calculation discards, and then show that the actual prescribed residue classes do not deviate much from a reference calculation. Positivity of the reference calculation alone does not suffice: the comparison requires an inverse estimate for a witnessing edge of a decreasing-prime tree, variance bounds, and stopping-time counts for hard endpoints.

Formalization scope

• IsJacobsthalBound k m: for every n : ℕ with 0 < n and n.primeFactors.card ≤ k, and every a : ℤ, some i < m has (a + i).natAbs.Coprime n.
• JacobsthalQuadratic: ∃ C > 0, ∀ k > 0, ∃ m, IsJacobsthalBound k m ∧ m ≤ C k^2.
• JacobsthalIteratedLog: the same with bound C k^2 / (log (log (3k)))^2; for $k\ge1$ the denominator is positive.
• The two targets live in separate definition files that both define IsJacobsthalBound identically.

A complete development needs the fundamental lemma of the sieve, Buchstab-type functions of the linear sieve, prime number theorem estimates in short ranges and progressions, the additive large sieve, a lattice-point count on plane curves, and renewal-type arguments for a continuous path process. Contributions formalizing Theorem 1.2 (the quantitative covering estimate), Lemma 2.1 (fundamental lemma of the sieve), Proposition 6.3 (positive reference margin), Proposition 8.2 (inverse estimate for an edge) and Corollary 9.3 are welcome.

Selected references

• OpenAI, A quadratic bound for Jacobsthal's function, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026/paper.pdf
• P. Erdős, On the integers relatively prime to n and on a number-theoretic function considered by Jacobsthal, Math. Scand., 1962. https://doi.org/10.7146/math.scand.a-10523
• R. C. Vaughan, On the order of magnitude of Jacobsthal's function, Proc. Edinburgh Math. Soc., 1977. https://doi.org/10.1017/S0013091500026560
• H. Iwaniec, On the problem of Jacobsthal, Demonstratio Math., 1978. https://doi.org/10.1515/dema-1978-0121
• H. Iwaniec, On the error term in the linear sieve, Acta Arith., 1971. https://doi.org/10.4064/aa-19-1-1-30
• L. Hajdu, N. Saradha, Disproof of a conjecture of Jacobsthal, Math. Comp., 2012. https://doi.org/10.1090/S0025-5718-2012-02581-6
• K. Ford, B. Green, S. Konyagin, J. Maynard, T. Tao, Long gaps between primes, J. Amer. Math. Soc., 2018. https://doi.org/10.1090/jams/876
• F. Costello, P. Watts, An upper bound on Jacobsthal's function, Math. Comp., 2015. https://doi.org/10.1090/S0025-5718-2014-02896-2
• J. Friedlander, H. Iwaniec, Opera de Cribro, AMS, 2010. https://doi.org/10.1090/coll/057

Motivation: when is a polynomial value free of high powers?

An integer $a$ is $k$-power-free if no prime power $p^k$ divides it (zero is never $k$-power-free). For a fixed integer polynomial $f$ one expects $f(n)$ to be $k$-power-free for a positive proportion of integers $n$, given by an Euler product of local densities, as soon as no prime $k$th power divides every value of $f$. The heuristic is a sieve: discard the $n$ with $p^k\mid f(n)$ for each prime $p$. Small primes are handled by the Chinese remainder theorem; the problem lies with primes $p$ larger than the range of $n$, where $f(n)$ can be divisible by $p^k$ only if it has an unusually large square-full part. The case $k=d-2$, where $d=\deg f$, is the first exponent left open by classical methods. Its best-known instance is the squarefreeness of $n^4+2$, singled out by Erdős in 1953 and again in his 1965 survey.

Timeline

• 1933 — Ricci proves the density asymptotic when $k\ge d$ (Rend. Circ. Mat. Palermo 57).
• 1953 — Erdős proves infinitely many $(d-1)$-power-free values for $d\ge3$ and singles out the unresolved squarefreeness of $n^4+2$ (J. London Math. Soc.).
• 1967 — Hooley obtains the asymptotic at exponent $k=d-1$ (Mathematika 14).
• 1976 — Nair proves the asymptotic for $k\ge(\sqrt2-\tfrac12)d$, which reaches $k=d-2$ for $d\ge24$ (Mathematika 23).
• 1998 — Granville shows that the $abc$ conjecture implies the predicted squarefree density for every separable polynomial without a fixed square divisor (IMRN 1998).
• 2006 — Heath-Brown's affine determinant method gives $k\ge(3d+2)/4$, reaching $k=d-2$ for $d\ge10$.
• 2011 — Browning, combining this with Salberger's global determinant method, reaches $k\ge(3d+1)/4$, hence $k=d-2$ for $d\ge9$ (Arch. Math. 96); Xiao gives a published reproof (IMRN 2017).
• 2013–2015 — Heath-Brown treats binomials $x^d+c$ for $k\ge(5d+3)/9$ (Q. J. Math. 64); Reuss obtains a power-saving error at $k=d-1$ (Bull. LMS 47).
• 2026 — An OpenAI preprint, Squarefree values of quartics and power-free values of polynomials (OpenAI Math Release, September 24, 2026), claims the case $k=d-2$ for all degrees $4\le d\le 8$, including squarefree values of every admissible irreducible quartic. It has not been peer reviewed, and its proof is not formally verified.

Setting

Let $f\in\mathbb Z[x]$ be irreducible over $\mathbb Q$, of degree $d$, and let $k\ge2$. Define

$$\rho_f(q)=\#\{a\in\mathbb Z/q\mathbb Z:\ f(a)\equiv0\pmod q\},\qquad S_{f,k}(X)=\#\{1\le n\le X:\ f(n)\text{ is $k$-power-free}\}.$$

The local admissibility condition is $\rho_f(p^k)<p^k$ for every prime $p$: no prime $k$th power divides all values of $f$. The predicted density is

$$c_{f,k}=\prod_p\Bigl(1-\frac{\rho_f(p^k)}{p^k}\Bigr).$$

Formalization targets

Goal: power-free values at exponent $d-2$ in every degree $d\ge4$ (Corollary 1.2)

Let $f\in\mathbb Z[x]$ be irreducible over $\mathbb Q$ with $d=\deg f\ge4$, put $k=d-2$, and assume $\rho_f(p^k)<p^k$ for every prime $p$. Then the Euler product converges,

$$c_{f,k}>0,\qquad S_{f,k}(X)=c_{f,k}X+o_f(X)\quad(X\to\infty).$$

For $4\le d\le 8$ this is the paper's new Theorem 1.1; for $d\ge9$ it follows from Browning's theorem. Already the case $d=4$ (squarefree values of quartics such as $n^4+2$ and $n^4+1$) is new. The goal statement is published on the platform with status Open.

Significance

The result itself. The theorem closes the exponent $k=d-2$ for every degree, answering Erdős's question about $n^4+2$ and giving the first unconditional squarefree-density theorem for an arbitrary admissible irreducible quartic. No primitivity or sign condition on $f$ is required. The same large-prime estimate also gives densities for separable products and simultaneous power-freeness of several polynomials (Corollary 1.3).

Formalizing it. The statement is elementary, but its proof uses number-field factorization, the unit theorem, determinant methods for counting points on surfaces and curves, and explicit Hilbert-function computations. None of these components is machine-checked. A formal proof would certify a result that the literature had only reached conditionally (on $abc$) or in higher degrees. The finite-prime sieve and the deduction of the density from a large-prime tail bound are reusable for other power-free-value problems.

Difficulty

The sieve over primes $p\le X$ is routine. The obstacle is the primes $p>X$: one must show that very few $n\in(X,2X]$ have $p^k\mid f(n)$ for some such $p$ (Proposition 1.4, with a power saving $X^{1-\delta}$). Counting solutions of $f(n)=yp^k$ as integer points on the surface $f(x)=yz^k$ with determinant methods succeeds only when $p$ is large; in the intermediate range the point counts are too weak, and the existing determinant bounds stop exactly at $k\ge(3d+1)/4$.

Formalization scope

• $f$ is a Polynomial ℤ whose image in Polynomial ℚ is irreducible, with natDegree ≥ 4; the exponent is f.natDegree - 2 (at least $2$, so the natural-number subtraction is harmless).
• PowerFree k a says no prime $p$ has $p^k\mid a$, so $a=0$ is not power-free, matching the source convention; negative values are allowed.
• $\rho_f(q)$ counts $a\in\{0,\dots,q-1\}$ with $q\mid f(a)$; $S_{f,k}(X)$ counts $1\le n\le\lfloor X\rfloor$ over real $X$.
• The density constant is a tprod over Nat.Primes; the goal asserts Multipliable explicitly, so the constant is not a junk value, together with $c_{f,k}>0$ and $S_{f,k}(X)-c_{f,k}X=o(X)$.
• No height or uniformity in $f$ is asserted, matching the source.
• Needed infrastructure: algebraic number fields and ideal factorization, the unit theorem, Hensel lifting, determinant-method point counting, and an Euler-product sieve. The $d\ge9$ case also needs Browning's theorem (in Xiao's formulation), itself unformalized.

Selected references

• G. Ricci, Ricerche aritmetiche sui polinomi, Rend. Circ. Mat. Palermo 57 (1933). https://doi.org/10.1007/BF03017586
• P. Erdős, Arithmetical properties of polynomials, J. London Math. Soc. 28 (1953). https://doi.org/10.1112/jlms/s1-28.4.416
• C. Hooley, On the power free values of polynomials, Mathematika 14 (1967). https://doi.org/10.1112/S002557930000797X
• M. Nair, Power free values of polynomials, Mathematika 23 (1976). https://doi.org/10.1112/S0025579300008779
• A. Granville, ABC allows us to count squarefrees, IMRN 1998. https://doi.org/10.1155/S1073792898000592
• T. D. Browning, Power-free values of polynomials, Arch. Math. 96 (2011). https://doi.org/10.1007/s00013-011-0224-7
• S. Y. Xiao, Power-free values of binary forms and the global determinant method, IMRN 2017. https://doi.org/10.1093/imrn/rnw165
• D. R. Heath-Brown, Power-free values of polynomials, Q. J. Math. 64 (2013). https://doi.org/10.1093/qmath/har030
• T. Reuss, Power-free values of polynomials, Bull. London Math. Soc. 47 (2015). https://doi.org/10.1112/blms/bdu116
• OpenAI, Squarefree values of quartics and power-free values of polynomials, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2; Corollary 1.2, p. 4). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Squarefree-values-of-quartics-and-power-free-values-of-polynomials-September-24-2026/manuscript.pdf

Motivation

Goldbach-type problems ask which sets are sumsets of primes. The inverse Goldbach problem, due to Ostmann (1956), reverses the question: can the set of primes itself, up to finitely many changes, be written as a sumset $A+B=\{a+b:a\in A,\ b\in B\}$ with both $A$ and $B$ having at least two elements? Ostmann conjectured that it cannot: the primes are asymptotically additively indecomposable. The problem is a clean test of how much additive structure the primes can carry, and it connects sieve theory (the primes avoid one residue class modulo each prime) with inverse questions for the large sieve.

Background

• 1954–1955. Hornfeck proves early restrictions on additive decompositions of the primes (doi:10.1007/BF01187376).
• 1956. Ostmann formulates the conjecture in his treatise on additive number theory (doi:10.1007/978-3-662-11030-0).
• 1964. Laffer and Mann show that a hypothetical decomposition must have two infinite summands (doi:10.2140/pjm.1964.14.547).
• 1988–1996. Pomerance, Sárközy and Stewart, and Hofmann and Wolke, obtain sieve restrictions on the summands (doi:10.2140/pjm.1988.133.363, doi:10.1007/BF01189097).
• 2001. Elsholtz combines the large and larger sieves to put both counting functions near the square-root scale and rules out decompositions into three nontrivial summands (doi:10.1112/S0025579300014406).
• 2014–2016. Green and Harper show that an inverse large-sieve conjecture would imply Ostmann's conjecture (arXiv:1311.6176); Elsholtz and Harper sharpen the binary counting bounds (doi:10.1090/S0002-9947-2014-06384-8); Shao proves a finite ternary obstruction (doi:10.1353/ajm.2016.0038).
• 2020–2026. Hanson, then Croot, Mao and Yip, and Croot, Mao, Pohoata and Yip prove partial inverse theorems for the large sieve and derive further necessary conditions on a hypothetical decomposition (doi:10.1017/S0305004118000518, arXiv:2510.08862, arXiv:2607.15311).

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

Setting

Let $\mathbb N_0=\{0,1,2,\dots\}$ and let $P$ be the set of positive primes. For $A,B\subseteq\mathbb N_0$ the sumset is $A+B=\{a+b:a\in A,\ b\in B\}$. Two sets are asymptotically equal if their symmetric difference $X\triangle Y=(X\setminus Y)\cup(Y\setminus X)$ is finite. A decomposition is nontrivial if $|A|\ge2$ and $|B|\ge2$; the trivial decompositions $\{0\}+P$ are excluded.

Formalization targets

Goal: Theorem 1.1 (Ostmann's conjecture)

$$A,B\subseteq\mathbb N_0,\ |A|\ge2,\ |B|\ge2\ \Longrightarrow\ (A+B)\triangle P\ \text{is infinite}.$$

Milestone: Theorem 2.3 (two infinite summands)

$$\text{There are no infinite }A,B\subseteq\mathbb N_0\text{ with }(A+B)\triangle P\text{ finite}.$$

Theorem 2.3 is the core of the proof; Lemma 2.2 reduces Theorem 1.1 to it by a short sieve argument.

The goal OAI.Ostmann.inverseGoldbach is open on the platform.

Significance

Theorem 1.1 resolves Ostmann's conjecture. The conclusion controls both requirements of an eventual decomposition: if $|A|,|B|\ge2$ and $A+B$ contains every sufficiently large prime, then $A+B$ contains infinitely many composite numbers. The proof does not go through the general inverse large-sieve conjecture of Green and Harper; it uses the simultaneous residue restrictions together with coverage of every large prime directly.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The statement is elementary, so the formal target is short; the difficulty is entirely in the proof.

Difficulty

Counting alone cannot work: sieve bounds put $A(x)$ and $B(x)$ near $\sqrt x$, which is compatible with the lower bound $A(x)B(x)\gg x/\log x$ forced by covering the primes. The known necessary conditions (large intersections with quadratic images) fall short of the near-containment that Green and Harper's conditional route requires. The proof must turn the local information (modulo each prime $p$, the images of $A$ and $-B$ are disjoint) into a global contradiction: it rules out correlations with translated multiplicative characters of every order, compares a positive sumset statistic with its average over the primes, and handles residue indicators with no prescribed algebraic form via a finite-field comparison of binary trees. The paper runs to about 80 pages.

Formalization scope

• primes = {n : ℕ | Nat.Prime n}; sumset A B is Mathlib's pointwise A + B on Set ℕ.
• A.Nontrivial means $A$ has two distinct elements.
• InverseGoldbach asserts Set.Infinite (sumset A B ∆ primes); TwoInfiniteSummandsImpossible uses EventuallyPrimeSumset A B := ∃ N, ∀ n ≥ N, n ∈ A + B ↔ n.Prime, which is equivalent to a finite symmetric difference.
• OAI.Ostmann.main is the same statement as the goal without the definition file and is included as a reference item.

A complete development needs the additive large sieve (Montgomery–Vaughan), Gallagher's larger sieve, Mertens-type estimates, character sums over finite fields including the quadratic large sieve, prime number theorems in progressions with the exceptional character, and Fourier analysis on $\mathbb F_p$. Contributions formalizing Lemma 2.1 (fixed shifts), Lemma 2.2 (finite summands), Lemma 2.4 (square-root bounds), Proposition 3.1, Corollary 4.2 (mixed-character decorrelation), Proposition 5.1 and Lemma 6.1 (tree comparison) are welcome.

Selected references

• OpenAI, The additive indecomposability of the primes, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/the-additive-indecomposability-of-the-primes-September-24-2026/paper.pdf
• H.-H. Ostmann, Additive Zahlentheorie. Erster Teil, Springer, 1956. https://doi.org/10.1007/978-3-662-11030-0
• W. B. Laffer, H. B. Mann, Decomposition of sets of group elements, Pacific J. Math., 1964. https://doi.org/10.2140/pjm.1964.14.547
• C. Elsholtz, The inverse Goldbach problem, Mathematika, 2001. https://doi.org/10.1112/S0025579300014406
• B. Green, A. J. Harper, Inverse questions for the large sieve, Geom. Funct. Anal., 2014. https://doi.org/10.1007/s00039-014-0288-1
• C. Elsholtz, A. J. Harper, Additive decompositions of sets with restricted prime factors, Trans. Amer. Math. Soc., 2015. https://doi.org/10.1090/S0002-9947-2014-06384-8
• X. Shao, On an inverse ternary Goldbach problem, Amer. J. Math., 2016. https://doi.org/10.1353/ajm.2016.0038
• B. Hanson, Additive correlation and the inverse problem for the large sieve, Math. Proc. Cambridge Philos. Soc., 2020. https://doi.org/10.1017/S0305004118000518
• E. Croot, J. Mao, C. Pohoata, C. H. Yip, A sharp inverse theorem for the quadratic large sieve, preprint, 2026. https://arxiv.org/abs/2607.15311
• H. L. Montgomery, R. C. Vaughan, The large sieve, Mathematika, 1973. https://doi.org/10.1112/S0025579300004708

Motivation: largest prime factors of neighbouring integers

Let $P^+(n)$ be the largest prime factor of an integer $n\ge2$. The classical theory of smooth numbers (Dickman 1930, Ramaswami 1949, de Bruijn 1951) shows that $\log P^+(n)/\log n$ has a limiting distribution: the proportion of $n\le X$ with $P^+(n)\le X^a$ tends to $\rho(1/a)$, where $\rho$ is the Dickman function. Multiplicative structure of $n$ and of $n+1$ is expected to be independent, since consecutive integers share no prime factor, but proving independence of such "additive shifts" of multiplicative data is the core difficulty of the Chowla/Elliott circle of problems. Erdős and Pomerance (1978) asked whether $P^+(n)$ and $P^+(n+1)$ are asymptotically independent with Dickman marginals, and, as a consequence, whether $P^+(n)<P^+(n+1)$ holds for exactly half of all $n$ (a comparison question usually attributed to Erdős and Turán).

Timeline

• 1930–1951 — Dickman, Ramaswami and de Bruijn establish the one-variable law $\#\{n\le X: P^+(n)\le X^a\}/X\to\rho(1/a)$.
• 1978 — Erdős and Pomerance formulate the joint independence problem, prove that each ordering of $P^+(n),P^+(n+1)$ has lower natural density at least $0.0099$, and show that $P^+(n)/P^+(n+1)$ rarely lies in $(X^{-\delta},X^{\delta})$ (Aequationes Math. 17 (1978)).
• 2005 — de la Bretèche, Pomerance and Tenenbaum raise the lower density to $0.05544$ (and $0.05866$ via an observation of Fouvry).
• 2017–2018 — Wang obtains $0.1063$ and $0.1356$.
• 2018 — Teräväinen proves the joint Dickman law in logarithmic density, and logarithmic density $1/2$ for the ordering (Forum Math. Sigma 6 (2018)).
• 2019 — Tao and Teräväinen obtain the joint law for ordinary averages outside an exceptional set of scales of logarithmic density zero (Algebra Number Theory 13 (2019)).
• 2021 — Wang proves the ordinary joint law conditionally on the Elliott–Halberstam conjecture for friable integers (J. Number Theory 223).
• 2022 — Jiang, Lü and Wang prove averaged-over-shift versions (Adv. Math. 409).
• 2025–2026 — Lü and Wang reach lower density $0.2017$; Yang reaches $0.280$ (arXiv:2607.16032); Tao and Teräväinen give a quantitative joint law outside exceptional scales (arXiv:2512.01739).
• 2026 — An OpenAI preprint, The joint Dickman law for consecutive integers (OpenAI Math Release, September 24, 2026), claims the unconditional joint law in ordinary natural density at every scale. It has not been peer reviewed, and its proof is not formally verified.

Setting

For $n\ge2$, $P^+(n)$ is the largest prime dividing $n$. The Dickman function $\rho:[0,\infty)\to\mathbb R$ is the continuous function with

$$\rho(u)=1\ (0\le u\le1),\qquad u\rho'(u)=-\rho(u-1)\ (u>1),$$

equivalently $\rho(u)=1-\int_1^u \rho(t-1)\,\frac{dt}{t}$ for $u\ge1$. For a property $P$ of integers and real $X>0$, the natural density at scale $X$ is

$$\mathrm{realDensity}(P,X)=\frac1X\,\#\{2\le n\le X:\ P(n)\}.$$

Formalization targets

Goal: the joint Dickman law (Theorem 1.1)

For every fixed $a,b\in(0,1)$,

$$\lim_{X\to\infty}\frac1X\#\{2\le n\le X:\ P^+(n)\le n^a,\ P^+(n+1)\le n^b\}=\rho(1/a)\,\rho(1/b),$$

with $X$ running over all reals and ordinary, unweighted counting. The goal statement is published on the platform with status Open.

Milestones: equal ordering densities (Corollary 1.2)

$$\lim_{X\to\infty}\frac1X\#\{2\le n\le X:\ P^+(n)<P^+(n+1)\}=\tfrac12, \qquad \lim_{X\to\infty}\frac1X\#\{2\le n\le X:\ P^+(n+1)<P^+(n)\}=\tfrac12 .$$

Significance

The result itself. Theorem 1.1 says that, in natural density, $\log P^+(n)/\log n$ and $\log P^+(n+1)/\log n$ are independent with Dickman marginals. It settles the Erdős–Pomerance independence question positively, removes the logarithmic weighting of Teräväinen's theorem and the exceptional scales of Tao–Teräväinen, and implies the Erdős–Turán comparison: because the limiting marginal is continuous, the product law gives no mass to the diagonal, so each strict ordering has density $1/2$ (Corollary 1.2). Previous unconditional work only gave lower natural densities, never the existence of the density.

Formalizing it. The goal is a clean density statement about elementary objects, but its proof combines Matomäki–Radziwiłł short-interval estimates, sieve bounds, a divisor amplifier, graph comparison and cut-norm sampling. No part of this argument is machine-checked. Even the one-variable Dickman law (the marginal case) is not in Mathlib, and would be a reusable milestone in its own right.

Difficulty

Independence of $n$ and $n+1$ is a binary correlation problem for multiplicative data, of the same nature as the two-point Chowla conjecture. Tao's entropy-decrement and logarithmic-averaging method handles such correlations only with weight $1/n$, or at almost all scales; the step that fails for ordinary density is ruling out a positive correlation along a sparse sequence of scales. The indicator $\mathbf 1_{P^+(n)\le n^a}$ is also not multiplicative, so short-interval theorems for multiplicative functions do not apply to it directly.

Formalization scope

• Nat.maxPrimeFac n (largest element of the prime factor list, a faithful backport of the Mathlib definition) represents $P^+(n)$; its junk values at $0,1$ are irrelevant since counting starts at $n=2$.
• realDensity P X is #{n ∈ [2, ⌊X⌋] : P n} / X as a real number, and limits are Tendsto … atTop over real $X$, matching "the limit over all real $X$".
• The thresholds are $P^+(n)\le n^a$ with real powers (n:ℝ)^a, and the hypotheses $0<a<1$, $0<b<1$ are explicit.
• $\rho$ is constructed by iterating the delay integral equation stepApprox and evaluating the $\lceil u\rceil$-th iterate at $u$; this agrees with the Dickman function on $[0,\infty)$, which is the only range used ($1/a,1/b>1$). A wrong $\rho$ would make the goal false, so this definition is part of what solvers should check.
• Needed infrastructure: the one-variable Dickman law, Selberg–Delange and sieve estimates, short-interval mean values of multiplicative functions, and profinite/Haar-measure compactness arguments. Contributions formalizing the smooth-number marginal or the deduction of Corollary 1.2 from Theorem 1.1 are welcome.

Selected references

• K. Dickman, On the frequency of numbers containing prime factors of a certain relative magnitude, Ark. Mat. Astr. Fys. 22A (1930).
• N. G. de Bruijn, On the number of positive integers $\le x$ and free of prime factors $>y$, Proc. KNAW Ser. A 54 (1951). https://research.tue.nl/en/publications/on-the-number-of-positive-integers-leq-x-and-free-of-prime-factor/
• P. Erdős and C. Pomerance, On the largest prime factors of $n$ and $n+1$, Aequationes Math. 17 (1978), 311–321. https://www.renyi.hu/~p_erdos/1978-29.pdf
• J. Teräväinen, On binary correlations of multiplicative functions, Forum Math. Sigma 6 (2018), e10. https://doi.org/10.1017/fms.2018.10
• T. Tao and J. Teräväinen, The structure of correlations of multiplicative functions at almost all scales, with applications to the Chowla and Elliott conjectures, Algebra Number Theory 13 (2019). https://doi.org/10.2140/ant.2019.13.2103
• K. Matomäki and M. Radziwiłł, Multiplicative functions in short intervals, Ann. of Math. 183 (2016). https://doi.org/10.4007/annals.2016.183.3.6
• T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers, preprint (2026). https://arxiv.org/abs/2512.01739
• OpenAI, The joint Dickman law for consecutive integers, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1 and Corollary 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-joint-Dickman-law-for-consecutive-integers-September-24-2026/paper.pdf