FormalConjectures/ErdosProblems/895.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, 3 contain sorry, 0 declared as axioms

Erdős Problem 895

References:

Imports (1)
  1. theorem Erdos895.erdos_895 sorry line 44 source

    depends on sorry what this means

    Statement uses: Iff, True, Filter.Eventually, Nat, SimpleGraph, Set.Icc, OfNat.ofNat, SimpleGraph.CliqueFree, Exists, And, Ne, Eq, HAdd.hAdd, Membership.mem, Set, SimpleGraph.IsIndepSet, Insert.insert, Singleton.singleton, Filter.atTop

    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.

  2. theorem Erdos895.erdos_895.variants.eighteen sorry line 55 source

    depends on sorry what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, SimpleGraph, Set.Icc, SimpleGraph.CliqueFree, Exists, And, Ne, Eq, HAdd.hAdd, Membership.mem, Set, SimpleGraph.IsIndepSet, Insert.insert, Singleton.singleton

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

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem Erdos895.erdos_895.variants.hindman Hajnal thought that there is in fact an independent set which is a Hindman set - that is, an independent set of the shape sorry line 70 source

    Source documentation

    Hajnal thought that there is in fact an independent set which is a Hindman set - that is, an independent set of the shape $$\left\{ \sum_{i\in S}a_i : S\subseteq \{1,\ldots,k\}\right\}$$ for some $a_1,\ldots,a_k$ (provided $n$ is sufficiently large depending on $k$).

    The general question of an independent Hindman set remains open. Here the $a_i$ are taken to be distinct positive integers and $S$ ranges over the nonempty subsets of $\{1,\ldots,k\}$.

    depends on sorry what this means

    Statement uses: Iff, True, Nat, Filter.Eventually, SimpleGraph, Set.Icc, OfNat.ofNat, SimpleGraph.CliqueFree, Exists, Fin, And, StrictMono, Set, SimpleGraph.IsIndepSet, Eq, Set.image, Subtype, Membership.mem, Set.ofPred, Finset and 3 more

    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_895.variants.hindman : answer(sorry) ↔
    ∀ k : ℕ, ∀ᶠ n in atTop, ∀ G : SimpleGraph (Set.Icc 1 n), G.CliqueFree 3 →
      ∃ a : Fin k → ℕ, StrictMono a ∧ ∃ I : Set (Set.Icc 1 n), G.IsIndepSet I ∧
        Subtype.val '' I = {m | ∃ S : Finset (Fin k), S.Nonempty ∧ m = ∑ i ∈ S, a i} := by
…