Erdős problem 830 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

830.lean

Retained formal statement2 of 5

Erdos Problem 830, Part 2 We say that $a,b\in \mathbb{N}$ are an amicable pair if $\sigma(a)=\sigma(b)=a+b$ . If $A(x)$ counts the number of amicable $1\leq a\leq b\leq x$ then is it true that $A(x) > x^{1-o(1)}?$

FormalConjectures/ErdosProblems/830.leanErdos830.erdos_830.parts.ii1 lineExact file

1sorry ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, x ^ (1 - o x) < Erdos830.A x

OpenStatement only, no proof

Sources

Search problems.science