submission
Lean accepted this proof on 12 Oct 2026. What happens to it next is decided by people, and that decision is recorded below.
Provenance
Review decision
Already solved before this submissionNOT_NOVEL
Approval 52 is withdrawn for NOT_NOVEL by explicit reward-owner direction. A substantive complete public proof of Wilf's inequality for every numerical semigroup of embedding dimension four predates this submission. Source: https://github.com/kseth/wilf-e4/tree/caa574de768d15b5095284d97e9e272ba69973c1 . Public GitHub PushEvent 23118344264 dates that exact head to 2026-10-05 18:48:40 UTC; this submission was accepted on 2026-10-12 04:25:00.695378 UTC. Review matched the full target and hypotheses, inspected the manuscript and all 16 checkers, and reproduced input hashes, interval coverage, residual counts, and algebraic checks. No concrete proof gap was identified. The complete dynamic-programming predicates were not independently rerun; their full PASS replay is author-supplied, and the analytic argument was reviewed rather than kernel-certified. The prior result is supported by an inspectable proof and computational evidence, not merely an announcement. The original v3 policy required substantial source use for this prior-publication branch; the first review found that uncertain. This specifically authorized historical correction applies the owner's new prior-proof eligibility rule openly. Prospective policy v4 disqualifies an established earlier proof of the same direct problem even without Lean or source use. The accepted v3 record and original assessment are preserved; other approvals are not automatically reconsidered. The Lean verification remains VERIFIED. This decision concerns reward novelty and does not allege copying or misconduct. Unsigned payout instruction 37 is cancelled with its amount, destination, and history preserved; the target is on a reversible admission hold. Contrary evidence about the prior proof's validity, scope, or publication date can support reconsideration.
Rejected · decided 12 Oct 2026
Formal statement
Math30.Problem22Verification 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.
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice
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