Erdős problem 987 · problems.science

Clunie [Cl67] proved that there exists an infinite sequence $\{z_\nu\}$ on the unit circle with $A_\nu \le \nu$ for all $\nu \ge 1$ . Translating $z_\nu = e(x_\nu)$ , the natural domain of $x_\nu$ is the half-open unit interval $\mathrm{Ico}\,0\,1$ , matching the original [Er64b]/[Cl67] statement (any unit complex number is allowed, including $z = 1$ , i.e. $x = 0$ ).

Sources

Browse retained paths and inspect the exact material available for this Problem.

10 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

987.lean

Retained formal statement8 of 10

An internal OpenAI model (see [APSSV26b, §3]) proved that there exists an infinite sequence $x_1, x_2, \ldots \in (0, 1)$ such that $\sup_n \left\lvert \sum_{j \le n} e(k x_j) \right\rvert \ll (k \log k)^{1/2}$ for all $k \ge 1$ (in particular $A_k \ll (k \log k)^{1/2}$ ).

Note: the bound is restricted to $k \ge 2$ since $\log 1 = 0$ would make the RHS vanish at $k = 1$ , while the LHS $\|\sum_{j < n} e(x_j)\|$ can equal $1$ (e.g. for $n = 1$ ).

FormalConjectures/ErdosProblems/987.leanErdos987.erdos_987.variants.sqrt_log_upper_bound3 linesExact file

1∃ x,2  ∃ (_ : ∀ (j : ℕ), x j ∈ Set.Ioo 0 1),3    ∃ C, ∃ (_ : 0 < C), ∀ (k n : ℕ), 2 ≤ k → ‖∑ j ∈ Finset.range n, additiveChar (↑k * x j)‖ ≤ C * √(↑k * Real.log ↑k)

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science