Number theory

Erdős 416 - part i

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Does V(2x)/V(x)→2 ?

References

erdosproblems.com/416

No one has attempted this yet.

Formal statement

Lean type

Filter.Tendsto (fun x => Erdos416.V (2 * x) / Erdos416.V x) Filter.atTop (nhds 2)

What you must prove

import FormalConjectures.ErdosProblems.«416»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos416.erdos_416.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/416.lean

Source type SHA-256: sha256:e59204a269577064de274740a6a877339d25875f3f26f185d95133e79bbc2f70
Task id: fc-379fc029-parts-i-3edddfe88a-formalized-v1
Task commitment: sha256:f6322395ccaa8fe40ad3cde87658a407c9a223382ebd2f59b6f03bc8ab606ad8

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.