certified
Near density one half, the sumset A + A in a binary vector space contains a linear subspace of bounded codimension, with a bound depending only on the density parameter. This settles the half-density target, not Green's full extremal problem.
Submitted by JenW1N
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 proves the near-half-density case of Green’s Problem 51, formalized as Green51.green_51.one_half. For every fixed k > 0 and sufficiently large n, any subset A of 𝔽₂ⁿ with density greater than 1/2 − k/√n has a sumset A+A containing a linear subspace of codimension at most ⌈1 + 256e·k²⌉. This bound depends only on k, as required, and the linear-subspace conclusion is stronger than the requested affine-coset conclusion. The argument combines Boolean-cube separator estimates and Fourier analysis to control the directions missing from A+A. A polynomial interpolation argument then shows that these missing directions can be excluded by a bounded number of linear constraints. Their common kernel supplies the required subspace. The production verifier confirmed the exact statement and task commitment, built the challenge and solution, and accepted the proof with Lean’s kernel in the landrun+seccomp sandbox. A separate compilation in the pinned Lean environment also succeeded. The transitive axiom closure contained only propext, Quot.sound, and Classical.choice. Mathematical review found no material mismatch with the intended near-half-density question or exploitation of the formal definitions. Prior-art review examined Sanders’s “Green’s sumset problem at density one half,” subsequent related literature, public formalization records, and accessible recent announcements. Sanders proves a special case and explicitly asks the extension addressed here; the inspected sources did not establish an earlier solution substantially reproduced by this submission or an earlier completed target-specific formalization. Extended web, repository, registry, and social searches found no qualifying disqualifying evidence before the submission’s acceptance on 9 September 2026 at 01:00:04 UTC. Published problem: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf Prior work: https://arxiv.org/abs/1003.5649 Review criteria: https://github.com/conjectures-io/conjectures-validator/blob/main/docs/MANUAL_REVIEW_CRITERIA.md
Approved · decided 9 Sept 2026
Formal statement
True ↔
∀ (k : ℝ),
0 < k → ∃ c, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ α > 1 / 2 - k / √↑n, α ≤ 1 → n ≤ Green51.guaranteedMaxCosetDim n α + cVerification 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.
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
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice