Erdős 10 - grechuk

Decision code

REVIEW_APPROVED

Lean verified the exact published Grechuk task. The proof faithfully establishes infinitely many even natural numbers that cannot be written as a prime plus at most three powers of two, using the Crocker covering-congruence construction. Although the underlying number-theoretic construction predates this submission, the result was not already available in the pinned Lean environment and no copying, misattribution, or other v1 disqualification was established. The submission earns the displayed conjecture bounty.

APPROVED · decided 6 Aug 2026

• ✓Manifest validpassed
• ✓Task commitment matchespassed
• ✓Production taskpassed
• ✓Production sandboxpassed
• ✓Source type hash matchespassed
• ✓Trusted file hashes matchpassed
• ✓Submission policy respectedpassed
• ✓Challenge builtpassed
• ✓Solution builtpassed
• ✓Statement unchangedpassed
• ✓Only permitted axiomspassed
• ✓Lean kernel acceptedpassed
• -Nanoda enablednot passed
• -Nanoda acceptednot passed

Stage COMPLETED · Checked in 1 min 18 s · Sandbox landrun+seccomp · Axioms permitted: propext, Quot.sound, Classical.choice

Task bundle

sha256:75dae50947998fe526401998132fe589b236a539908bc9166e8f2b05d8a8f28f

Report digest

sha256:23494236c7a90578519d4686436297b6a8a08017deac8e18f8d686f96edffc37