Skip to content

Erdős problem 427

Erdős Problem 427: is it true that, for every nn and dd, there exists kk such that d∣pn+1+⋯+pn+k, d \mid p_{n + 1} + \cdots + p_{n + k}, where prp_r denotes the rrth prime?

How the state got here

1 of 6 recorded
  1. Prior stateNone retained
  2. WorkNo submitted work retained
  3. VerificationNo check retained
  4. DecisionNo Repository has decided
  5. StandingA Result stands here
  6. Next gapNot recorded

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

Exact provenance

Problem row
sha256:888d1b01937ec95afc4144f44c3bae1d573f5685bb24a3113d373e51114dcdaf
Metadata
sha256:af51f6c755074da414fe5ba4d1be8872b1efa7617c949ab6b3b43d053f6a7d6c
Observation
sha256:9c8326e865b6017b103af7611c852a06776d81964979b8ab5a1b800cd550dff6
Content
sha256:42e358fa10139722b1c19b18b03ae7800096e38bb01fe2efd5341e73568f4535
Repository
sha256:a956b84c437202e5a02cc9e036a621bd14a302b34a75758115730bdbb77c52a4
Projection
sha256:a4a96441668a9f8b33afbcb3f696a2639f5fae145f36ddc063d7f67d5fb87ce8
Source commit
36c6d0fef71a3fec84d9dcd5eeca4e22e378f7cb

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.

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