certified

Green's open problem 39

Certified 23 Sept 2026, published by conjectures.io.

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)

The proof

This proof was approved in review, so the file the kernel accepted is published in full.

Read the proof

Verification report

Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.

The task it was checked against

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.

The submission and the sandbox

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.

The trusted build

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.

The kernel's verdict

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

Bounty.target

Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice