erdős #410
Let , the sum of divisors function, and . Is it true that for all
Worked, still open.
number theory · open · formalized (Lean) · 0 attempts
machinery: iterated-arithmetic-function,sum-of-divisors-sigma,abundancy-ratio-bound,normal-order-small-prime-factors,anatomy-of-integers,EGPS-iteration-framework,prime-distribution
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
* If you allow **(n=1)**, then it is **false**: (\sigma(1)=1), so (\sigma_k(1)=1) for all $k$ and (\sigma_k(1)^{1/k}=1).
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 · open (literature)
theorem erdos_410 : answer(sorry) ↔ ∀ n > 1,
Tendsto (fun k : ℕ ↦ ((sigma 1)^[k] n : ℝ) ^ (1 / (k : ℝ))) atTop atTopformal-conjectures/410.lean ↗oeis
links
status
open