feat(GreensOpenProblems): 39

[jeangud]

Description

If $A \subset \mathbb{Z}/p\mathbb{Z}$ is random, $|A| = \sqrt{p}$, can we almost surely cover $\mathbb{Z}/p\mathbb{Z}$ with $100\sqrt{p}$ translates of $A$?

• Closes Green's Open Problems #39 #1595
• 🤖 First draft created with help from Gemini 3.1 Pro. I then modified it to handle edge cases, improved code modularity, added variants, and simple tests. I then asked Gemini to come up with non-trivial tests by enumeration.
• Formulation handles the 3 problem variants mentioned in Green's original comments.

Testing

✅ Builds successfully

$ lake build FormalConjectures/GreensOpenProblems/39.lean 
Build completed successfully (7982 jobs).

[mo271]

Thanks, looks mathematically correct to me, just some nits

[jeangud]

@mo271 thank you for the comments: addressed! ✅

I am hesitant to ask 🫣 but if you can spare the time, #2274 should also be ready for another look (despite the awaiting-author). No rush at all!

[mo271]

@mo271 thank you for the comments: addressed! ✅

I am hesitant to ask 🫣 but if you can spare the time, #2274 should also be ready for another look (despite the awaiting-author). No rush at all!

Thanks again!

Btw: you can remove the awaiting-author label by commenting

-awaiting-author

on a pr. We should document this better...

[jeangud]

@mo271 thank you for the comments: addressed! ✅
I am hesitant to ask 🫣 but if you can spare the time, #2274 should also be ready for another look (despite the awaiting-author). No rush at all!

Thanks again!

Btw: you can remove the awaiting-author label by commenting

-awaiting-author

on a pr. We should document this better...

🤯 Thank you for the pointer! Proposing #3934 if useful, please discard/close if not needed.