certified
For a uniformly chosen set of floor(sqrt(p)) residues, the probability that at most 100 * floor(sqrt(p)) translates cover the cyclic group tends to zero. This refutes the published covering-probability target.
Submitted by Jordan
Certified 23 Sept 2026, published by conjectures.io.
Bounty paid
$2,260at today's rate
2,734.2271 α locked at submission
Solver
JordanWho this proof is credited to.
The run
Provenance
Review decision
Approved in reviewREVIEW_APPROVED
Green 39: APPROVED / REVIEW_APPROVED under policy v3 for the full locked bounty of 2734.227177984 Alpha. Production run 35 verified the exact committed proof and task. A fresh isolated replay on September 22, 2026 using the same verifier image also passed Lean, Comparator, statement equality, task integrity and allowed-axiom checks in 224.915 seconds; Nanoda was disabled. The submission proves that the native covering probability tends to zero for uniform floor(sqrt(p))-element sets and at most 100*floor(sqrt(p)) translates. Both probability limits and the source-certificate premise are discharged in the submitted proof. Stronger uniform linear-hole lemmas imply robustness to ceiling choices by an elementary coupling; that rounding extension is a reviewer deduction, not a separately Lean-checked theorem. No material statement mismatch, earlier eligible submission, qualifying prior solution, or supported disqualification was established. Bollobas-Janson-Riordan's cited results do not cover the required n approximately k^2 regime. Primary sources: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf and https://arxiv.org/pdf/0910.3815 . References to an unidentified frozen manuscript remain a provenance limitation, not established evidence of copying or prior resolution. The human operator explicitly approved this submission after receiving the re-review. The assessments and re-review came from the same Codex agent; multiple independent assessments were not completed and no independent consensus is claimed. The review is not an exhaustive literature search or complete line-by-line audit. The submitter may request reconsideration from the review team with contrary evidence, citing submission 4c981fff-af7e-4fc8-bb2e-9fe13fd7f632.
Approved · decided 22 Sept 2026
Formal statement
True ↔
Filter.Tendsto
(fun p =>
have k := (↑p).sqrt;
have c := 100 * k;
↑(Green39.proportionCoverable (↑p) k c))
Filter.atTop (nhds 1)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.
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