Values of n + φ(n)
DefinitionErdős Problem 822#✓fully proved
MathlibExt.NumberTheory.ErdosProblem822Wanted.conjecture
The statement that the set \(\{n + \varphi(n) : n \in \mathbb{N}\}\), where \(\varphi\) is Euler's totient function, has positive lower density in \(\mathbb{N}\).
def conjecture : Prop :=
0 < (Set.range fun n => n + Nat.totient n).lowerDensityUses 1 · Used by 1
Statement usesLower density
Used byErdős Problem 822 is true
TheoremErdős Problem 822 is true#●ready to prove
MathlibExt.NumberTheory.ErdosProblem822Wanted.conjecture_holds
The set \(\{n + \varphi(n) : n \in \mathbb{N}\}\), where \(\varphi\) is Euler's totient function, has positive lower density in \(\mathbb{N}\).
public theorem_wanted conjecture_holds : conjecturedef conjecture : Prop :=
0 < (Set.range fun n => n + Nat.totient n).lowerDensityWantedExt/NumberTheory/ErdosProblem822Wanted.lean:38
Sources
Sources
- M. R. Gabdullin, V. V. Iudelevich, and F. Luca, Numbers of the form k + f(k), Journal of Number Theory 262 (2024), 58–85, https://doi.org/10.1016/j.jnt.2024.03.010.
Uses 1
Statement usesErdős Problem 822
1 fully proved1 ready to prove
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.