491.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/491
[Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254.
[Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79.
[Wi70] E. Wirsing, A characterization of $\log n$ as an additive arithmetic function. Symposia Math. (1970), 45-57.

Imports (1)

theorem Erdos491.erdos_491 sorry line 51 source
depends on sorry what this means
Statement uses: Iff, True, Nat, Real, GT.gt, OfNat.ofNat, Nat.Coprime, Eq, HMul.hMul, HAdd.hAdd, Exists, LT.lt, abs, HSub.hSub, Asymptotics.IsBigO, Filter.atTop, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.