Back to Problems

firoozbakht_conjecture_consequence

Specification

The inequality $p_{n+1}-p_n < (\log p_n)^2-\log p_n$ holds for all $n>4$. A consequence of Firuzbakht's conjecture.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement 
theorem firoozbakht_conjecture_consequence (n : ℕ) (hn : 3 < n) (P : type_of% firoozbakht_conjecture) :
    (n+1).nth Prime - n.nth Prime < (log (n.nth Prime))^2 - log (n.nth Prime)
ID: Wikipedia__Firoozbakht__firoozbakht_conjecture_consequence
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.