Skip to content

Erdős problem 830

Start work

We say that a,b∈Na,b\in \mathbb{N} are an amicable pair if σ(a)=σ(b)=a+b\sigma(a)=\sigma(b)=a+b. If A(x)A(x) counts the number of amicable 1≤a≤b≤x1\leq a\leq b\leq x then one can show that A(x)≤xexp⁡(−(12+o(1))(log⁡xlog⁡log⁡x)1/2)A(x) \leq x \exp(-(\tfrac{1}{2}+o(1))(\log x\log\log x)^{1/2}).

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

830.lean

Retained formal statement5 of 5

We say that a,b∈Na,b\in \mathbb{N} are an amicable pair if σ(a)=σ(b)=a+b\sigma(a)=\sigma(b)=a+b. If A(x)A(x) counts the number of amicable 1≤a≤b≤x1\leq a\leq b\leq x then one can show that A(x)≤xexp⁡(−(12+o(1))(log⁡xlog⁡log⁡x)1/2)A(x) \leq x \exp(-(\tfrac{1}{2}+o(1))(\log x\log\log x)^{1/2}).

FormalConjectures/ErdosProblems/830.leanErdos830.erdos_830.variants.pomerance_stronger3 linesExact file
∃ o,  o =o[Filter.atTop] 1 ∧    ∀ᶠ (x : ℝ) in Filter.atTop, Erdos830.A x ≤ x * Real.exp (-(1 / 2 + o x) * √(Real.log x * Real.log (Real.log x)))
SolvedStatement only, no proof