Conjectures.io

Combinatorics

Green18.green_18

Suppose that GG is a finite group, and let A⊂G×GA \subset G \times G be a subset of density α\alpha. Is it true that there are ≫α∣G∣3\gg_\alpha |G|^3 triples x,y,gx, y, g such that (x,y),(gx,y),(x,gy)(x, y), (gx, y), (x, gy) all lie in AA? Note: A is taken as α\alpha-dense, i.e. ∣A∣≥α∣G∣2|A| \ge \alpha |G|^2 [Au16, Question 2]

References

  • [Au16] Austin, Tim. "Ajtai–Szemerédi theorems over quasirandom groups." Recent trends in combinatorics. Cham: Springer International Publishing, 2016. 453-484.
  • [So13] Solymosi, Jozsef. "Roth-type theorems in finite groups." European Journal of Combinatorics 34.8 (2013): 1454-1458.
  • [Go01] Gowers, William T. "A new proof of Szemerédi's theorem." Geometric & Functional Analysis GAFA 11.3 (2001): 465-588.

No one has attempted this yet.

Formal statement

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) ^ 3

What you must prove

import FormalConjectures.GreensOpenProblems.«18»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green18.green_18" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/18.lean

Source type SHA-256
sha256:5a31ee676aa0957a349062ecdb11dfccb340dc34ec96516418e8eed3f7e9c9d0
Task id
fc-379fc029-green18-green-18-1150586578-formalized-v1
Task commitment
sha256:3df78339cf1b181306b3249bcd8f8588b7054a3feb4e2a0575238a9eca1226cb

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.