certified
The limiting lower covering density of radius-two linear codes is f(2) = 1. This establishes the radius-two target, not the separate question about growing covering radius.
Submitted by JenW1N
Certified 17 Sept 2026, published by conjectures.io.
Review decision
Approved in reviewREVIEW_APPROVED
Green 40, f(2)=1: APPROVED / REVIEW_APPROVED, policy v3. Submission accepted 2026-09-15 19:25:16.587283+00:00. The exact accepted proof and task passed production verification. The target is the radius-two linear-code covering-density liminf f(2)=1. The proof constructs linear kernel codes along diverging lengths and combines an upper bound approaching one with the sphere-covering lower bound. This establishes the committed target; it does not resolve the separate behavior as the covering radius grows. The cited earlier contribution proves only the lower bound and a reduction, not the exact target. No material task defect, earlier eligible target holder, or published disqualification was established. Approved for the full locked bounty of 4,342.552883665 Alpha; no formalization-defect award applies. Two independent agent assessments, covering formal semantics/integrity and prior-source eligibility, agree with this outcome; no material disagreement required resolution. They used separate contexts of the same model family. No fresh Lean replay was performed. Sources: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf ; https://github.com/conjectures-io/conjectures-contribution/tree/93c77e1b15f5a7ca22bd1b777a26bcc51d3b247e/contributions/green-40-f-two-eq-one/61648655993994f3bfd0ae9b44322f5541653c3d63d5c284213e49162addebe5. The miner may request reconsideration from the review team, citing submission 8186c13b-077f-45bb-8702-870f1dab27e3 and providing contrary evidence.
Approved · decided 16 Sept 2026
Formal statement
True ↔ Green40.f 2 = 1Verification 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