Back to Problems

erdos_1148.variants.weaker

Specification

[Va99] reports this is 'obvious' if we replace $\leq n$ with $\leq n+2\sqrt{n}$.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement 
theorem erdos_1148.variants.weaker : ∀ n, erdos_1148_weaker_prop n
ID: ErdosProblems__1148__erdos_1148.variants.weaker
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.