Combinatorics

Green's open problem 39

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

? [Gr24]

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.GreensOpenProblems.«39»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green39.green_39" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  Filter.Tendsto
    (fun p =>
      have k := (↑p).sqrt;
      have c := 100 * k;
      ↑(Green39.proportionCoverable (↑p) k c))
    Filter.atTop (nhds 1)

Original conjecture source: FormalConjectures/GreensOpenProblems/39.lean

Source type SHA-256: sha256:d8c0cb751eaf5d2498d0c7acc2225a74b6751efaf4828398f274e41553ce6f1b
Task id: fc-v2-green39-green-39-f72e918955b7f8891b4df047-formalized
Task commitment: sha256:393d44be9d9a360e808279fbee14920a3564ac6a5e72f67f56e38f7280046000

References

[Gr24] Green, Ben. "100 open problems." (2024).
[BJR11] Bollobás, Béla, Svante Janson, and Oliver Riordan. "On covering by translates of a set." Random Structures & Algorithms 38.1‐2 (2011): 33-67.

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.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord