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

Reference: erdosproblems.com/562

Imports (1)
  1. theorem Erdos562.erdos_562 Documented declaration: erdos_562 sorry line 43 source

    Source documentation

    Let $R_r(n)$ denote the $r$-uniform hypergraph Ramsey number: the minimal $m$ such that if we $2$-colour all edges of the complete $r$-uniform hypergraph on $m$ vertices then there must be some monochromatic copy of the complete $r$-uniform hypergraph on $n$ vertices.

    Prove that, for $r \ge 3$, $$ \log_{r-1} R_r(n) \asymp_r n, $$ where $\log_{r-1}$ denotes the $(r-1)$-fold iterated logarithm.

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Asymptotics.IsTheta, Real, Filter.atTop, Nat.iterate, Real.log, HSub.hSub, Combinatorics.hypergraphRamsey

    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_562 : answer(sorry) ↔
    ∀ r ≥ 3, (fun n ↦ log^[r - 1] (hypergraphRamsey r n)) =Θ[atTop] (fun n ↦ (n : ℝ)) := by
…