certified
Green's open problem 47
Exact-containment version disproved
A counterexample refutes the literal exact quadratic-containment statement. It does not refute the broader inverse large sieve conjecture allowing finitely many exceptions.
Submitted by JenW1N
- Lean verification:
- Passed
- Conjectures review:
- Approved
- Reward:
- Paid
The PDF is a working mathematical exposition. Lean verification applies to the formal source, not the prose.
Certified 9 Sept 2026, published by conjectures.io.
Review decision
Approved in reviewREVIEW_APPROVED
Approved under REVIEW_APPROVED pursuant to manual-review policy v2. The submission gives a counterexample to the exact-containment statement in Green47.green_47. It takes A = {2} ∪ {q² : q is prime and q ≡ 1 mod 8}. For every odd prime p, this set occupies at most (p+1)/2 residue classes, yet its counting function exceeds the proposed O(√X / log¹⁰⁰X) bound and it is not contained in the image of any rational quadratic polynomial on the integers. The proof establishes these properties using quadratic residues, primes in arithmetic progressions, and a finite-field moment identity. The production verifier accepted the exact counterexample statement and task commitment in the landrun+seccomp sandbox. A separate compilation of the submitted proof with the pinned Lean environment succeeded, and its transitive axiom closure contained only propext, Quot.sound, and Classical.choice. The counterexample faithfully refutes the particular exact-containment question published in Green’s Problem 47. It does not refute the broader Green– Harper inverse-sieve conjecture, which permits finitely many exceptions: removing the single element 2 leaves a set of squares. This distinction is present in the published mathematical formulations and does not establish a formalization defect. Prior-art review found no qualifying earlier solution substantially reproduced by the submission and no earlier completed, target-specific public formalization. Searches covered relevant literature, public repository discussions, and accessible indexed web and social sources; inaccessible, private, deleted, or unindexed material remains a limitation. No disqualifying evidence was established, supporting approval for the full bounty. Published problem: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf Broader conjecture: https://arxiv.org/abs/1311.6176 Review criteria: https://github.com/conjectures-io/conjectures-validator/blob/main/docs/MANUAL_REVIEW_CRITERIA.md
Approved · decided 9 Sept 2026
Formal statement
True ↔
∀ (A : Set ℕ),
(∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ((fun a => ↑a) '' A).ncard ≤ (p + 1) / 2) →
((fun X => ↑(A ∩ Set.Iic X).ncard) =O[Filter.atTop] fun X => √↑X / Real.log ↑X ^ 100) ∨
∃ P, P.degree = 2 ∧ ∀ a ∈ A, ∃ z, ↑a = Polynomial.eval (↑z) PVerification 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