586.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/586
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[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.
[Er97] Erdős, Paul, Problems in number theory. New Zealand J. Math. (1997), 155-160.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67.
[Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537.
[BBMST22] Balister, Paul and Bollobás, Béla and Morris, Robert and Sahasrabudhe, Julian and Tiba, Marius, On the Erdős covering problem: the density of the uncovered set. Invent. Math. (2022), 377-414.

Imports (1)

theorem Erdos586.erdos_586 sorry line 54 source
depends on sorry what this means
Statement uses: Iff, False, Exists, CoveringSystem, Int, Pairwise, CoveringSystem.ι, Not, LE.le, Ideal, CoveringSystem.moduli
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
15 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.