FormalConjectures/ErdosProblems/13.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

3 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 13

Reference: erdosproblems.com/13

Imports (1)
  1. def Erdos13.IsForbiddenTripleFree A finite set of naturals A is said to be forbidden-triple-free if for all a, b, c ∈ A, if a < min(b, c) then a does not divide b + c line 36 source

    Source documentation

    A finite set of naturals A is said to be forbidden-triple-free if for all a, b, c ∈ A, if a < min(b, c) then a does not divide b + c.

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

    Statement uses: Finset, Nat

    Proof uses: Membership.mem, LT.lt, Min.min, Not, Dvd.dvd, HAdd.hAdd

    7 instances, coercions and auxiliary constants left out.

    def IsForbiddenTripleFree (A : Finset ℕ) : Prop :=
…
  2. theorem Erdos13.erdos_13 sorry line 48 source

    depends on sorry what this means

    Statement uses: Exists, Real, Nat, Finset, LE.le, Finset.Icc, OfNat.ofNat, Erdos13.IsForbiddenTripleFree, Finset.card, HAdd.hAdd, HDiv.hDiv

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

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem Erdos13.erdos_13.variants.general A general version asks, for a fixed sorry line 59 source

    Source documentation

    A general version asks, for a fixed $r \in \mathbb{N}$, if a set $A \subseteq \{1, ..., N\}$ has no $a \in A$ and $b_1, ..., b_r \in A$ such that $a | (b_1 + ... + b_r)$ and $a < \min(b_1, ..., b_r)$, then is it true that $|A| \le N/(r+1) + O(1)$?

    depends on sorry what this means

    Statement uses: Iff, True, Nat, Exists, Real, Finset, LE.le, Finset.Icc, OfNat.ofNat, Membership.mem, Fin, LT.lt, Not, Dvd.dvd, Finset.sum, Finset.univ, Finset.card, HAdd.hAdd, HDiv.hDiv

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

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_13.variants.general : answer(sorry) ↔ ∀ r : ℕ, ∃ C : ℝ, ∀ N : ℕ,
    ∀ A ⊆ Icc 1 N,
    (∀ a ∈ A, ∀ (b : Fin r → ℕ), (∀ i, b i ∈ A) → (∀ i, a < b i) →
      ¬ (a ∣ ∑ i, b i)) →
    (A.card : ℝ) ≤ (N : ℝ) / (r + 1) + C := by
…