47.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/47
[Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. (1992), 34-50.
[Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186.
[Er96b] Erdős, Paul, Some problems I presented or planned to present in my short talk. Analytic number theory, Vol. 1 (Allerton Park, IL, 1995) (1996), 333-335.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67.
[Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021).
[LiSa24] Liu, Y. and Sawhney, M., On further questions regarding unit fractions. arXiv:2404.07113 (2024).

Imports (1)

theorem Erdos47.erdos_47 sorry line 57 source
depends on sorry what this means
Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Finset, LE.le, Finset.Icc, HMul.hMul, Real.log, Finset.reciprocalSum, Exists, And, Eq, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.