Skip to content

Erdős problem 987

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

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

Note: erdosproblems.com/987 phrases the problem with the *open* interval xν(0,1)x_\nu \in (0, 1), which excludes z=1z = 1 and is strictly stronger than what [Er64b]/[Cl67] state; we align with the original papers here. The shifted-vdc k+1\le k + 1 variant under the open interval is preserved as linear_upper_bound_clunie.

FormalConjectures/ErdosProblems/987.leanErdos987.erdos_987.variants.linear_upper_bound1 lineExact file
x, ∃ (_ : ∀ (j : ℕ), x jSet.Ico 0 1), ∀ (k : ℕ), 1 ≤ kErdos987.A x k ≤ ↑↑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.

Search problems.science

Find a Problem, Result, source, or page