feat(GreensOpenProblems): 32

[jeangud]

Description

Let $p$ be a prime and let $A \subset \mathbb{Z}/p\mathbb{Z}$ be a set of size $\lfloor \sqrt{p} \rfloor$. Is there a dilate of $A$ containing a gap of length $100\sqrt{p}$?

• Closes Green's Open Problems #32 #1588
• Added the different variants mentioned by Green in the comments.
• Tried making the code re-usable with HasGap, HasLargeGapDilate, and HasCosetHole which help express all the variants easily.
• Implemented with the help of Gemini 3.1 Pro 🤖 : generating a rough first draft, and then adjusting manually for style, simplicity/modularity, and fixing various edge cases.

Testing

• Builds successfully

$ lake build FormalConjectures/GreensOpenProblems/32.lean 
Build completed successfully (7975 jobs).

[mo271]

Thanks, LGTM, just some suggestions for more tests

[mo271]

Thanks again!