Back to Problems

erdos_1064

Specification

Let $ϕ(n)$ be the Euler's totient function, then the $n$ satisfies $ϕ(n)>ϕ(n - ϕ(n))$ have asymptotic density 1. Reference: [LuPo02] Luca, Florian and Pomerance, Carl, On some problems of {M}\polhk akowski-{S}chinzel and {E}rd\H os concerning the arithmetical functions {$\phi$} and {$\sigma$}. Colloq. Math.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement
theorem erdos_1064 : {n | φ n > φ (n - φ n)}.HasDensity 1
ID: ErdosProblems__1064__erdos_1064
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

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