erdős #822
Does the set of integers of the form have positive (lower) density?
Worked, still open.
number theory · solved · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 11 · solved (literature)
theorem erdos_822 :
answer(True) ↔ (Set.range fun n => n + Nat.totient n).HasPosDensityformal-conjectures/822.lean ↗oeis
A121048 — a(n) = n + phi(n), where phi is the Euler totient function.2,3,5,6,9,8,13,12,15,14,21,16,25,20,23,24,33,24,37,28,33,32,45,32,45,38,45,40,57,38,61,48,53,50,59,48,73,56,63,56,81,54,A155085 — a(n) = n + sum of divisors of n.2,5,7,11,11,18,15,23,22,28,23,40,27,38,39,47,35,57,39,62,53,58,47,84,56,68,67,84,59,102,63,95,81,88,83,127,75,98,95,130,
status
solved