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.«18»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Green18.green_18" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔
∀ α > 0,
∃ c > 0,
∃ m₀,
∀ (G : Type u_1) [inst : Group G] [inst_1 : Fintype G] [inst_2 : DecidableEq G] (A : Finset (G × G)),
Fintype.card G ≥ m₀ →
↑A.card ≥ α * ↑(Fintype.card G) ^ 2 → ↑(Green18.numNaiveCorners A) ≥ c * ↑(Fintype.card G) ^ 3Original conjecture source: FormalConjectures/GreensOpenProblems/18.lean
References
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 · 12 lemmas
Individual lemmas, special cases and supporting work, shown in their original scope.
9 Sept 2026