submission
Lean accepted this proof on 2 Nov 2026. What happens to it next is decided by people, and that decision is recorded below.
Review decision
Already solved before this submissionNOT_NOVEL
NOT_NOVEL: David Turturean's September 2026 manuscript gives an unconditional proof of Erdos 456(iii), publicly documented on September 23 before this submission's November 2 acceptance. Review of Section 4 and Appendix D found no material gap. Policy v4 excludes a later independent proof or first Lean formalization of an already solved target. No plagiarism finding is made. Prior manuscript: https://www.overleaf.com/read/fhqfmykkcmpb#7c626d . Public claim record: https://github.com/plasma-ai/erdos/blob/17c86a0d4ebe1487a087ceb8c14952a10ec2f2bd/wiki/problems/arithmetic_functions/E0456/claims/2026_09_23_turturean.md . Lean verification remains valid; this decision concerns reward eligibility.
Rejected · decided 2 Nov 2026
Formal statement
True ↔ {q | Nat.Prime q ∧ ∀ (n : ℕ), Erdos456.m n = q ↔ n = q - 1}.InfiniteVerification report
Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.
Manifest valid - Passed
The task bundle held together: the exact file set, a strict manifest, and every trusted hash matching the bytes on disk.
Task commitment matches - Passed
The bundle digest the submission committed to is the digest of the bundle that was actually verified.
Production task - Passed
The task came from the production pool rather than a test fixture.
Trusted file hashes match - Passed
The pinned dependencies agree across the manifest, the lockfile and the checkout, down to the same Formal Conjectures commit.
Submission policy respected - Passed
The submitted source passed the static scan: no imports, no axiom declarations, no sorry, no native_decide, no unsafe options.
Production sandbox - Passed
The run happened under real isolation, Landrun with seccomp, and the sandbox passed its own live self-test before the proof was touched.
Challenge built - Passed
The trusted Challenge.lean, which contains no miner code, compiled on its own.
Source type hash matches - Passed
The source theorem in the compiled environment still hashes to the type recorded in the task, so the statement has not drifted upstream.
Solution built - Passed
The submitted Solution.lean compiled.
Statement unchanged - Passed
The theorem the proof establishes has exactly the same canonical type as the task's target - it was not weakened or restated.
Only permitted axioms - Passed
The transitive axiom closure of the proof stays inside the axioms this task permits.
Lean kernel accepted - Passed
The Lean kernel replayed the proof and accepted it.
Nanoda accepted - Not run
A second kernel, written independently of Lean's, also accepted the proof.
One kernel, not two
This task does not require a second, independent kernel, so Nanoda was not run. The verdict rests on a single kernel implementation.
Theorems established
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice