All open problems
Source labels openChecked July 26, 2026

Written on the Wall IICombinatorics

Written on the Wall II - Conjecture 160

Mathematical statement

WOWII Conjecture 160

For a simple connected graph GG, Ls(G)maxvl(v)+maxvT(v)cC4(G)L_s(G) \ge \max_v l(v) + \max_v T(v) \cdot c_{C_4}(G) where:

  • Ls(G)=SimpleGraph.LsGL_s(G) = \mathrm{SimpleGraph.Ls}\, G is the maximum number of leaves over all spanning trees of GG,
  • maxvl(v)\max_v l(v) is the maximum local independence number over vertices,
  • maxvT(v)\max_v T(v) is the maximum number of triangles incident to any vertex,
  • cC4(G)c_{C_4}(G) is the number of induced 4-cycles in GG.

Statement source: Written on the Wall II statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

conjecture160

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem conjecture160 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :    let maxL := (Finset.univ.image (indepNeighborsCard G)).max' (by simp)    let maxT := maxTrianglesAtVertex G    let cC4 := countInducedC4 G    (maxL : ) + (maxT : ) * (cC4 : )  Ls G := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References