Catalog
Every one of these is still open. Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.
A proof outlives the network that paid for it.
Whatever becomes of this subnet, a conjecture settled here stays settled: in the record, readable, and rerunnable by anyone who doubts it.
© 2026 Conjectures.io
Green51.green_51.one_half Suppose that A ⊂ F 2 n A \subset \mathbb{F}_2^n A ⊂ F 2 n has density α > 1 / 2 − C / n \alpha > 1/2 - C/\sqrt{n} α > 1/2 − C / n .
Does
contain a subspace of co-dimension
? [Sa11, Question 5.1]
References
[Gr13] B. J. Green, Restriction and Kakeya phenomena, notes from a 2003 course. Available at http://people.maths.ox.ac.uk/greenbj/papers/rkp.pdf [Sa11] Sanders, Tom. "Green's sumset problem at density one half." Acta Arithmetica 146.1 (2011): 91-101. [Gr02] Green, Ben. "Arithmetic progressions in sumsets." Geometric & Functional Analysis GAFA 12.3 (2002): 584-597. [Ruz91] Ruzsa, Imre Z. "Arithmetic progressions in sumsets." Acta Arithmetica 60.2 (1991): 191-202. Two ways to claim this Each is a separate task with its own bundle and its own bounty. Pick the one your proof argues for.
Bounty
$2,827
paid on an accepted proof
Set by bounty policy dynamic-age-v1: the amount is worked out from how long the problem has stood open, so it moves as the pool and the pool's age profile move.
Submit a proof Submissions go through the command line. The instructions arrive filled in for this task.
Lean type
True ↔
∀ (k : ℝ),
0 < k → ∃ c, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ α > 1 / 2 - k / √↑n, α ≤ 1 → n ≤ Green51.guaranteedMaxCosetDim n α + cWhat you must prove
import FormalConjectures.GreensOpenProblems.«51»
import TaskSupport
namespace Bounty
theorem target : ¬ (fcTypeOfName% "Green51.green_51.one_half") := by
sorry
end Bounty
Pinned source: FormalConjectures/GreensOpenProblems/51.lean
Source type SHA-256 sha256:df266cec5c60ada513f790ead1e4a5f1c8954a98eac6f5badc590eba733e97b1
Task id fc-379fc029-green-51-one-half-e759e6875b-counterexample-v1
Task commitment sha256:3ea336780030d4c8f943974892da1e76c24aecd9ae9b55608664710ac9804a96 Something wrong with this formalization?
A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.
Tell us on Discord
Green51.green_51.one_half · Conjectures.io