Erdős problem 997 · problems.science

Is it true that, for every $\alpha$ , the sequence $\{ \alpha p_n\}$ is not well-distributed, if $p_n$ is the sequence of primes?

Sources

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

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

997.lean

Retained formal statement1 of 3

Is it true that, for every $\alpha$ , the sequence $\{ \alpha p_n\}$ is not well-distributed, if $p_n$ is the sequence of primes?

The answer is yes, by [APSSV26, Section 4]; a Lean formalisation is available in [Mo26].

FormalConjectures/ErdosProblems/997.leanErdos997.erdos_9971 lineExact file

1True ↔ ∀ (α : ℝ), ¬Erdos997.IsWellDistributed fun n => Int.fract (α * ↑(Nat.nth Nat.Prime n))

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.