erdos_373.variants.of_lower_bound

Specification

Show that if `P(n(n−1)) > 4 log n` for large enough `n`, where `P(m)` denotes the largest prime factor of `m`, then the equation `n!=a_1!a_2!···a_k!`, with `n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k`, has only finitely many solutions.

Actions

Submit a Proof

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

Submit Proof

Lean 4 Statement

theorem erdos_373.variants.of_lower_bound
    (H : ∀ᶠ (n : ℕ) in Filter.atTop, 4*(n : ℝ).log < (n*(n-1 : ℕ)).maxPrimeFac) :
    S.Finite

ID: ErdosProblems__373__erdos_373.variants.of_lower_bound

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.