Conjectures.io

Combinatorics

Green32.green_32

Let pp be a prime and let A⊂Z/pZA \subset \mathbb{Z}/p\mathbb{Z} be a set of size ⌊p⌋\lfloor \sqrt{p} \rfloor. Is there a dilate of AA containing a gap of length 100p100\sqrt{p}?

References

  • [Sh20] Shakan, George. "A Large Gap in a Dilate of a Set." SIAM Journal on Discrete Mathematics 34.4 (2020): 2553-2555.

No one has attempted this yet.

Formal statement

Lean type

True ↔ Green32.HasLargeGapDilate fun p => √↑p

What you must prove

import FormalConjectures.GreensOpenProblems.«32»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green32.green_32" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/32.lean

Source type SHA-256
sha256:34a15fafb12e479ed77eb1f1d3d4de1aa95356f84654036449004d377aabe8be
Task id
fc-379fc029-green32-green-32-de5356479f-formalized-v1
Task commitment
sha256:e7d3c8eb5bff700e965e4454924617bd0c15df0033d4817fa00201d174334f39

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.