947.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/947
[Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72.
[Er50] Erdős, P., On integers of the form $2^k+p$ and some related problems. Summa Brasil. Math. (1950), 113-123.

Imports (1)

theorem Erdos947.erdos_947 sorry line 51 source
depends on sorry what this means
Statement uses: Not, Exists, StrictCoveringSystem, Int, Pairwise, CoveringSystem.ι, StrictCoveringSystem.toCoveringSystem, Function.onFun, Set, Disjoint, CoveringSystem.coset
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.