Back to Problems

erdos_244.variants.Romanoff

Specification

Romanoff [Ro34] proved that the answer is yes if $C$ is an integer. [Ro34] Romanoff, N. P., _Über einige Sätze der additiven Zahlentheorie_. Math. Ann. (1934), 668-678.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement 
theorem erdos_244.variants.Romanoff {C : ℕ} (hC : 1 < C) :
    0 < { p + ⌊C ^ k⌋₊ | (p) (k) (_ : p.Prime) }.lowerDensity
ID: ErdosProblems__244__erdos_244.variants.Romanoff
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.