FormalConjectures/ErdosProblems/564.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

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 564

Reference: erdosproblems.com/564

Imports (1)
  1. theorem Erdos564.erdos_564 Documented declaration: erdos_564 sorry line 41 source

    Source documentation

    Let $R_3(n)$ be the minimal $m$ such that if the edges of the $3$-uniform hypergraph on $m$ vertices are $2$-coloured then there is a monochromatic copy of the complete $3$-uniform hypergraph on $n$ vertices.

    Is there some constant $c>0$ such that $$ R_3(n) \geq 2^{2^{cn}}? $$

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, HPow.hPow, HMul.hMul, Combinatorics.hypergraphRamsey, 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_564 : answer(sorry) ↔
    ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (2 : ℝ) ^ (2 : ℝ) ^ (c * n) ≤ hypergraphRamsey 3 n := by
…

    Mentions: c