Erdős problem 427

Erdős Problem 427: is it true that, for every $n$ and $d$ , there exists $k$ such that $d \mid p_{n + 1} + \cdots + p_{n + k},$ where $p_r$ denotes the $r$ th prime?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

427.lean

Retained formal statement1 of 3

Erdős Problem 427: is it true that, for every $n$ and $d$ , there exists $k$ such that $d \mid p_{n + 1} + \cdots + p_{n + k},$ where $p_r$ denotes the $r$ th prime?

FormalConjectures/ErdosProblems/427.leanErdos427.erdos_4271 lineExact file

1True ↔ Erdos427.erdos427

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.