1187.lean`

2 declarations, 2 contain sorry, 0 declared as axioms

References:

erdosproblems.com/1187
[Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
[GrTa08] Green, Ben and Tao, Terence, The primes contain arbitrarily long arithmetic progressions. Ann. of Math. (2) (2008), 481-547.

Imports (1)

theorem Erdos1187.erdos_1187.parts.i sorry line 47 source
depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Finite, Int, Exists, Set, And, Set.IsAPOfLength, ENat, Membership.mem, Nat.Prime, Eq
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos1187.erdos_1187.parts.ii sorry line 64 source
depends on sorry what this means
Statement uses: Iff, False, Nat, LE.le, OfNat.ofNat, Finite, Int, Exists, Set, And, Nat.Prime, Set.IsAPOfLengthWith, ENat, Membership.mem, Eq
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.