Back to Problems

erdos_470.variants.abundancy_index

Specification

If there are no odd weird numbers then every weird number has abundancy index < 4.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement 
theorem erdos_470.variants.abundancy_index :
    (∀ n : ℕ, n.Weird → ¬Odd n) → ∀ n, n.Weird → AbundancyIndex n < 4
ID: ErdosProblems__470__erdos_470.variants.abundancy_index
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.