certified
Erdős 939
Certified 6 Aug 2026, published by conjectures.io.
- Bounty paid
- $718
- Verified
- 6 Aug 2026
- verifier validato
- Attribution
- conjectures.io
Review decision
- Decision code
- FORMALIZATION_DEFECT_AWARD
Lean verified the exact published task, but the formal predicate omits the intended requirement that the powerful numbers be positive. The submitted proof uses this omission in the r = 4 case by taking the set {0, 1}; zero is accepted by the encoded Nat.Full predicate, while it is not an admissible positive powerful number in the intended problem. Therefore the artifact proves the published Lean statement but does not settle the intended Erdős 939 conjecture. The submission receives the $750 USD-equivalent formalization-defect award in Subnet 66 Alpha instead of the displayed conjecture bounty.
APPROVED · decided 6 Aug 2026
Formal statement
True ↔ ∀ r ≥ 4, (Erdos939.Erdos939Sums r).NonemptyVerification report
- 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 42 s · Sandbox landrun+seccomp · Axioms permitted: propext, Quot.sound, Classical.choice
Provenance
- Task bundle
- sha256:2c68588e889c3bd7b9d1ba57f88ce2946432555d3748a7f62861661c03547a54
- Report digest
- sha256:f05d1949e3bcbfbe92955b3fcc8b0fc699ab69eef6a9d27fb720ea0a59e87b3a