If $n! = i \prod p_{i}^{k_{i}}$ is the factorisation into distinct primes then let $h (n)$ count the number of distinct exponents $k_{i}$ . Prove that there exists some $c > 0$ such that $h (n) \sim c (\frac{n}{lo g n})^{1/2}$ as $n \to \infty$ .

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

## This is (still) an open Erdős–Selfridge problem

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

AMS 11 · solved (literature)

theorem erdos_912.variants.selfridge :
    (fun n => (h n : ℝ)) =Θ[atTop] (fun n => (n / Real.log n) ^ (1 / 2 : ℝ))

open