certified
Green's open problem 24 - conjecture
Asymptotic variant proved
The asymptotic constant gamma equals 1/3. The submission completes the upper bound and credits the earlier lower-bound contribution. This establishes the asymptotic target, not the separate finite-size statement.
Submitted by JenW1N
- Lean verification:
- Passed
- Conjectures review:
- Approved
- Reward:
- Paid
Certified 2 Oct 2026, published by conjectures.io.
Review decision
Approved in reviewREVIEW_APPROVED
Approved for the full locked bounty. The September 23 submission passed all required Lean verification checks on the authorized extended retry. Review of the pinned statement found that it expresses the intended asymptotic conjecture Green24.variants.gamma = 1/3; the known issue with the sibling finite-size theorem does not affect this target. No qualifying earlier complete solution or earlier eligible reward holder was identified. Relevant prior work includes Aaronson's original conjecture (https://arxiv.org/abs/1801.07135), Korsky's weaker upper bound 47/122 (https://arxiv.org/abs/2609.02308), and the general reduction of Randjelovic, Shao, Xu, Zhang and Zhou (https://arxiv.org/abs/2609.06975). These do not resolve this exact target. The public September 17 lower-bound contribution is reused and credited, with 29 declarations matching after normalization: https://github.com/conjectures-io/conjectures-contribution/tree/main/contributions/green-24-variants-conjecture . The submission completes the upper bound needed for equality with 1/3. The operator explicitly approved acceptance following one advisory audit. This record does not claim that multiple independent agent assessments were completed.
Approved · decided 26 Sept 2026
Formal statement
Green24.variants.gamma = 1 / 3Verification 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