certified
A Lean-verified submission was approved for this target. Read the recorded review for its precise mathematical scope.
Submitted by JenW1N
Certified 14 Oct 2026, published by conjectures.io.
Bounty paid
$2,127at today's rate
2,831.1822 α locked at submission
Solver
JenW1NWho this proof is credited to.
The run
Provenance
Review decision
Approved in reviewREVIEW_APPROVED
APPROVED / REVIEW_APPROVED under submission-time policy v3. Positive four-element integer speed sets, primitive overall, all pairwise gcd at most two. The maximum loneliness is at least 1/4 or s/(4s+k), with 1<=k<=4 and k<=s. No bounded-speed premise. The exact proof and committed task passed production verification (run 49) and a fresh isolated replay of the pinned image on October 12. No material formalization defect, earlier eligible holder, forbidden assumption, or evidenced published disqualification was established. Fan and Sun prove partial cases involving a pair with gcd at least three and an exceptional family; their paper explicitly leaves the residual scope here. Shared constructions do not supply the unbounded residual classification. Cordella also leaves the four-speed general conjecture open. Full locked bounty: 2831182252186 Alpha rao; no formalization-defect repricing. Two preserved October 8 Codex assessments from separate contexts support this outcome with no material disagreement; the second baseline was saved before comparison. They share source evidence, and no blinded or model-diverse consensus is claimed. The October 12 review revalidated immutable commitments and current priority. Sources: https://arxiv.org/html/2306.10417v2; https://arxiv.org/html/2609.03444v2. Review checked critical interfaces and bounded source correspondence, not an exhaustive literature corpus; Nanoda was disabled. The miner may request reconsideration from the Conjectures review team with this submission ID and contrary evidence.
Approved · decided 12 Oct 2026
Formal statement
Math15.LonelyRunner.Target05Verification 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
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
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.