FormalConjectures.ErdosProblems.«318»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 318

References:

erdosproblems.com/318

[ErSt75] Erdős, P. and Straus, E. G., Solution to Problem 387. Nieuw Arch. Wisk. (1975), 183.

[Sa75] Sattler, R., Solution to Problem 387. Nieuw Arch. Wisk. (1975), 184-189.

[Sa82b] Sattler, R., On Erdős property P₁ for the arithmetical sequence. Nederl. Akad. Wetensch. Indag. Math. (1982), 347--352.

[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

[La26] D. Larsen, Erdős problem 318 (2026)


open Set Real


namespace Erdos318

A set A : Set ℕ is said to have propery P₁ if for any nonconstant sequence f : A → {-1, 1}, one can always select a finite, nonempty subset S ⊆ A \ {0} such that ∑ n ∈ S, fₙ / n = 0. This is defined in [Sa82b].

def P₁ (A : Set ℕ) : Prop := ∀ (f : ℕ → ℝ),
  f ∘ (Subtype.val : (A \ {0} : Set ℕ) → ℕ) ≠ (fun _ => 1) →
  f ∘ (Subtype.val : (A \ {0} : Set ℕ) → ℕ) ≠ (fun _ => - 1) →
  Set.range f ⊆ {1, -1} →
  ∃ S : Finset ℕ, S.Nonempty ∧ ↑S ⊆ A \ {0} ∧ ∑ n ∈ S, f n / n = 0

ℕ has property P₁. This is proved in [ErSt75].

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_318.variants.univ : P₁ univ := by⊢ P₁ Set.univ
  sorryAll goals completed! 🐙

Sattler proved in [Sa75] that the set of odd numbers has property P₁.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_318.variants.odd : P₁ {n | Odd n} := by⊢ P₁ {n | Odd n}
  sorryAll goals completed! 🐙

The set of squares does not have property P₁.

@[category test, AMS 11]
theorem erdos_318.variants.squares : ¬ P₁ ({n | IsSquare n}) := by⊢ ¬P₁ {n | IsSquare n}
  simp only [P₁, not_forall, not_exists, not_and]⊢ ∃ x,
  ∃ (_ : x ∘ Subtype.val ≠ fun x => 1) (_ : x ∘ Subtype.val ≠ fun x => -1) (_ : range x ⊆ {1, -1}),
    ∀ (x_1 : Finset ℕ), x_1.Nonempty → ↑x_1 ⊆ {n | IsSquare n} \ {0} → ¬∑ n ∈ x_1, x n / ↑n = 0
  -- Consider the function `f` that sends `1` to `1` and sends all other numbers to `-1`.
  refine ⟨fun n => if n = 1 then 1 else - 1, fun h => ?_, fun h => ?_,
    fun x ⟨y, hy⟩ => ?_, fun S h hs => ?_⟩refine_1h:(fun n => if n = 1 then 1 else -1) ∘ Subtype.val = fun x => 1⊢ Falserefine_2h:(fun n => if n = 1 then 1 else -1) ∘ Subtype.val = fun x => -1⊢ Falserefine_3x:ℝx✝:x ∈ range fun n => if n = 1 then 1 else -1y:ℕhy:(fun n => if n = 1 then 1 else -1) y = x⊢ x ∈ {1, -1}refine_4S:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}⊢ ¬∑ n ∈ S, (fun n => if n = 1 then 1 else -1) n / ↑n = 0
  ·refine_1h:(fun n => if n = 1 then 1 else -1) ∘ Subtype.val = fun x => 1⊢ False have : (- 1 : ℝ) = 1 := by⊢ ¬P₁ {n | IsSquare n} simpa using congr_fun h ⟨4, ⟨⟨2, byh:(fun n => if n = 1 then 1 else -1) ∘ Subtype.val = fun x => 1⊢ 4 = 2 * 2 grindAll goals completed! 🐙⟩, byh:(fun n => if n = 1 then 1 else -1) ∘ Subtype.val = fun x => 1⊢ 4 ∉ {0} grindAll goals completed! 🐙⟩⟩
    grindAll goals completed! 🐙
  ·refine_2h:(fun n => if n = 1 then 1 else -1) ∘ Subtype.val = fun x => -1⊢ False have : 1 = (- 1 : ℝ) := by⊢ ¬P₁ {n | IsSquare n} simpa using congr_fun h ⟨1, ⟨IsSquare.one, byh:(fun n => if n = 1 then 1 else -1) ∘ Subtype.val = fun x => -1⊢ 1 ∉ {0} grindAll goals completed! 🐙⟩⟩
    grindAll goals completed! 🐙
  ·refine_3x:ℝx✝:x ∈ range fun n => if n = 1 then 1 else -1y:ℕhy:(fun n => if n = 1 then 1 else -1) y = x⊢ x ∈ {1, -1} by_cases x = 1posx:ℝx✝:x ∈ range fun n => if n = 1 then 1 else -1y:ℕhy:(fun n => if n = 1 then 1 else -1) y = xh✝:x = 1⊢ x ∈ {1, -1}negx:ℝx✝:x ∈ range fun n => if n = 1 then 1 else -1y:ℕhy:(fun n => if n = 1 then 1 else -1) y = xh✝:¬x = 1⊢ x ∈ {1, -1} <;>posx:ℝx✝:x ∈ range fun n => if n = 1 then 1 else -1y:ℕhy:(fun n => if n = 1 then 1 else -1) y = xh✝:x = 1⊢ x ∈ {1, -1}negx:ℝx✝:x ∈ range fun n => if n = 1 then 1 else -1y:ℕhy:(fun n => if n = 1 then 1 else -1) y = xh✝:¬x = 1⊢ x ∈ {1, -1} grindAll goals completed! 🐙
  -- Consider two cases: `1 ∈ S` or `1 ∉ S`. In the first case, the finite sum over `S` is bounded
  -- below by `1 - (π ^ 2 / 6 - 1)`, which is positive. In the second case, the finite sum over `S`
  -- is negative.
  by_cases h1 : 1 ∈ SposS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ ¬∑ n ∈ S, (fun n => if n = 1 then 1 else -1) n / ↑n = 0negS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∉ S⊢ ¬∑ n ∈ S, (fun n => if n = 1 then 1 else -1) n / ↑n = 0
  ·posS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ ¬∑ n ∈ S, (fun n => if n = 1 then 1 else -1) n / ↑n = 0 rw [Finset.sum_eq_add_sum_diff_singleton h1, Finset.sum_congr rfl
      (g := fun n : ℕ => (- 1 : ℝ) / n)]posS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ ¬(fun n => if n = 1 then 1 else -1) 1 / ↑1 + ∑ n ∈ S \ {1}, -1 / ↑n = 0posS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ ∀ x ∈ S \ {1}, (fun n => if n = 1 then 1 else -1) x / ↑x = -1 / ↑x
    ·posS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ ¬(fun n => if n = 1 then 1 else -1) 1 / ↑1 + ∑ n ∈ S \ {1}, -1 / ↑n = 0 simp only [↓reduceIte, Nat.cast_one, div_self one_ne_zero, ← ne_eq, div_eq_mul_one_div
        (- 1 : ℝ), ← Finset.mul_sum, neg_one_mul (∑ x ∈ S \ {1}, 1 / (x : ℝ)), ← sub_eq_add_neg]posS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ 1 - ∑ x ∈ S \ {1}, 1 / ↑x ≠ 0
      apply ne_of_gtpos.hS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ 0 < 1 - ∑ x ∈ S \ {1}, 1 / ↑x
      calc
      _ < 1 - (π ^ 2 / 6 - 1) := byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ 0 < 1 - (π ^ 2 / 6 - 1)
        have : π ^ 2 < 3.15 ^ 2 := byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ 0 < 1 - (π ^ 2 / 6 - 1) gcongrhabS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ π < 3.15; exact Real.pi_lt_d2All goals completed! 🐙
        linarithAll goals completed! 🐙
      _ = 1 - (∑' n : ℕ, 1 / (n : ℝ) ^ 2 - 1) := byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ 1 - (π ^ 2 / 6 - 1) = 1 - (∑' (n : ℕ), 1 / ↑n ^ 2 - 1) congre_a.e_aS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ π ^ 2 / 6 = ∑' (n : ℕ), 1 / ↑n ^ 2; exact hasSum_zeta_two.tsum_eq.symmAll goals completed! 🐙
      _ ≤ 1 - ∑ n ∈ S \ {1}, 1 / (n : ℝ) := byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ 1 - (∑' (n : ℕ), 1 / ↑n ^ 2 - 1) ≤ 1 - ∑ n ∈ S \ {1}, 1 / ↑n
        gcongrhS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ ∑ n ∈ S \ {1}, 1 / ↑n ≤ ∑' (n : ℕ), 1 / ↑n ^ 2 - 1
        have : 1 = 1 / ((1 : ℕ) : ℝ) := byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ 1 - (∑' (n : ℕ), 1 / ↑n ^ 2 - 1) ≤ 1 - ∑ n ∈ S \ {1}, 1 / ↑n norm_castS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ 1 = 1 / 1; grindAll goals completed! 🐙
        nth_rewrite 3 [this]hS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sthis:1 = 1 / ↑1 := 
  Eq.mpr
    (id
      (Eq.trans (congr (congrArg Eq (Eq.symm Nat.cast_one)) (congrArg (fun x => x / ↑1) (Eq.symm Nat.cast_one)))
        (congr (congrArg Eq Nat.cast_one) (congr (congrArg HDiv.hDiv Nat.cast_one) Nat.cast_one))))
    squares._proof_12⊢ ∑ n ∈ S \ {1}, 1 / ↑n ≤ ∑' (n : ℕ), 1 / ↑n ^ 2 - 1 / ↑1
        rw [le_sub_iff_add_le, ← Finset.sum_eq_sum_diff_singleton_add h1]hS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sthis:1 = 1 / ↑1 := 
  Eq.mpr
    (id
      (Eq.trans (congr (congrArg Eq (Eq.symm Nat.cast_one)) (congrArg (fun x => x / ↑1) (Eq.symm Nat.cast_one)))
        (congr (congrArg Eq Nat.cast_one) (congr (congrArg HDiv.hDiv Nat.cast_one) Nat.cast_one))))
    squares._proof_12⊢ ∑ x ∈ S, 1 / ↑x ≤ ∑' (n : ℕ), 1 / ↑n ^ 2
        let S' := S.preimage (· ^ 2) (Function.Injective.injOn
          (Nat.pow_left_injective (byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sthis:1 = 1 / ↑1 := 
  Eq.mpr
    (id
      (Eq.trans (congr (congrArg Eq (Eq.symm Nat.cast_one)) (congrArg (fun x => x / ↑1) (Eq.symm Nat.cast_one)))
        (congr (congrArg Eq Nat.cast_one) (congr (congrArg HDiv.hDiv Nat.cast_one) Nat.cast_one))))
    squares._proof_12⊢ 2 ≠ 0 decideAll goals completed! 🐙)))
        have hS' : S'.map ⟨(· ^ 2), Nat.pow_left_injective (byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sthis:1 = 1 / ↑1 := 
  Eq.mpr
    (id
      (Eq.trans (congr (congrArg Eq (Eq.symm Nat.cast_one)) (congrArg (fun x => x / ↑1) (Eq.symm Nat.cast_one)))
        (congr (congrArg Eq Nat.cast_one) (congr (congrArg HDiv.hDiv Nat.cast_one) Nat.cast_one))))
    squares._proof_12S':Finset ℕ := S.preimage (fun x => x ^ 2) ⋯⊢ 2 ≠ 0 decideAll goals completed! 🐙)⟩ = S := byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ 1 - (∑' (n : ℕ), 1 / ↑n ^ 2 - 1) ≤ 1 - ∑ n ∈ S \ {1}, 1 / ↑n
          apply Finset.coe_injectiveaS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sthis:1 = 1 / ↑1 := 
  Eq.mpr
    (id
      (Eq.trans (congr (congrArg Eq (Eq.symm Nat.cast_one)) (congrArg (fun x => x / ↑1) (Eq.symm Nat.cast_one)))
        (congr (congrArg Eq Nat.cast_one) (congr (congrArg HDiv.hDiv Nat.cast_one) Nat.cast_one))))
    squares._proof_12S':Finset ℕ := S.preimage (fun x => x ^ 2) ⋯⊢ ↑(Finset.map { toFun := fun x => x ^ 2, inj' := ⋯ } S') = ↑S
          have h : (S : Set ℕ) ⊆ Set.range (· ^ 2) :=
            hs.trans (byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sthis:1 = 1 / ↑1 := 
  Eq.mpr
    (id
      (Eq.trans (congr (congrArg Eq (Eq.symm Nat.cast_one)) (congrArg (fun x => x / ↑1) (Eq.symm Nat.cast_one)))
        (congr (congrArg Eq Nat.cast_one) (congr (congrArg HDiv.hDiv Nat.cast_one) Nat.cast_one))))
    squares._proof_12S':Finset ℕ := S.preimage (fun x => x ^ 2) ⋯⊢ {n | IsSquare n} \ {0} ⊆ range fun x => x ^ 2 simp [isSquare_iff_exists_sq, Set.subset_def]All goals completed! 🐙)
          simpa [S', Set.image_preimage_eq_iff] using hAll goals completed! 🐙
        rw [← hS', Finset.sum_map, Function.Embedding.coeFn_mk]hS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sthis:1 = 1 / ↑1 := 
  Eq.mpr
    (id
      (Eq.trans (congr (congrArg Eq (Eq.symm Nat.cast_one)) (congrArg (fun x => x / ↑1) (Eq.symm Nat.cast_one)))
        (congr (congrArg Eq Nat.cast_one) (congr (congrArg HDiv.hDiv Nat.cast_one) Nat.cast_one))))
    squares._proof_12S':Finset ℕ := S.preimage (fun x => x ^ 2) ⋯hS':Finset.map { toFun := fun x => x ^ 2, inj' := ⋯ } S' = S := 
  Finset.coe_injective
    (have h :=
      HasSubset.Subset.trans hs
        (of_eq_true
          (Eq.trans (congrArg (fun x => setOf x \ {0} ⊆ range fun x => x ^ 2) (funext fun n => squares._simp_13 n))
            (Eq.trans
              (Eq.trans
                (forall_congr fun x =>
                  Eq.trans
                    (Eq.trans
                      (implies_congr
                        (Eq.trans (mem_diff._simp_1 x)
                          (congrArg (fun x_1 => (∃ r, x = r ^ 2) ∧ ¬x_1) mem_singleton_iff._simp_1))
                        mem_range._simp_1)
                      and_imp._simp_1)
                    forall_exists_index._simp_1)
                forall_eq_apply_imp_iff._simp_1)
              (Eq.trans
                (forall_congr fun a =>
                  Eq.trans
                    (implies_congr
                      (congrArg Not
                        (Eq.trans Nat.pow_eq_zero._simp_1
                          (Eq.trans
                            (congrArg (And (a = 0))
                              (Eq.trans (congrArg Not (OfNat.ofNat_ne_zero._simp_1 2)) not_false_eq_true))
                            (and_true (a = 0)))))
                      (Eq.trans
                        (congrArg Exists
                          (funext fun y =>
                            pow_left_inj₀._simp_1 (of_eq_true (one_le._simp_2 y)) (of_eq_true (one_le._simp_2 a))
                              (of_eq_true (Eq.trans (congrArg Not (OfNat.ofNat_ne_zero._simp_1 2)) not_false_eq_true))))
                        exists_eq._simp_1))
                    (implies_true ¬a = 0))
                (implies_true ℕ)))));
    Eq.mpr
      (id
        (Eq.trans
          (congrArg (fun x => x = ↑S)
            (Eq.trans
              (Finset.coe_map
                { toFun := fun x => x ^ 2, inj' := Nat.pow_left_injective (of_decide_eq_true (id (Eq.refl true))) }
                (S.preimage (fun x => x ^ 2)
                  (Function.Injective.injOn (Nat.pow_left_injective (of_decide_eq_true (id (Eq.refl true)))))))
              (Eq.trans (image_congr fun a a_1 => Eq.refl (a ^ 2))
                (congrArg (image fun x => x ^ 2)
                  (Finset.coe_preimage S
                    (Function.Injective.injOn (Nat.pow_left_injective (of_decide_eq_true (id (Eq.refl true))))))))))
          squares._simp_14))
      h)⊢ ∑ x ∈ S', 1 / ↑(x ^ 2) ≤ ∑' (n : ℕ), 1 / ↑n ^ 2
        simpa [Nat.cast_pow] using Summable.sum_le_tsum S' (fun _ _ => byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sthis:1 = 1 / ↑1 := 
  Eq.mpr
    (id
      (Eq.trans (congr (congrArg Eq (Eq.symm Nat.cast_one)) (congrArg (fun x => x / ↑1) (Eq.symm Nat.cast_one)))
        (congr (congrArg Eq Nat.cast_one) (congr (congrArg HDiv.hDiv Nat.cast_one) Nat.cast_one))))
    squares._proof_12S':Finset ℕ := S.preimage (fun x => x ^ 2) ⋯hS':Finset.map { toFun := fun x => x ^ 2, inj' := ⋯ } S' = S := 
  Finset.coe_injective
    (have h :=
      HasSubset.Subset.trans hs
        (of_eq_true
          (Eq.trans (congrArg (fun x => setOf x \ {0} ⊆ range fun x => x ^ 2) (funext fun n => squares._simp_13 n))
            (Eq.trans
              (Eq.trans
                (forall_congr fun x =>
                  Eq.trans
                    (Eq.trans
                      (implies_congr
                        (Eq.trans (mem_diff._simp_1 x)
                          (congrArg (fun x_1 => (∃ r, x = r ^ 2) ∧ ¬x_1) mem_singleton_iff._simp_1))
                        mem_range._simp_1)
                      and_imp._simp_1)
                    forall_exists_index._simp_1)
                forall_eq_apply_imp_iff._simp_1)
              (Eq.trans
                (forall_congr fun a =>
                  Eq.trans
                    (implies_congr
                      (congrArg Not
                        (Eq.trans Nat.pow_eq_zero._simp_1
                          (Eq.trans
                            (congrArg (And (a = 0))
                              (Eq.trans (congrArg Not (OfNat.ofNat_ne_zero._simp_1 2)) not_false_eq_true))
                            (and_true (a = 0)))))
                      (Eq.trans
                        (congrArg Exists
                          (funext fun y =>
                            pow_left_inj₀._simp_1 (of_eq_true (one_le._simp_2 y)) (of_eq_true (one_le._simp_2 a))
                              (of_eq_true (Eq.trans (congrArg Not (OfNat.ofNat_ne_zero._simp_1 2)) not_false_eq_true))))
                        exists_eq._simp_1))
                    (implies_true ¬a = 0))
                (implies_true ℕ)))));
    Eq.mpr
      (id
        (Eq.trans
          (congrArg (fun x => x = ↑S)
            (Eq.trans
              (Finset.coe_map
                { toFun := fun x => x ^ 2, inj' := Nat.pow_left_injective (of_decide_eq_true (id (Eq.refl true))) }
                (S.preimage (fun x => x ^ 2)
                  (Function.Injective.injOn (Nat.pow_left_injective (of_decide_eq_true (id (Eq.refl true)))))))
              (Eq.trans (image_congr fun a a_1 => Eq.refl (a ^ 2))
                (congrArg (image fun x => x ^ 2)
                  (Finset.coe_preimage S
                    (Function.Injective.injOn (Nat.pow_left_injective (of_decide_eq_true (id (Eq.refl true))))))))))
          squares._simp_14))
      h)x✝¹:ℕx✝:x✝¹ ∉ S'⊢ 0 ≤ (↑x✝¹ ^ 2)⁻¹ positivityAll goals completed! 🐙) (byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sthis:1 = 1 / ↑1 := 
  Eq.mpr
    (id
      (Eq.trans (congr (congrArg Eq (Eq.symm Nat.cast_one)) (congrArg (fun x => x / ↑1) (Eq.symm Nat.cast_one)))
        (congr (congrArg Eq Nat.cast_one) (congr (congrArg HDiv.hDiv Nat.cast_one) Nat.cast_one))))
    squares._proof_12S':Finset ℕ := S.preimage (fun x => x ^ 2) ⋯hS':Finset.map { toFun := fun x => x ^ 2, inj' := ⋯ } S' = S := 
  Finset.coe_injective
    (have h :=
      HasSubset.Subset.trans hs
        (of_eq_true
          (Eq.trans (congrArg (fun x => setOf x \ {0} ⊆ range fun x => x ^ 2) (funext fun n => squares._simp_13 n))
            (Eq.trans
              (Eq.trans
                (forall_congr fun x =>
                  Eq.trans
                    (Eq.trans
                      (implies_congr
                        (Eq.trans (mem_diff._simp_1 x)
                          (congrArg (fun x_1 => (∃ r, x = r ^ 2) ∧ ¬x_1) mem_singleton_iff._simp_1))
                        mem_range._simp_1)
                      and_imp._simp_1)
                    forall_exists_index._simp_1)
                forall_eq_apply_imp_iff._simp_1)
              (Eq.trans
                (forall_congr fun a =>
                  Eq.trans
                    (implies_congr
                      (congrArg Not
                        (Eq.trans Nat.pow_eq_zero._simp_1
                          (Eq.trans
                            (congrArg (And (a = 0))
                              (Eq.trans (congrArg Not (OfNat.ofNat_ne_zero._simp_1 2)) not_false_eq_true))
                            (and_true (a = 0)))))
                      (Eq.trans
                        (congrArg Exists
                          (funext fun y =>
                            pow_left_inj₀._simp_1 (of_eq_true (one_le._simp_2 y)) (of_eq_true (one_le._simp_2 a))
                              (of_eq_true (Eq.trans (congrArg Not (OfNat.ofNat_ne_zero._simp_1 2)) not_false_eq_true))))
                        exists_eq._simp_1))
                    (implies_true ¬a = 0))
                (implies_true ℕ)))));
    Eq.mpr
      (id
        (Eq.trans
          (congrArg (fun x => x = ↑S)
            (Eq.trans
              (Finset.coe_map
                { toFun := fun x => x ^ 2, inj' := Nat.pow_left_injective (of_decide_eq_true (id (Eq.refl true))) }
                (S.preimage (fun x => x ^ 2)
                  (Function.Injective.injOn (Nat.pow_left_injective (of_decide_eq_true (id (Eq.refl true)))))))
              (Eq.trans (image_congr fun a a_1 => Eq.refl (a ^ 2))
                (congrArg (image fun x => x ^ 2)
                  (Finset.coe_preimage S
                    (Function.Injective.injOn (Nat.pow_left_injective (of_decide_eq_true (id (Eq.refl true))))))))))
          squares._simp_14))
      h)⊢ Summable fun x => (↑x ^ 2)⁻¹ simpAll goals completed! 🐙)
    ·posS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ S⊢ ∀ x ∈ S \ {1}, (fun n => if n = 1 then 1 else -1) x / ↑x = -1 / ↑x intro _ _posS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∈ Sx✝:ℕa✝:x✝ ∈ S \ {1}⊢ (fun n => if n = 1 then 1 else -1) x✝ / ↑x✝ = -1 / ↑x✝; grindAll goals completed! 🐙
  ·negS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∉ S⊢ ¬∑ n ∈ S, (fun n => if n = 1 then 1 else -1) n / ↑n = 0 suffices ∑ n ∈ S, (fun n ↦ if n = 1 then 1 else - 1) n / (n : ℝ) < 0 from byS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∉ Sthis:∑ n ∈ S, (fun n => if n = 1 then 1 else -1) n / ↑n < 0 := ?m.627⊢ ¬∑ n ∈ S, (fun n => if n = 1 then 1 else -1) n / ↑n = 0 linarithAll goals completed! 🐙
    refine Finset.sum_neg (fun p hp => ?_) hnegS:Finset ℕh:S.Nonemptyhs:↑S ⊆ {n | IsSquare n} \ {0}h1:1 ∉ Sp:ℕhp:p ∈ S⊢ (fun n => if n = 1 then 1 else -1) p / ↑p < 0
    have : p ≠ 1 := by⊢ ¬P₁ {n | IsSquare n} grindAll goals completed! 🐙
    simp_all [neg_div, zero_lt_iff, (not_iff_not.2 mem_singleton_iff).1 (hs hp).2]All goals completed! 🐙

For any set A containing exactly one even number, A does not have property P₁. Sattler [Sa82] credits this observation to Erdős, who presumably found this after [ErGr80].

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_318.variants.contain_single_even {A : Set ℕ} (hA : {n | n ∈ A ∧ Even n}.ncard = 1) :
    ¬ P₁ A := byA:Set ℕhA:{n | n ∈ A ∧ Even n}.ncard = 1⊢ ¬P₁ A
  sorryAll goals completed! 🐙

There exists a set A with positive density that does not have property P₁. #TODO: prove this lemma by assuming erdos_318.contain_single_even.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_318.parts.i : ∃ A : Set ℕ, HasPosDensity A ∧ ¬ P₁ A := by⊢ ∃ A, A.HasPosDensity ∧ ¬P₁ A
  sorryAll goals completed! 🐙

Every infinite arithmetic progression has property P₁. This is proved in [Sa82b].

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_318.variants.infinite_AP {A : Set ℕ} (hA : A.IsAPOfLength ⊤) : P₁ A := byA:Set ℕhA:A.IsAPOfLength ⊤⊢ P₁ A
  sorryAll goals completed! 🐙

Does the set of squares excluding 1 have property P₁?

Larsen [La26] proved that this set does have property P₁.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_318.parts.ii : answer(True) ↔  P₁ ({n | IsSquare n} \ {1}) := by⊢ True ↔ P₁ ({n | IsSquare n} \ {1})
  sorryAll goals completed! 🐙


end Erdos318