FormalConjectures/ErdosProblems/848.lean

GitHub source file

5 declarations, 2 contain sorry, 0 declared as axioms

1. def Erdos848.NonSquarefreeProductProp A set $A$ has the non-squarefree product property if $ab + 1$ is not squarefree for all $a, b ∈ A$ line 42 source

   Source documentation

   A set $A$ has the non-squarefree product property if $ab + 1$ is not squarefree for all $a, b ∈ A$.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, Nat

   Proof uses: Membership.mem, Not, Squarefree, HAdd.hAdd, HMul.hMul, OfNat.ofNat

   8 instances, coercions and auxiliary constants left out.

   def NonSquarefreeProductProp (A : Finset ℕ) : Prop :=
   …

2. def Erdos848.A₇ The candidate extremal set: $\{n ∈ \{0, \dots, N-1\} : n ≡ 7 (mod 25)\}$ line 46 source

   Source documentation

   The candidate extremal set: $\{n ∈ \{0, \dots, N-1\} : n ≡ 7 (mod 25)\}$.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Finset

   Proof uses: Finset.filter, Eq, HMod.hMod, OfNat.ofNat, Finset.range

   4 instances, coercions and auxiliary constants left out.

   def A₇ (N : ℕ) : Finset ℕ :=
   …

3. def Erdos848.Erdos848For The Erdős Problem 848 statement for a fixed $N$: any set $A ⊆ \{0, \dots, N-1\}$ with the non-squarefree product property has cardinality at most $|A₇(N)|$ line 51 source

   Source documentation

   The Erdős Problem 848 statement for a fixed $N$: any set $A ⊆ \{0, \dots, N-1\}$ with the non-squarefree product property has cardinality at most $|A₇(N)|$.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat

   Proof uses: Finset, LE.le, Finset.range, Erdos848.NonSquarefreeProductProp, Finset.card, Erdos848.A₇

   4 instances, coercions and auxiliary constants left out.

   def Erdos848For (N : ℕ) : Prop :=
   …

4. theorem Erdos848.erdos_848 Is the maximum size of a set $A ⊆ \{1, \dots, N\}$ such that $ab + 1$ is never squarefree (for all $a, b ∈ A$) achieved by taking those $n ≡ 7 \pmod{25}$? sorry line 66 source

   Source documentation

   Is the maximum size of a set $A ⊆ \{1, \dots, N\}$ such that $ab + 1$ is never squarefree (for all $a, b ∈ A$) achieved by taking those $n ≡ 7 \pmod{25}$?

   This asks whether Erdos848 N holds for all $N$ (formulated using A ⊆ Finset.range N).

   This was solved for all sufficiently large $N$ by Sawhney in this note. In fact, Sawhney proves something slightly stronger, that there exists some constant $c>0$ such that if $\lvert A\rvert \geq (\frac{1}{25}-c)N$ and $N$ is large then $A$ is contained in either $\{ n\equiv 7\pmod{25}\}$ or $\{n\equiv 18\pmod{25}\}$.

   depends on sorry what this means

   Statement uses: Iff, True, Nat, Erdos848.Erdos848For

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   1 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_848 : answer(True) ↔ ∀ N, Erdos848For N := by
   …

   Mentions: Erdos848.Erdos848For

5. theorem Erdos848.erdos_848.variants.asymptotic There exists $N₀$ such that for all $N ≥ N₀$, if $A ⊆ \{1, \dots, N\}$ satisfies that $ab + 1$ is never squarefree for all $a, b ∈ A$, then $|A| ≤ |\{n ≤ N : n ≡ 7 \pmod{25}\}|$ sorry line 79 source

   Source documentation

   There exists $N₀$ such that for all $N ≥ N₀$, if $A ⊆ \{1, \dots, N\}$ satisfies that $ab + 1$ is never squarefree for all $a, b ∈ A$, then $|A| ≤ |\{n ≤ N : n ≡ 7 \pmod{25}\}|$.

   More precisely, Sawhney proves: there exist absolute constants $η > 0$ and $N₀$ such that for all $N ≥ N₀$, if $|A| ≥ (1/25 - η)N$ then $A ⊆ \{n : n ≡ 7 \pmod{25}\}$ or $A ⊆ \{n : n ≡ 18 \pmod{25}\}$.

   A complete formal Lean 4 proof is available at: https://github.com/The-Obstacle-Is-The-Way/erdos-banger

   depends on sorry what this means

   Statement uses: Filter.Eventually, Nat, Erdos848.Erdos848For, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

   3 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_848.variants.asymptotic : ∀ᶠ N in Filter.atTop, Erdos848For N := by
   …

   Mentions: Erdos848.Erdos848For