Documentation

FormalConjectures.ErdosProblems.«1061»

Erdős Problem 1061 #

References:

source
@[reducible, inline]
noncomputable abbrev Erdos1061.S (x : ℝ) :
ℝ

Let S x count the number of ordered pairs of positive integers (a, b) with a + b ≤ x such that σ(a) + σ(b) = σ(a + b), where σ is the sum of divisors function.

In particular, (a, b) and (b, a) are counted separately; an unordered variant could be obtained by additionally requiring a ≤ b.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Erdos1061.erdos_1061 :
    sorry ↔ ∃ (c : ℝ), 0 < c ∧ Asymptotics.IsEquivalent Filter.atTop S fun (x : ℝ) => c * x

    How many (ordered) solutions are there to σ(a) + σ(b) = σ(a + b) with a + b ≤ x? Is it true that this number is asymptotic to c * x for some constant c > 0?