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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/997.lean

Formal Conjectures

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.

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

AI alongside literature
Erdős AI contributions wiki · 31 Mar, 2026
Machine
OpenAI internal model
Open the source record
Formalization
Erdős AI contributions wiki · 1 Apr, 2026
Machine
Aristotle
Open the source record
argument
VibeMathed
Machine
OpenAI internal model
People
Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, Gregory Valiant
Reported outcome
resolved
Open the source record