Conjectures.io

Combinatorics

Green12.green_12

Let GG be an abelian group of size NN, and suppose that A⊂GA \subset G has density α\alpha. Are there at least α15N10\alpha^{15} N^{10} tuples (x1,…,x5,y1,…,y5)∈G10(x_1, \dots, x_5, y_1, \dots, y_5) \in G^{10} such that xi+yj∈Ax_i + y_j \in A whenever j∈{i,i+1,i+2}j \in \{i, i+1, i+2\}? Note: We interpret indices modulo 5.

References

No one has attempted this yet.

Formal statement

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 ^ 10

What you must prove

import FormalConjectures.GreensOpenProblems.«12»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green12.green_12" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/12.lean

Source type SHA-256
sha256:03ec075d26bd8f703eaf9c9734b182c8d67afc5948b8e208824c4460cde39d46
Task id
fc-379fc029-green12-green-12-cae949d0e1-formalized-v1
Task commitment
sha256:db038ff9e8a00661039435dc0ff6c7aa196a7969e57ad986157f8cd9e13dbb0a

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.