ErdosProblems · textbook · AMS 11
mediumknown result, no worker yet
Erdős Problem 1054
Theorem 1054 · Erdős
Let be the minimal integer such that is the sum of the smallest divisors of for some . Show that is undefined at , i.e. we get the junk value .
Formal statement · Lean 4.lean
theorem f_undefined_at_2 : f 2 = 0 := by
sorryProof. sorry
Nobody has tried yet.