certified
Green's open problem 47
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) PThe proof
This proof was approved in review, so the file the kernel accepted is published in full.
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