Erdős Problem 829

References:

• erdosproblems.com/829
• [Er83] Erdős, P. and Dudley, U., Some remarks and problems in number theory related to the work of Euler. Math. Mag. (1983), 292-298.

def Erdos829.cubes : Set ℕ

The set of perfect cubes in $\mathbb{N}$.

Equations

• Erdos829.cubes = {n : ℕ | ∃ (k : ℕ), k ^ 3 = n}

theorem Erdos829.mem_cubes_iff (m : ℕ) : m ∈ cubes ↔ ∃ k < m + 1, k ^ 3 = m

Membership in cubes can be witnessed by a bounded cube root, which makes it decidable for concrete values.

theorem Erdos829.erdos_829 : sorry ↔ ∃ (C : ℕ), (fun (n : ℕ) => ↑(AdditiveCombinatorics.sumRep cubes n)) =O[Filter.atTop] fun (n : ℕ) => Real.log ↑n ^ C

Erdős Problem 829 (open). Let $A \subseteq \mathbb{N}$ be the set of perfect cubes. Is it true that $(1_A \ast 1_A)(n) \ll (\log n)^{O(1)}$? That is, does there exist a natural number $C$ such that the number of representations of $n$ as a sum of two cubes is $O((\log n)^C)$ as $n \to \infty$?

theorem Erdos829.sumRep_cubes_zero : AdditiveCombinatorics.sumRep cubes 0 = 1

There is exactly one ordered pair of cubes summing to $0$, namely $(0, 0)$.

theorem Erdos829.sumRep_cubes_two : AdditiveCombinatorics.sumRep cubes 2 = 1

The only ordered pair of cubes summing to $2$ is $(1, 1)$.

theorem Erdos829.sumRep_cubes_three : AdditiveCombinatorics.sumRep cubes 3 = 0

The integer $3$ is not the sum of two cubes.

theorem Erdos829.sumRep_cubes_taxicab : AdditiveCombinatorics.sumRep cubes 1729 = 4

The Hardy-Ramanujan taxicab number satisfies $1729 = 1^3 + 12^3 = 9^3 + 10^3$, giving the four ordered representations $(1, 1728), (1728, 1), (729, 1000), (1000, 729)$.

theorem Erdos829.variants.mordell : Filter.limsup (fun (n : ℕ) => ↑(AdditiveCombinatorics.sumRep cubes n)) Filter.atTop = ⊤

Mordell proved $\limsup_{n \to \infty} (1_A \ast 1_A)(n) = \infty$, where $A$ is the set of perfect cubes. Equivalently, the number of representations of $n$ as a sum of two cubes is unbounded.

theorem Erdos829.variants.mahler : ∃ C > 0, ∃ᶠ (n : ℕ) in Filter.atTop, C * Real.log ↑n ^ (1 / 4) ≤ ↑(AdditiveCombinatorics.sumRep cubes n)

Mahler proved $(1_A \ast 1_A)(n) \gg (\log n)^{1/4}$ for infinitely many $n$, where $A$ is the set of perfect cubes.

[Ma35b] Mahler, K., On the lattice points on curves of genus 1. Proc. London Math. Soc. (2) (1935), 431-466.

theorem Erdos829.variants.stewart : ∃ C > 0, ∃ᶠ (n : ℕ) in Filter.atTop, C * Real.log ↑n ^ (11 / 13) ≤ ↑(AdditiveCombinatorics.sumRep cubes n)

Stewart improved Mahler's lower bound to $(1_A \ast 1_A)(n) \gg (\log n)^{11/13}$ for infinitely many $n$, where $A$ is the set of perfect cubes.

[St08] Stewart, C. L., Cubic Thue equations with many solutions. Int. Math. Res. Not. IMRN (2008), Art. ID rnn040, 11.