FormalConjectures/ErdosProblems/123.lean

GitHub source file

7 declarations, 4 contain sorry, 0 declared as axioms

1. def Erdos123.IsDComplete A sequence is said to be $d$-complete if every large integer is the sum of distinct integers from the sequence, none of which divide any other line 50 source

   Source documentation

   A sequence is said to be $d$-complete if every large integer is the sum of distinct integers from the sequence, none of which divide any other. This particular case of $d$-completeness was conjectured by Erdős and Lewin [ErLe96], who (among other related results) prove this when $a=3$, $b=5$, and $c=7$.

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

   Statement uses: Set, Nat

   Proof uses: Filter.Eventually, Exists, Finset, And, LE.le, IsAntichain, Dvd.dvd, Eq, Finset.sum, id, Filter.atTop

   6 instances, coercions and auxiliary constants left out.

   def IsDComplete (A : Set ℕ) : Prop :=
   …

2. def Erdos123.IsSnug Characterizes a "snug" finite set of natural numbers: all elements are within a multiplicative factor $(1 + ε)$ of the minimum line 64 source

   Source documentation

   Characterizes a "snug" finite set of natural numbers: all elements are within a multiplicative factor $(1 + ε)$ of the minimum. Specifically, for a finite set $A$ and $ε > 0$, all $a ∈ A$ satisfy $a < (1 + ε) · min(A)$.

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

   Statement uses: Real, Finset, Nat

   Proof uses: Exists, Finset.Nonempty, Membership.mem, LT.lt, HMul.hMul, HAdd.hAdd, OfNat.ofNat, Finset.min'

   12 instances, coercions and auxiliary constants left out.

   def IsSnug (ε : ℝ) (A : Finset ℕ) : Prop :=
   …

3. def Erdos123.PairwiseCoprime Predicate for pairwise coprimality of three integers line 71 source

   Source documentation

   Predicate for pairwise coprimality of three integers. Requires all three input values to be pairwise coprime to each other.

   standard axioms: propext what this means

   Statement uses: Nat

   Proof uses: Pairwise, Fin, Nat.succ, OfNat.ofNat, Function.onFun, Nat.Coprime, Matrix.vecCons, Matrix.vecEmpty

   1 instances, coercions and auxiliary constants left out.

   def PairwiseCoprime (a b c : ℕ) : Prop := Pairwise (Nat.Coprime.onFun ![a, b, c])
   …

   Mentions: c

4. theorem Erdos123.erdos_123 sorry line 91 source

   depends on sorry what this means

   Statement uses: Iff, True, Nat, GT.gt, OfNat.ofNat, Erdos123.PairwiseCoprime, Erdos123.IsDComplete, HMul.hMul, Set, Submonoid, Submonoid.powers

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

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

5. theorem Erdos123.erdos_123.variants.erdos_lewin_3_5_7 Erdős and Lewin [ErLe96] proved this conjecture when $a = 3$, $b = 5$, and $c = 7$ sorry line 98 source

   Source documentation

   Erdős and Lewin [ErLe96] proved this conjecture when $a = 3$, $b = 5$, and $c = 7$.

   depends on sorry what this means

   Statement uses: Erdos123.IsDComplete, HMul.hMul, Set, Nat, Submonoid, Submonoid.powers, OfNat.ofNat

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

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_123.variants.erdos_lewin_3_5_7 :
       IsDComplete (↑(powers 3) * ↑(powers 5) * ↑(powers 7)) := by sorry
   …

   Mentions: Erdos123.IsDComplete

6. theorem Erdos123.erdos_123.variants.powers_2_3 A simpler case: the set of numbers of the form $2^k 3^l$ ($k, l ≥ 0$) is d-complete sorry line 111 source

   Source documentation

   A simpler case: the set of numbers of the form $2^k 3^l$ ($k, l ≥ 0$) is d-complete.

   This was initially conjectured by Erdős in 1992, who called it a "nice and difficult" problem, but it was quickly proven by Jansen and others using a simple inductive argument:

   • If $n = 2m$ is even, apply the inductive hypothesis to $m$ and double all summands.
   • If $n$ is odd, let $3^k$ be the largest power of $3$ with $3^k ≤ n$, and apply the inductive hypothesis to $n - 3^k$ (which is even).

   depends on sorry what this means

   Statement uses: Erdos123.IsDComplete, HMul.hMul, Set, Nat, Submonoid, Submonoid.powers, OfNat.ofNat

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

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_123.variants.powers_2_3 : IsDComplete (↑(powers 2) * ↑(powers 3)) := by sorry
   …

   Mentions: Erdos123.IsDComplete

7. theorem Erdos123.erdos_123.variants.powers_2_3_5_snug In [Er92b] Erdős makes the stronger conjecture (for sorry line 119 source

   Source documentation

   In [Er92b] Erdős makes the stronger conjecture (for $a=2$, $b=3$, and $c=5$) that, for any $\epsilon>0$, all large integers $n$ can be written as the sum of distinct integers $b_1<\cdots <b_t$ of the form $2^k3^l5^m$ where $b_t<(1+\epsilon)b_1$.

   depends on sorry what this means

   Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Exists, Finset, And, LE.le, Set, HMul.hMul, Submonoid, Submonoid.powers, Erdos123.IsSnug, Eq, Finset.sum, Filter.atTop

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

   30 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_123.variants.powers_2_3_5_snug :
       answer(sorry) ↔ ∀ ε > 0, ∀ᶠ n in atTop,
         ∃ A : Finset ℕ, (A : Set ℕ) ⊆ ↑(powers 2) * ↑(powers 3) * ↑(powers 5) ∧ IsSnug ε A ∧
           ∑ x ∈ A, x = n := by sorry
   …

   Mentions: Erdos123.IsSnug