955.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

13 declarations, 7 contain sorry, 0 declared as axioms

Erdős Problem 955

References:

erdosproblems.com/955
[EGPS90] Erdős, P. and Granville, A. and Pomerance, C. and Spiro, C., On the normal behavior of the iterates of some arithmetic functions. Analytic number theory (Allerton Park, IL, 1989) (1990), 165-204.
[Er73b] Erdős, P., Über die Zahlen der Form $\sigma(n) - n$ und $n - \phi(n)$. Elem. Math. (1973), 83--86.
[Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
[PPT18] Pollack, Paul and Pomerance, Carl and Thompson, Lola, Divisor-sum fibers. Mathematika (2018), 330--342.
[Po14b] Pollack, Paul, Some arithmetic properties of the sum of proper divisors and the sum of prime divisors. Illinois J. Math. (2014), 125--147.
[PoPo16] Pollack, Paul and Pomerance, Carl, Some problems of Erdős on the sum-of-divisors function. Trans. Amer. Math. Soc. Ser. B (2016), 1--26.
[Tr15] Troupe, Lee, On the number of prime factors of values of the sum-of-proper-divisors function. J. Number Theory (2015), 120--135.
[Tr20] Troupe, Lee, Divisor sums representable as the sum of two squares. Proc. Amer. Math. Soc. (2020), 4189--4202.

Imports (1)

FormalConjecturesUtil

def Erdos955.s Let $s(n)=\sigma(n)-n=\sum_{\substack{d\mid n\\ d<n}}d$ be the sum of proper divisors function line 53 source
Source documentation
Let $s(n)=\sigma(n)-n=\sum_{\substack{d\mid n\\ d<n}}d$ be the sum of proper divisors function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HSub.hSub, ArithmeticFunction, ArithmeticFunction.sigma, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def s (n : ℕ) : ℕ := σ 1 n - n
…
```
theorem Erdos955.s_one line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos955.s, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos955.s_two line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos955.s, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos955.s_six line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos955.s, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos955.s_twelve line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos955.s, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos955.s_twenty_eight line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos955.s, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos955.erdos_955 If $A\subset \mathbb{N}$ has density $0$ then $s^{-1}(A)$ must also have density $0$ sorry line 76 source
Source documentation
If $A\subset \mathbb{N}$ has density $0$ then $s^{-1}(A)$ must also have density $0$.
A conjecture of Erdős, Granville, Pomerance, and Spiro [EGPS90].

depends on sorry what this means
Statement uses: Iff, True, Set, Nat, Set.HasDensity, OfNat.ofNat, Real, Set.univ, Set.ofPred, Membership.mem, Erdos955.s
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_955 :
    answer(sorry) ↔
      ∀ A : Set ℕ, A.HasDensity 0 → { x | s x ∈ A }.HasDensity 0 := by
…
```
Mentions: Erdos955.s
theorem Erdos955.erdos_955.variants.positive_density It is possible for $s(A)$ to have positive density even if $A$ has zero density (for example taking $A$ to be the product of two distinct primes) sorry line 86 source
Source documentation
It is possible for $s(A)$ to have positive density even if $A$ has zero density (for example taking $A$ to be the product of two distinct primes).

depends on sorry what this means
Statement uses: Exists, Set, Nat, And, Set.HasDensity, OfNat.ofNat, Real, Set.univ, GT.gt, Set.image, Erdos955.s
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_955.variants.positive_density :
    ∃ A : Set ℕ, A.HasDensity 0 ∧ (∃ d > 0, (s '' A).HasDensity d) := by
…
```
Mentions: Erdos955.s
theorem Erdos955.erdos_955.variants.empty_preimage Erdős [Er73b] proved that there are sets $A$ of positive density such that $s^{-1}(A)$ is empty sorry line 99 source
Source documentation
Erdős [Er73b] proved that there are sets $A$ of positive density such that $s^{-1}(A)$ is empty.
Here "positive density" means positive lower density: Erdős proved that the set of untouchable numbers (those not of the form $s(n)$) has positive lower density [Er73b, Satz I]. Pollack and Pomerance [PoPo16] conjecture that this set has a natural density and give a heuristic for its value. The same result is stated as erdos_418.variants.sigma in Erdős Problem 418.

depends on sorry what this means
Statement uses: Exists, Set, Nat, And, LT.lt, Real, OfNat.ofNat, Set.lowerDensity, Set.univ, Eq, Set.ofPred, Membership.mem, Erdos955.s, EmptyCollection.emptyCollection
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_955.variants.empty_preimage :
    ∃ A : Set ℕ, 0 < A.lowerDensity ∧ { x | s x ∈ A } = ∅ := by
…
```
Mentions: Erdos955.s
theorem Erdos955.erdos_955.variants.pollack_primes Pollack [Po14b] has shown that this is true if $A$ is the set of primes sorry line 107 source
Source documentation
Pollack [Po14b] has shown that this is true if $A$ is the set of primes.

depends on sorry what this means
Statement uses: Set.HasDensity, Nat, Set.ofPred, Nat.Prime, Erdos955.s, OfNat.ofNat, Real, Set.univ
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_955.variants.pollack_primes :
    { x | Nat.Prime (s x) }.HasDensity 0 := by
…
```
Mentions: Erdos955.s
theorem Erdos955.erdos_955.variants.troupe_unusually_many_prime_factors Troupe [Tr15] has shown that this is true if $A$ is the set of integers with unusually many prime factors sorry line 116 source
Source documentation
Troupe [Tr15] has shown that this is true if $A$ is the set of integers with unusually many prime factors.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Set.HasDensity, Nat, Set.ofPred, LT.lt, HMul.hMul, HAdd.hAdd, Real.log, Erdos955.s, ArithmeticFunction, ArithmeticFunction.cardDistinctFactors, Set.univ
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_955.variants.troupe_unusually_many_prime_factors :
    ∀ ε > 0, { x | (1 + ε) * Real.log (Real.log (s x)) <
      (ArithmeticFunction.cardDistinctFactors (s x) : ℝ) }.HasDensity 0 := by
…
```
Mentions: Erdos955.s
theorem Erdos955.erdos_955.variants.troupe_sum_of_two_squares Troupe [Tr20] has also shown this is true if $A$ is the set of integers which are the sum of two squares sorry line 126 source
Source documentation
Troupe [Tr20] has also shown this is true if $A$ is the set of integers which are the sum of two squares.

depends on sorry what this means
Statement uses: Set.HasDensity, Nat, Set.ofPred, Exists, Eq, Erdos955.s, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Real, Set.univ
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_955.variants.troupe_sum_of_two_squares :
    { x | ∃ a b : ℕ, s x = a^2 + b^2 }.HasDensity 0 := by
…
```
Mentions: Erdos955.s
theorem Erdos955.erdos_955.variants.pollack_pomerance_thompson_bound Documented declaration: pollack_pomerance_thompson_bound sorry line 138 source
Source documentation
Pollack, Pomerance, and Thompson [PPT18] prove that if $\epsilon(x)=o(1)$ and $A\subset \mathbb{N}$ has size at most $x^{1/2+\epsilon(x)}$ then $\#\{ n\leq x: s(n)\in A\} =o(x)$ as $x\to \infty$. It follows that (using $s(n)\ll n\log\log n$) if $A$ grows like $\lvert A\cap [1,x]\rvert\leq x^{1/2+o(1)}$ then $s^{-1}(A)$ has density $0$.

depends on sorry what this means
Statement uses: Set, Nat, Real, Filter.Tendsto, Filter.atTop, nhds, OfNat.ofNat, Filter.Eventually, LE.le, Nat.count, Membership.mem, Classical.propDecidable, HPow.hPow, HAdd.hAdd, HDiv.hDiv, Set.HasDensity, Set.ofPred, Erdos955.s, Set.univ
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_955.variants.pollack_pomerance_thompson_bound :
    ∀ (A : Set ℕ) (ε : ℕ → ℝ),
      Tendsto ε atTop (𝓝 0) →
      (∀ᶠ n : ℕ in atTop, (count (· ∈ A) n : ℝ) ≤ (n : ℝ) ^ ((1 / 2 : ℝ) + ε n)) →
      { x | s x ∈ A }.HasDensity 0 := by
…
```
Mentions: Erdos955.s