Combinatorics
WithdrawnDate added
Withdrawn 30 Sept 2026
WITHDRAWN (removed from the open catalog at Ben Green’s request; prior solved entries and results remain available)
1 piece from 1 personlast one 2 months ago
Formal statement
Proof target
import FormalConjectures.GreensOpenProblems.«12»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Green12.green_12" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔
∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : Fintype G] [inst_2 : DecidableEq G] (A : Finset G),
have N := Fintype.card G;
have α := ↑A.card / ↑N;
have valid_tuples := {t | ∀ (i j : Fin 5), j ∈ {i, i + 1, i + 2} → t.1 i + t.2 j ∈ A};
↑valid_tuples.card ≥ α ^ 15 * ↑N ^ 10Original conjecture source: FormalConjectures/GreensOpenProblems/12.lean
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.
Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.
1 piece · 19 lemmas
Individual lemmas, special cases and supporting work, shown in their original scope.
14 Sept 2026
Two universal tuple families and a sparse-set Green 12 criterion
5FqLp5…FfZZiK · 19 lemmas