Erdős problem 427 · problems.science

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?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/427.lean

Formal Conjectures

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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:427
PLBY Lean proofsErdosProblems.Erdos427

Reported activity

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

Formalization
Erdős AI contributions wiki · 26 Apr, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

Source audit

Source review

1 exact matching record

Native pull-request state, mechanical checks, semantic findings, and artifact availability are separate source facts. None is a Vela Verification, Decision, or change to Math Standing.

Formal Conjectures PR #4884

FormalConjectures/ErdosProblems/427.lean

PR openreview review requiredsource audit: inconclusive

passproof

formal proof conditions retained

The formal_proof tuple is explicitly conditional and names its assumption.

Condition: The linked proof derives the result assuming Shiu's theorem.

Limit: This is a retained manual metadata review; it does not execute or compare the linked proof.

Open upstream PR Open Problem 427head 601aff40d6

Read-only projection

Approval and merge remain upstream PR state. A passing build does not establish semantic fidelity. An unavailable artifact identity is not a proof failure.

Adapter conformance 9 / 9: exact source revision, bounded complete reads, typed roots, custody, implementation identity, reconstructibility, unsupported-state refusal, rights, and lifecycle semantics.

Web read projection

sha256:ca753f3b6ad07fd62ef1035ae56de1646cb2133dd1705f991bf29a2bd7da2780

Math source projection

sha256:1a90cbe1732e21e730753a12e6b3b1ecbd3e0019a287a5ba001c9a9fdccf881b

Adapter profile

sha256:6491df603d880f00dc7e69cb0817fda1a0d903efee3812c5af3c7b3e02773303

Adapter contract

sha256:5de25828202d0682f8ac39c2e58e5d9ed7a3f0474910d77c1c4e641a08543615

Inspect exact Math projection

View complete five-record source audit