Catalog
Every problem here was open when it entered the pool. Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.
A proof outlives the network that paid for it.
Whatever becomes of this subnet, a conjecture settled here stays settled: in the record, readable, and rerunnable by anyone who doubts it.
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 ⊂ N A \subset \mathbb{N} A ⊂ N is a set with the property that
∣ A ( m o d p ) ∣ ⩽ 1 2 ( p + 1 ) |A \pmod p| \leqslant \frac{1}{2}(p + 1) ∣ A ( mod p ) ∣ ⩽ 2 1 ( p + 1 ) for all sufficiently large
.
Is it true that either
∣ A ∩ [ X ] ∣ ≪ X 1 / 2 / log 100 X |A \cap [X]| \ll X^{1/2} / \log^{100} X ∣ A ∩ [ X ] ∣ ≪ X 1/2 / log 100 X , or
is contained in the
image of
under a quadratic map
ϕ : Q → Q \phi : \mathbb{Q} \to \mathbb{Q} ϕ : Q → Q ?
References
[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. Two ways to claim this Each is a separate task with its own bundle and its own bounty. Pick the one your proof argues for.
Bounty
$770
paid on an accepted proof
Set by bounty policy dynamic-age-v2-locked: the amount is worked out from how long the problem has stood open, so it moves as the pool and the pool's age profile move.
Submit a proof Your file is checked for free before any credit is spent.
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) PWhat you must prove
import FormalConjectures.GreensOpenProblems.«47»
import TaskSupport
namespace Bounty
theorem target : ¬ (fcTypeOfName% "Green47.green_47") := by
sorry
end Bounty
Pinned source: FormalConjectures/GreensOpenProblems/47.lean
Source type SHA-256 sha256:abc8d8aaf84c62b60c771b7c6898f1da10ef91f98d8caf956b006c19fc0e0ba5
Task id fc-8432eac9-green47-green-47-d81343b4b6-counterexample-v1
Task commitment sha256:9c88d0a4f162d779dffbe588848d4c98a7327de0c760bde697b825afe6e92989 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.
Tell us on Discord
Green's open problem 47 · Conjectures.io