All open problems
Source labels openChecked July 26, 2026

Written on the Wall IICombinatorics

Written on the Wall II - Conjecture 65

Mathematical statement

WOWII Conjecture 65:

For a simple connected graph GG, the size f(G)f(G) of a largest induced forest satisfies f(G)dist_min(A)+dist_min(M)/3f(G) \ge \operatorname{dist\_min}(A) + \lceil \operatorname{dist\_min}(M) / 3 \rceil, where AA is the set of minimum-degree vertices, MM is the set of maximum-degree vertices, and dist_min(S)=minvSdist(v,S)\operatorname{dist\_min}(S) = \min_{v \notin S} \operatorname{dist}(v, S) (see distMin).

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

conjecture65

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem conjecture65 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :    let A : Set α := {v | G.degree v = G.minDegree}    let M : Set α := {v | G.degree v = G.maxDegree}    (distMin G A : ) + ⌈(distMin G M : ) / 3 (G.largestInducedForestSize : ) := 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