Back to Problems

selfridge_seq_conjecture.variants.sufficient_condition

Specification

Selfridge conjectured that the number of prime factors of the `n`-th Fermat number does not grow monotonically in $n$. A sufficient condition for this conjecture to hold is that there exists a Fermat prime larger than 65537.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement 
theorem selfridge_seq_conjecture.variants.sufficient_condition (n : ℕ) (hn : Prime n.fermatNumber)
    (hn' : n ≥ 5) : type_of% selfridge_seq_conjecture
ID: Wikipedia__Selfridge__selfridge_seq_conjecture.variants.sufficient_condition
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.