Source labels openChecked July 26, 2026

Written on the Wall II - Conjecture 217

Mathematical statement

If $G$ is a finite simple connected graph on $n > 1$ vertices and $L_s(G) \le 4 \cdot \chi_{\mathrm{residue}=2}(G) + 2$ , then $G$ has a Hamiltonian path. Here $L_s(G)$ is the maximum number of leaves over all spanning trees and $\chi_{\mathrm{residue}=2}(G)$ is the indicator of $\mathrm{residue}(G) = 2$ .

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

conjecture217

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem conjecture217 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected)    (hL : Ls G ≤ 4 * (residueEqTwoIndicator G : ℝ) + 2) :    ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian := 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

Pinned Formal Conjectures sourceformalization Conjecture 217background E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pcbackground