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?

Result history

Published changes, performers, checks, and later corrections.

No result history yet

No proposed change is retained for this Problem, so there is nothing to show a decision on.

Correction history

No correction history

Technical detailsExact roots, source, and retained record identifiers

Problem row: sha256:888d1b01937ec95afc4144f44c3bae1d573f5685bb24a3113d373e51114dcdaf
Metadata: sha256:af51f6c755074da414fe5ba4d1be8872b1efa7617c949ab6b3b43d053f6a7d6c
Observation: sha256:8c823d621b7e1256c8e47c60a5f1c54c016a5507e6f27b2bab537f6f5f232067
Content: sha256:42e358fa10139722b1c19b18b03ae7800096e38bb01fe2efd5341e73568f4535

Repository: sha256:a956b84c437202e5a02cc9e036a621bd14a302b34a75758115730bdbb77c52a4
Projection: sha256:c9d14c459c518937e758918b5897dc3b22f1a55f07739afe99502f5b046c907a
Source commit: 2415f78e850aeee50afdca525c6f2e0ea606f207

Upstream source Inspect records Source JSON

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

Result history

Correction history

Exact provenance

Source review

FormalConjectures/ErdosProblems/427.lean

Search problems.science