← All papers
Gaps in Multiplicative Sidon Sets
math.NT
May 3, 2026 · v1
TL;DR
An upper bound g(n)<=floor(sqrt(n)) for gaps in multiplicative Sidon sets was autonomously discovered and formally verified in Lean by the Aristotle agent.
Abstract
For a positive integer $n$, let $g(n)$ denote the infimum of all real numbers $L$ such that there exists a multiplicative Sidon set $A\subseteq\{1,2,\dots,n\}$ that intersects every interval $[x,x+L]\subseteq[1,n]$. Sárközy asked for estimates on $g(n)$, and he in particular asked whether one has $g(n)\le\sqrt n$ for every $n\in\mathbb{N}$. We first show that this estimate does indeed hold, with a proof that was autonomously discovered and formally verified in Lean by Aristotle. Next, we improve the upper bound further and, with $ρ= \frac{13-\sqrt{69}}{10} < 0.47$, prove that $g(n)\ll_{\varepsilon} n^{ρ+\varepsilon}$ for every $\varepsilon > 0$.
Problem
Sarkozy asked how small the maximal gap can be in a multiplicative Sidon set contained in {1,...,n}, and specifically whether g(n) <= sqrt(n) holds for all n.
Approach
The authors first confirm g(n) <= floor(sqrt(n)) using an elementary construction (A = {a <= n : a = 1 mod floor(sqrt(n))}), which was autonomously discovered and formally verified in Lean by the AI system Aristotle. They then improve the bound using analytic number theory, combining prime-counting estimates in short intervals with a sieve over smooth moduli.
Results
The elementary bound g(n) <= sqrt(n) is established with a machine-verified proof. The improved bound is g(n) << n^(rho + epsilon) for rho = (13 - sqrt(69))/10 < 0.47, a power-saving improvement over the sqrt(n) barrier.