erdos_33.variants.vanDoorn

Specification

The smallest possible value of `lim sup n → ∞ |A ∩ {1, …, N}| / N^(1/2)` is at most `2φ^(5/2) ≈ 6.66`, with `φ` equal to the golden ratio. Proven by Wouter van Doorn.

Actions

Submit a Proof

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

Submit Proof

Lean 4 Statement

theorem erdos_33.variants.vanDoorn :
    ⨅ A : {A : Set ℕ | AdditiveBasisCondition A}, Filter.atTop.limsup (fun N =>
    (A.1.interIcc 1 N).ncard / (√N : EReal)) ≤ ↑(2 * (φ ^ ((5 : ℝ) / 2)))

ID: ErdosProblems__33__erdos_33.variants.vanDoorn

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

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