ErdosProblems · textbook · AMS 11

mediumknown result, no worker yet

Erdős Problem 1054

Theorem 1054 · Erdős

Let f(n)f(n) be the minimal integer mm such that nn is the sum of the kk smallest divisors of mm for some k≥1k\geq 1. Show that ff is undefined at n=2n=2, i.e. we get the junk value 00.

Formal statement · Lean 4.lean
theorem f_undefined_at_2 : f 2 = 0 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗