FormalConjectures/ErdosProblems/926.lean
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 926
References:
- erdosproblems.com/926
- [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35.
- [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.
- [Er74c] Erdős, Paul, Extremal problems on graphs and hypergraphs. (1974), 75-84.
- [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350.
- [Fu91] Füredi, Zoltán, On a Turán type problem of Erdős. Combinatorica (1991), 75--79.
- [AKS03] Alon, Noga and Krivelevich, Michael and Sudakov, Benny, Turán numbers of bipartite graphs and related Ramsey-type questions. Combin. Probab. Comput. (2003), 477-494.
Imports (1)
- def
Erdos926.HThe graph $H_k$ on the vertices $x, y_1, \ldots, y_k, z_{ij}$ ($i < j$): $x$ is adjacent to every $y_i$, and each pair $y_i, y_j$ is adjacent to the vertex $z_{ij}$ line 45 sourceSource documentation
The graph $H_k$ on the vertices $x, y_1, \ldots, y_k, z_{ij}$ ($i < j$): $x$ is adjacent to every $y_i$, and each pair $y_i, y_j$ is adjacent to the vertex $z_{ij}$.
standard axioms: propext what this means
Statement uses:
Nat,SimpleGraph,Sum,Unit,Fin,Subtype,Prod,LT.lt,Prod.fst,Prod.sndProof uses:
SimpleGraph.mk,Erdos926.H.match_1,True,Or,Eq,False5 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def H (k : ℕ) : SimpleGraph (Unit ⊕ (Fin k ⊕ {p : Fin k × Fin k // p.1 < p.2})) where … - theorem
Erdos926.erdos_926sorry line 80 sourcedepends on sorry what this means
Statement uses:
Iff,True,Nat,LE.le,OfNat.ofNat,Asymptotics.IsBigO,Real,Filter.atTop,SimpleGraph.extremalNumber,Sum,Unit,Fin,Subtype,Prod,LT.lt,Prod.fst,Prod.snd, Erdos926.H,HPow.hPow,HDiv.hDivProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous30 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
- theorem
Erdos926.erdos_926.variants.aksAlon, Krivelevich, and Sudakov [AKS03] proved $\mathrm{ex}(n;H_k) \ll kn^{3/2}$ with an absolute implied constant sorry line 87 sourceSource documentation
Alon, Krivelevich, and Sudakov [AKS03] proved $\mathrm{ex}(n;H_k) \ll kn^{3/2}$ with an absolute implied constant.
depends on sorry what this means
Statement uses:
Exists,Real,Nat,LE.le,OfNat.ofNat,SimpleGraph.extremalNumber,Sum,Unit,Fin,Subtype,Prod,LT.lt,Prod.fst,Prod.snd, Erdos926.H,HMul.hMul,HPow.hPow,HDiv.hDivProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous32 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem erdos_926.variants.aks : ∃ C : ℝ, ∀ k : ℕ, 4 ≤ k → ∀ n : ℕ, (extremalNumber n (H k) : ℝ) ≤ C * k * (n : ℝ) ^ (3 / 2 : ℝ) := by …Mentions: Erdos926.H