Conjectures.io

Combinatorics

Green33.green_33

Are there infinitely many qq for which there is a set A⊂Z/qZA \subset \mathbb{Z}/q\mathbb{Z}, ∣A∣=(2+o(1))q1/2|A| = (\sqrt{2} + o(1))q^{1/2}, with A+A=Z/qZA + A = \mathbb{Z}/q\mathbb{Z}? [Gr24]

References

  • [CaHa20] Caprace, Pierre-Emmanuel, and Pierre de la Harpe. "Groups with irreducibly unfaithful subsets for unitary representations." Confluentes Mathematici 12.1 (2020): 31-68.
  • [CrLe07] Croot, Ernie, and Vsevolod F. Lev. "Open problems in additive combinatorics." Additive combinatorics 43.207-233 (2007): 1.

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ (ε : ℝ), 0 < ε → ∃ᶠ (q : ℕ+) in Filter.atTop, ∃ A, A + A = Finset.univ ∧ |↑A.card / √↑↑q - √2| < ε

What you must prove

import FormalConjectures.GreensOpenProblems.«33»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green33.green_33" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/33.lean

Source type SHA-256
sha256:47220fa6ee4c5b7a3e11a18fd29683f9e3280055ba18709e222cab741e5cdd70
Task id
fc-379fc029-green33-green-33-e3e3dfe09b-formalized-v1
Task commitment
sha256:81204a7c6fae0cf040da3eaa1196be7b66ce5f90126cbaf2684c421d530dc46e

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.