Green's open problem 44

Sieve

[N]

by removing half the residue classes mod

p_i

, for primes

2 \leqslant p_1 < p_2 < \dots < p_{1000} < N^{9/10}

. Does the remaining set have size at most

\frac{1}{10} N

? We interpret "half the residue classes" as

\lfloor p_i / 2 \rfloor

Withdrawn 10 Sept 2026

PRIOR_EXTERNAL_FORMALIZATION (Green 44, also Erdos 1202, was resolved negatively by Price and GPT-5.4 Pro. The public plby/lean-proofs Erdos1202 counterexample predates pool admission; its unchanged source and an exact-target bridge were independently kernel-checked on September 9. See EXTERNAL-SOLUTIONS-2026-09-10.md for public sources.)

Formal statement

Proof target

import FormalConjectures.GreensOpenProblems.«44»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green44.green_44" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ (N : ℕ) (p : Fin 1000 → ℕ) (A : (i : Fin 1000) → Finset (ZMod (p i))),
    have remaining := {x ∈ Finset.Icc 1 N | ∀ (i : Fin 1000), ↑x ∉ A i};
    (∀ (i : Fin 1000), Nat.Prime (p i)) →
      StrictMono p → p 999 ^ 10 < N ^ 9 → (∀ (i : Fin 1000), (A i).card = p i / 2) → 10 * remaining.card ≤ N

Original conjecture source: FormalConjectures/GreensOpenProblems/44.lean

Task id: fc-8432eac9-green44-green-44-2629003ac1-formalized-v1
Task commitment: sha256:904ef8967f03c77ef2a49b0bcf6a62516b7b6451a208d74e3ebdfc2431f9042b

References

[Gr24] Ben Green's 100 Open Problems

[Er80] Erdős, Paul. "A survey of problems in combinatorial number theory." Annals of Discrete Mathematics 6 (1980): 89-115.

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