diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture189.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture189.lean
new file mode 100644
index 000000000..a9e5796fa
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture189.lean
@@ -0,0 +1,81 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 189
+
+**Verbatim statement (WOWII #189, status O):**
+> If G is a simple connected graph with n > 1 such that maximum { dist_even(v) : dist_even(v) is the number of vertices at even distance from v } ≤ 1 + σ(G), then G has a Hamiltonian path.
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj189
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture189
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`. -/
+noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/-- The **second-smallest degree** of `G`'s degree sequence — DeLaVina's
+`σ(G)` per the WOWII definitions popup (defEntry 65): "order the degree
+sequence in nondecreasing order `d_1 ≤ d_2 ≤ … ≤ d_n`, the second smallest
+degree of the sequence is the 2nd entry". For graphs with `n ≤ 1` we
+conventionally return `0`. -/
+noncomputable def secondSmallestDegree (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
+  (degreeSequence G).getD 1 0
+
+/--
+WOWII [Conjecture 189](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj189)
+(status O):
+
+For a simple connected graph `G`, if `max_v distEven(v) ≤ 1 + σ(G)`,
+then `G` has a Hamiltonian path.
+
+Here `distEven(v)` is the number of vertices at even distance from `v`, and
+`σ(G)` is the **second-smallest degree** of `G`'s degree sequence (per
+WOWII defEntry 65).
+-/
+@[category research open, AMS 5]
+theorem conjecture189 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected)
+    (hσ : (Finset.univ.image (distEven G)).max' (by simp) ≤ 1 + secondSmallestDegree G) :
+    ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian := by
+  sorry
+
+-- Sanity checks
+
+/-- The second-smallest degree is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) [DecidableRel G.Adj] :
+    0 ≤ secondSmallestDegree G := Nat.zero_le _
+
+/-- `distEven G v` is positive for any vertex `v`. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) (v : Fin 3) : 0 < distEven G v := by
+  unfold distEven
+  apply Finset.card_pos.mpr
+  exact ⟨v, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ⟨0, by simp [SimpleGraph.dist_self]⟩⟩⟩
+
+end WrittenOnTheWallII.GraphConjecture189
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture199.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture199.lean
new file mode 100644
index 000000000..88beb777c
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture199.lean
@@ -0,0 +1,75 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 199
+
+**Verbatim statement (WOWII #199, status O):**
+> If G is a simple connected graph with n > 1 such that tree(G) - 2 ≤ κ(G), then G has a Hamiltonian path.
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj199
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture199
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `largestInducedTreeSize G` is the number of vertices in a largest induced subtree of `G`. -/
+noncomputable def largestInducedTreeSize (G : SimpleGraph α) : ℕ :=
+  sSup { n | ∃ s : Finset α, s.card = n ∧ (G.induce (s : Set α)).IsTree }
+
+/-- The vertex connectivity `κ(G)`: the minimum number of vertices whose removal
+disconnects the graph (or `n - 1` when the graph is complete).
+Vertex connectivity is not yet in Mathlib; we define it here as the minimum size of
+a vertex separator, where removing `S` leaves the induced subgraph on `Sᶜ` disconnected.
+-- TODO: replace with a Mathlib definition when one becomes available. -/
+noncomputable def vertexConnectivity (G : SimpleGraph α) : ℕ :=
+  if Fintype.card α ≤ 1 then 0
+  else sInf { k | ∃ S : Finset α, S.card = k ∧
+    (¬(G.induce (↑Sᶜ : Set α)).Connected ∨ S.card = Fintype.card α - 1) }
+
+/--
+WOWII [Conjecture 199](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, if `tree(G) - 2 ≤ κ(G)`, then `G` has a Hamiltonian path.
+Here `tree(G)` is the number of vertices in a largest induced tree and
+`κ(G) = vertexConnectivity G` is the vertex connectivity of `G`.
+-/
+@[category research open, AMS 5]
+theorem conjecture199 (G : SimpleGraph α) (h : G.Connected)
+    (hκ : largestInducedTreeSize G - 2 ≤ vertexConnectivity G) :
+    ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian := by
+  sorry
+
+-- Sanity checks
+
+/-- The `largestInducedTreeSize` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ largestInducedTreeSize G := Nat.zero_le _
+
+/-- The vertex connectivity is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ vertexConnectivity G := Nat.zero_le _
+
+end WrittenOnTheWallII.GraphConjecture199
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture24.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture24.lean
new file mode 100644
index 000000000..40fffaf67
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture24.lean
@@ -0,0 +1,78 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 24
+
+**Verbatim statement (WOWII #24, status F):**
+> If G is a simple connected graph, then b(G) ≥ λ(G) + CEIL[minimum of dist_even(v)/3]
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj24
+
+This conjecture is **disproved** on the WOWII page (status F). Following the
+upstream pattern established in #3823 for the closely related Conjecture 23,
+we record the disproof using `answer(False) ↔ ...`.
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture24
+
+open Classical SimpleGraph
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`.
+Distance 0 (the vertex itself) is even, so `distEven G v ≥ 1`. -/
+noncomputable def distEven {α : Type*} [Fintype α]
+    (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/--
+WOWII [Conjecture 24](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj24)
+(status F, disproved):
+
+For every finite simple connected graph `G`,
+`b(G) ≥ λ(G) + ⌈(min_v dist_even(v)) / 3⌉`
+where `b(G)` is the size of a largest induced bipartite subgraph,
+`λ(G) := max_v l(v)` is the maximum over all vertices of the independence
+number of the open neighbourhood of `v`, and `dist_even(v)` is the number of
+vertices at even distance from `v`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture24 : answer(False) ↔
+    ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α],
+      ∀ (G : SimpleGraph α) (_ : G.Connected),
+        let maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+        let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
+        (maxL : ℝ) + ⌈(minDistEven : ℝ) / 3⌉ ≤ b G := by
+  sorry
+
+-- Sanity checks
+
+/-- `distEven G v` is always positive, since `v` itself is at distance 0 (even) from itself. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) (v : Fin 3) : 0 < distEven G v := by
+  unfold distEven
+  apply Finset.card_pos.mpr
+  exact ⟨v, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ⟨0, by simp [SimpleGraph.dist_self]⟩⟩⟩
+
+/-- The invariant `b G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphConjecture24
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean
new file mode 100644
index 000000000..37535638a
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean
@@ -0,0 +1,75 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 25
+
+**Verbatim statement (WOWII #25, status F):**
+> If G is a simple connected graph, then b(G) ≥ 2 CEIL[(1 + minimum of dist_even(v))/3]
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj25
+
+This conjecture is **disproved** on the WOWII page (status F; "same
+counterexample as in #24"). Following the upstream pattern established in
+#3823 for Conjecture 23, we record the disproof using `answer(False) ↔ ...`.
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture25
+
+open Classical SimpleGraph
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`.
+Distance 0 (the vertex itself) is even, so `distEven G v ≥ 1`. -/
+noncomputable def distEven {α : Type*} [Fintype α]
+    (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/--
+WOWII [Conjecture 25](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj25)
+(status F, disproved):
+
+For every finite simple connected graph `G`,
+`b(G) ≥ 2 · ⌈(1 + min_v dist_even(v)) / 3⌉`
+where `b(G)` is the size of a largest induced bipartite subgraph and
+`dist_even(v)` is the number of vertices at even distance from `v`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture25 : answer(False) ↔
+    ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α],
+      ∀ (G : SimpleGraph α) (_ : G.Connected),
+        let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
+        2 * ⌈(1 + (minDistEven : ℝ)) / 3⌉ ≤ b G := by
+  sorry
+
+-- Sanity checks
+
+/-- `distEven G v` is always at least 1, since `v` itself is at distance 0 (even) from itself. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 4)) (v : Fin 4) : 1 ≤ distEven G v := by
+  unfold distEven
+  apply Finset.card_pos.mpr
+  exact ⟨v, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ⟨0, by simp [SimpleGraph.dist_self]⟩⟩⟩
+
+/-- The invariant `b G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphConjecture25
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture63.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture63.lean
new file mode 100644
index 000000000..a25fc553c
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture63.lean
@@ -0,0 +1,70 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 63
+
+**Verbatim statement (WOWII #63, status O):**
+> If G is a simple connected graph, then f(G) ≥ CEIL[(minimum of dist_even(v) + b(G) + 1)/3]
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj63
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture63
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`. -/
+noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/--
+WOWII [Conjecture 63](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`,
+`f(G) ≥ ⌈(min_v distEven(v) + b(G) + 1) / 3⌉`
+where `f(G) = largestInducedForestSize G` is the size of a largest induced forest,
+`b(G)` is the largest induced bipartite subgraph size, and
+`distEven(v)` is the number of vertices at even distance from `v`.
+-/
+@[category research open, AMS 5]
+theorem conjecture63 (G : SimpleGraph α) (h : G.Connected) :
+    let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
+    ⌈((minDistEven : ℝ) + b G + 1) / 3⌉ ≤ (G.largestInducedForestSize : ℝ) := by
+  sorry
+
+-- Sanity checks
+
+/-- The largest induced forest size is a natural number (nonneg). -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ G.largestInducedForestSize := Nat.zero_le _
+
+/-- `distEven` of any vertex is positive. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) (v : Fin 3) : 0 < distEven G v := by
+  unfold distEven
+  apply Finset.card_pos.mpr
+  exact ⟨v, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ⟨0, by simp [SimpleGraph.dist_self]⟩⟩⟩
+
+end WrittenOnTheWallII.GraphConjecture63
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture72.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture72.lean
new file mode 100644
index 000000000..86c27f474
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture72.lean
@@ -0,0 +1,75 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 72
+
+**Verbatim statement (WOWII #72, status O):**
+> If G is a simple connected graph, then tree(G) ≥ CEIL[average of ecc(v) + maximum of λ(v) /3]
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj72
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture72
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `largestInducedTreeSize G` is the number of vertices in a largest induced subtree of `G`.
+A tree is a connected acyclic graph; an induced tree is an induced subgraph that is a tree. -/
+noncomputable def largestInducedTreeSize (G : SimpleGraph α) : ℕ :=
+  sSup { n | ∃ s : Finset α, s.card = n ∧ (G.induce (s : Set α)).IsTree }
+
+/-- The average eccentricity of `G`: the mean of `eccentricity G v` over all vertices. -/
+noncomputable def averageEccentricity (G : SimpleGraph α) : ℝ :=
+  (∑ v : α, (G.eccentricity v).toNat) / (Fintype.card α : ℝ)
+
+/--
+WOWII [Conjecture 72](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`,
+`tree(G) ≥ ⌈(ecc_avg(G) + max_v l(v)) / 3⌉`
+where `tree(G)` is the number of vertices in a largest induced tree,
+`ecc_avg(G)` is the average eccentricity of `G`, and
+`max_v l(v) = max_v indepNeighborsCard G v` is the maximum over all vertices of
+the independence number of the neighbourhood.
+-/
+@[category research open, AMS 5]
+theorem conjecture72 (G : SimpleGraph α) (h : G.Connected) :
+    let maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+    ⌈(averageEccentricity G + (maxL : ℝ)) / 3⌉ ≤ (largestInducedTreeSize G : ℝ) := by
+  sorry
+
+-- Sanity checks
+
+/-- The `largestInducedTreeSize` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ largestInducedTreeSize G := Nat.zero_le _
+
+/-- The average eccentricity is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ averageEccentricity G := by
+  unfold averageEccentricity
+  positivity
+
+end WrittenOnTheWallII.GraphConjecture72
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture84.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture84.lean
new file mode 100644
index 000000000..d0fc44532
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture84.lean
@@ -0,0 +1,74 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 84
+
+**Verbatim statement (WOWII #84, status O):**
+> If G is a simple connected graph, then tree(G) ≥ 2 rad(G) / δ(G)
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj84
+
+Here `δ(G)` is the **minimum degree** of `G` (lowercase delta in the WOWII
+HTML, rendered as `<font face="Symbol">d</font>`), not the average distance.
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture84
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `largestInducedTreeSize G` is the number of vertices in a largest induced subtree of `G`. -/
+noncomputable def largestInducedTreeSize (G : SimpleGraph α) : ℕ :=
+  sSup { n | ∃ s : Finset α, s.card = n ∧ (G.induce (s : Set α)).IsTree }
+
+/--
+WOWII [Conjecture 84](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj84)
+(status O):
+
+For a simple connected graph `G` with positive minimum degree,
+`tree(G) ≥ 2 · rad(G) / δ(G)`,
+where `tree(G)` is the number of vertices in a largest induced subtree,
+`rad(G)` is the radius, and `δ(G) = G.minDegree` is the minimum degree.
+
+The hypothesis `0 < G.minDegree` follows from connectedness on a nontrivial
+vertex set, but is stated explicitly so the theorem reads as a real-valued
+inequality without `x / 0` corner cases.
+-/
+@[category research open, AMS 5]
+theorem conjecture84 (G : SimpleGraph α) [DecidableRel G.Adj]
+    (h : G.Connected) (hδ : 0 < G.minDegree) :
+    2 * (G.radius.toNat : ℝ) / (G.minDegree : ℝ) ≤ (largestInducedTreeSize G : ℝ) := by
+  sorry
+
+-- Sanity checks
+
+/-- The `largestInducedTreeSize` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ largestInducedTreeSize G := Nat.zero_le _
+
+/-- The largest induced tree size is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ (largestInducedTreeSize G : ℝ) :=
+  Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphConjecture84
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture85.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture85.lean
new file mode 100644
index 000000000..cb15220bb
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture85.lean
@@ -0,0 +1,70 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 85
+
+**Verbatim statement (WOWII #85, status O):**
+> If G is a simple connected graph, then tree(G) ≥ CEIL[sqrt(1 + 2*minimum of dist_even(v))]
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj85
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture85
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`. -/
+noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/-- `largestInducedTreeSize G` is the number of vertices in a largest induced subtree of `G`. -/
+noncomputable def largestInducedTreeSize (G : SimpleGraph α) : ℕ :=
+  sSup { n | ∃ s : Finset α, s.card = n ∧ (G.induce (s : Set α)).IsTree }
+
+/--
+WOWII [Conjecture 85](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`,
+`tree(G) ≥ ⌈√(1 + 2 · min_v distEven(v))⌉`
+where `tree(G)` is the number of vertices in a largest induced tree and
+`distEven(v)` is the number of vertices at even distance from `v`.
+-/
+@[category research open, AMS 5]
+theorem conjecture85 (G : SimpleGraph α) (h : G.Connected) :
+    let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
+    ⌈Real.sqrt (1 + 2 * (minDistEven : ℝ))⌉ ≤ (largestInducedTreeSize G : ℝ) := by
+  sorry
+
+-- Sanity checks
+
+/-- The `largestInducedTreeSize` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ largestInducedTreeSize G := Nat.zero_le _
+
+/-- `Real.sqrt` is nonneg. -/
+@[category test, AMS 5]
+example (x : ℝ) : 0 ≤ Real.sqrt x := Real.sqrt_nonneg x
+
+end WrittenOnTheWallII.GraphConjecture85
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture91.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture91.lean
new file mode 100644
index 000000000..aa83e1bc2
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture91.lean
@@ -0,0 +1,66 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 91
+
+**Verbatim statement (WOWII #91, status O):**
+> If G is a simple connected graph, then b(G) ≤ 1 + f(G) * (CEIL[average of λ(v) ])/2
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj91
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture91
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 91](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`,
+`b(G) ≤ 1 + f(G) · ⌈avg_v l(v)⌉ / 2`
+where `b(G)` is the largest induced bipartite subgraph size,
+`f(G) = largestInducedForestSize G` is the largest induced forest size, and
+`avg_v l(v) = l G` is the average independence number of the neighbourhoods.
+-/
+@[category research open, AMS 5]
+theorem conjecture91 (G : SimpleGraph α) (h : G.Connected) :
+    b G ≤ 1 + (G.largestInducedForestSize : ℝ) * ⌈l G⌉ / 2 := by
+  sorry
+
+-- Sanity checks
+
+/-- The invariant `b G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+/-- The average indep-neighbors `l G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ l G := by
+  unfold l averageIndepNeighbors
+  apply div_nonneg
+  · apply Finset.sum_nonneg; intro v _; exact Nat.cast_nonneg _
+  · exact Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphConjecture91
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture96.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture96.lean
new file mode 100644
index 000000000..63cb0d7c6
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture96.lean
@@ -0,0 +1,68 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 96
+
+**Verbatim statement (WOWII #96, status O):**
+> If G is a simple connected graph, then α(G) ≤ 1 + minimum dist_even(v)*(maximum of λ(v) -1)
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj96
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture96
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`. -/
+noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/--
+WOWII [Conjecture 96](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`,
+`α(G) ≤ 1 + min_v distEven(v) · (max_v l(v) - 1)`
+where `α(G) = G.indepNum` is the independence number,
+`distEven(v)` is the number of vertices at even distance from `v`, and
+`max_v l(v)` is the maximum independence number of a vertex neighbourhood.
+-/
+@[category research open, AMS 5]
+theorem conjecture96 (G : SimpleGraph α) (h : G.Connected) :
+    let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
+    let maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+    (G.indepNum : ℝ) ≤ 1 + (minDistEven : ℝ) * ((maxL : ℝ) - 1) := by
+  sorry
+
+-- Sanity checks
+
+/-- The independence number is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ G.indepNum := Nat.zero_le _
+
+/-- The independence number is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ G.indepNum := Nat.zero_le _
+
+end WrittenOnTheWallII.GraphConjecture96