Erdős problem 830
We say that are an amicable pair if . If counts the number of amicable then one can show that .
Sources
FormalConjectures/ErdosProblems/
830.lean
Retained formal statement
We say that are an amicable pair if . If counts the number of amicable then one can show that .
∀ᶠ (x : ℝ) in Filter.atTop, Erdos830.A x ≤ x * Real.exp (-Real.nthRoot 3 (Real.log x))SolvedStatement only, no proof