certified
The accepted file establishes a result about a faulty formal statement. It does not settle the intended mathematical problem. The recorded review explains the mismatch.
Submitted by 5FqLp5…FfZZiK
Certified 6 Aug 2026, published by conjectures.io.
Review decision
Defect in the published taskFORMALIZATION_DEFECT_AWARD
Approved under FORMALIZATION_DEFECT_AWARD. The production verifier accepted the exact frozen Erdős 15 counterexample task, but the published Lean statement asks for summability over the rational numbers rather than convergence of the intended real-valued series. The miner validly refuted the task we published; this does not settle the informal Erdős problem. The validator therefore authorized the fixed $750 USD-equivalent formalization-defect award. It was paid as 1,044.286814577 Subnet 66 Alpha to hotkey 5FqLp5QmNRiHGyj3xbLVnDHfCx25qxJX5CUhpndF9GFfZZiK and finalized at chain event 8785036-19-218 on 2026-08-06 11:51:12 UTC.
Partial award · decided 25 Aug 2026
Formal statement
True ↔ Summable fun k => (-1) ^ (k + 1) * (↑k + 1) / ↑(Nat.nth Nat.Prime k)Verification 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