erdos_830.parts.ii

Specification

**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)}?\]

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem erdos_830.parts.ii : answer(sorry) ↔ ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧ ∀ᶠ x in atTop,
    x ^ (1 - o x) < A x

ID: ErdosProblems__830__erdos_830.parts.ii

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.