Number theory

Green's open problem 47

Suppose that a large sieve process leaves a set of quadratic size. Is that set quadratic? The following very particular instance is probably the simplest [Gr24]: Suppose that

A \subset \mathbb{N}

is a set with the property that

|A \pmod p| \leqslant \frac{1}{2}(p + 1)

for all sufficiently large

p

. Is it true that either

|A \cap [X]| \ll X^{1/2} / \log^{100} X

, or

A

is contained in the image of

\mathbb{Z}

under a quadratic map

\phi : \mathbb{Q} \to \mathbb{Q}

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.«47»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green47.green_47" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ (A : Set ℕ),
    (∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ((fun a => ↑a) '' A).ncard ≤ (p + 1) / 2) →
      ((fun X => ↑(A ∩ Set.Iic X).ncard) =O[Filter.atTop] fun X => √↑X / Real.log ↑X ^ 100) ∨
        ∃ P, P.degree = 2 ∧ ∀ a ∈ A, ∃ z, ↑a = Polynomial.eval (↑z) P

Original conjecture source: FormalConjectures/GreensOpenProblems/47.lean

Source type SHA-256: sha256:478085e193f4b867ece2a9d656977157d85b9b785d1b0819fec86f218a23d78c
Task id: fc-v2-green47-green-47-e7065d1c45ae5ffa3c1f7473-formalized
Task commitment: sha256:476d068ba296a1e78aa6d7b4197b557caa2765b492bca6f2f342fd3736569f9d

References

[Gr24] Ben Green's 100 Open Problems

[GH14] Green, Ben, and Adam J. Harper. "Inverse questions for the large sieve." Geometric and Functional Analysis 24.4 (2014): 1167-1203.
[HV09] Helfgott, Harald Andrés, and Akshay Venkatesh. "How small must ill-distributed sets be." Analytic number theory 2 (2009): 224-234.
[Wa12] Walsh, Miguel N. "The inverse sieve problem in high dimensions." (2012): 2001-2022.
[Wa14] Walsh, Miguel N. "The algebraicity of ill-distributed sets." Geometric and Functional Analysis 24.3 (2014): 959-967.

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