Back to Problems

odd_perfect_number.lower_bound

Specification

A known result: If an odd perfect number exists, it must be greater than $10^{1500}$ and must have at least 101 prime factors (including multiplicities). Reference: Pascal Ochem, Michaël Rao (2012). "Odd perfect numbers are greater than 10^1500"

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement 
theorem odd_perfect_number.lower_bound (n : ℕ) (hn : Odd n) (hp : Perfect n) :
    n > 10^1500 ∧ (n.primeFactorsList).length ≥ 101
ID: Other__OddPerfectNumber__odd_perfect_number.lower_bound
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.