Back to Problems

erdos_12.variants.erdos_sarkozy

Specification

Given any function $f(x)\to \infty$ as $x\to \infty$ there exists a set $A$ with the property that there are no distinct $a,b,c \in A$ such that $a \mid (b+c)$ and $b,c > a$, such that there are infinitely many $N$ such that \[\lvert A\cap\{1,\ldots,N\}\rvert > \frac{N}{f(N)}.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem erdos_12.variants.erdos_sarkozy (f : ℕ → ℕ) (hf : atTop.Tendsto f atTop) :
    ∃ A, IsGood A ∧ {N : ℕ | (N : ℝ) / f N < (A.interIcc 1 N).ncard}.Infinite
ID: ErdosProblems__12__erdos_12.variants.erdos_sarkozy
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.