Skip to content

Written on the Wall II -… to Written on the Wall II -…

TheoremWritten on the Wall II - Conjecture 34#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture34.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture34.conjecture34

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-graph-proofs/blob/b60c2e548910b32eb3b602f6a8e67af806e4b9f6/LeanGraphProofs/WOWII34.lean#L350.

WOWII Conjecture 34

For a simple connected graph \(G\), \(\operatorname{path}(G) \ge \lceil \operatorname{dist}\_{\operatorname{avg}}(C, V) + \operatorname{dist}\_{\operatorname{avg}}(M, V) \rceil\), where \(\operatorname{path}(G)\) is the number of vertices of a largest induced path of \(G\), \(C\) is the set of center vertices (those with minimum eccentricity), \(M\) is the set of maximum-degree vertices, and \(\operatorname{dist}\_{\operatorname{avg}}(S, V)\) is the average of all nonzero distances \(\operatorname{dist}\_G(s, v)\) with \(s \in S\) and \(v \in V\).

The conjecture is false. The counterexample below was documented by Salvatore Mercuri. Let \(G\) be the tree on \(39\) vertices formed by a vertex with three pendant leaves, joined by a path of five edges to the root of a perfect binary tree of depth four. Then \(\operatorname{path}(G) = 11\), while \(C\) and \(M\) are singletons whose distance sums are \(154\) and \(266\), so the bound is \(\lceil (154 + 266) / 38 \rceil = 12\).

Lean formalization by Wentao Li, with AI assistance.

theorem conjecture34 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected),
      let C : Set α := center G
      let M : Set α := {v | G.degree v = G.maxDegree}
      let distAvg (S : Set α) : ℝ :=
        open scoped Classical in
        let pairs := (S.toFinset ×ˢ Finset.univ).filter (fun p => G.dist p.1 p.2 ≠ 0)
        (∑ p ∈ pairs, (G.dist p.1 p.2 : ℝ)) / pairs.card
      Int.ceil (distAvg C + distAvg M) ≤ (path G : ℤ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture34.lean, line 58.

Sources
LeanWrittenOnTheWallII.GraphConjecture34.conjecture34

TheoremWritten on the Wall II - Conjecture 36#

The conjecture is false. The counterexample below has a subdivided triangle on vertices 0, 1, 9; vertices 7, 8 adjacent to all three triangle vertices; and leaves 3, 2 attached to 7, 8, respectively. It has radius three, one diametrical pair, and largest induced-path order five.

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture36.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.

WrittenOnTheWallII.GraphConjecture36.conjecture36

Proved here.

WOWII Conjecture 36:

For every finite simple connected graph \(G\), \(\operatorname{path}(G) \ge 2 \cdot \operatorname{rad}(G) / \operatorname{dp}(G)\), where \(\operatorname{path}(G)\) is the number of vertices in a largest induced path, \(\operatorname{rad}(G)\) is the radius of \(G\), and \(\operatorname{dp}(G)\) is the number of diametrical pairs of \(G\) — that is, the number of pairs of vertices at distance \(\operatorname{diam}(G)\).

Disproved by Waller in Oct 2003 (counterexample: path number 5, radius 3, dp 1).

theorem conjecture36 :
    ¬ ∀ {α : Type} [Fintype α] [DecidableEq α] [Nontrivial α],
      ∀ (G : SimpleGraph α) [DecidableRel G.Adj] (_ : G.Connected) (_ : 0 < dp G),
        (2 * G.radius.toNat : ℝ) / (dp G : ℝ) ≤ (path G : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture36.lean, line 119.

Sources
LeanWrittenOnTheWallII.GraphConjecture36.conjecture36

TheoremWritten on the Wall II - Conjecture 40#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture40.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

WrittenOnTheWallII.GraphConjecture40.conjecture40

Open: stated without proof.

WOWII Conjecture 40

For a nontrivial connected graph G the size f(G) of a largest induced forest satisfies f(G) ≥ ceil((p(G) + b(G) + 1)/2) where p(G) is the path cover number and b(G) is the largest induced bipartite subgraph size.

theorem conjecture40 (h_conn : G.Connected) (h_nontrivial : 1 < Fintype.card α) :
    ⌈(((pathCoverNumber G : ℝ) + b G + 1) / 2)⌉ ≤  G.largestInducedForestSize

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture40.lean, line 44.

Sources
LeanWrittenOnTheWallII.GraphConjecture40.conjecture40

TheoremWritten on the Wall II - Conjecture 58#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Counterexample

The conjecture is false. A counterexample is given by taking \(K_{3,3}\) (with bipartition \(\{0,1,2\}\), \(\{3,4,5\}\)) and \(K_{73}\) (on vertices \(\{6,\ldots,78\}\)), then adding edges between vertex \(0\) and every vertex of \(K_{73}\).

This graph \(G\) has \(n = 79\) vertices and satisfies: - \(b(G) \ge 7\): the set \(\{0,1,2,3,4,5,6\}\) induces a bipartite subgraph - \(f(G) \le 6\): the largest induced forest has at most 6 vertices - \(l_{\mathrm{avg}}(G) = 92/79\) - \(\lceil b(G) / l_{\mathrm{avg}}(G) \rceil \ge 7 > 6 \ge f(G)\)

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture58.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture58.conjecture58

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/4bd72a06842a10e1b8d7bb0fd6b1ef5e6bd20210/FormalConjectures/WrittenOnTheWallII/GraphConjecture58.lean#L772.

WOWII Conjecture 58

For a connected graph G, the size f(G) of a largest induced forest satisfies f(G) ≥ ceil( b(G) / average l(v) ) where b(G) is the largest induced bipartite subgraph and l(v) is the independence number of G.neighborSet v.

This conjecture is false. A counterexample is the graph described in the module docstring above: a \(K_{3,3}\) joined to a \(K_{73}\) via vertex \(0\), giving \(\lceil b/l_{\mathrm{avg}} \rceil \ge 7 > 6 \ge f(G)\).

The counterexample has been found by Moritz Firsching and Goran Žužić using an experimental pipeline.

theorem conjecture58 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_hG : G.Connected),
      Nat.ceil (G.b / G.l_avg) ≤ G.largestInducedForestSize

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture58.lean, line 63.

Sources
LeanWrittenOnTheWallII.GraphConjecture58.conjecture58

TheoremWritten on the Wall II - Conjecture 59#

References: - E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture59.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture59.conjecture59

Solved: stated here; a Lean proof is at https://github.com/QDKStorm/wowii59-counterexample/blob/main/Counterexample59.lean; a Lean proof is at https://github.com/anagnorisis2peripeteia/formal-conjectures/blob/69388817d384ea44a5ef4b2aed1097c8281f9c3a/FormalConjectures/WrittenOnTheWallII/GraphConjecture59.lean.

WOWII Conjecture 59

For a simple connected graph \(G\), the size \(f(G)\) of a largest induced forest satisfies \(f(G) \ge \lceil \sqrt{\mathrm{residue}(G) \cdot b(G)} \rceil\), where \(\mathrm{residue}(G)\) is the Havel-Hakimi residue (the number of zeros remaining after applying the Havel-Hakimi algorithm to the degree sequence until termination) and \(b(G)\) is the size of a largest induced bipartite subgraph.

See: Favaron, Mahéo, Saclé (1991) for the residue; DeLaVina's Graffiti.pc for the conjecture.

This conjecture is false. There is a connected counterexample on 123 vertices with residue G = 101, b G = 122, and G.largestInducedForestSize = 111. Indeed, 101 * 122 = 12322 = 111 ^ 2 + 1, so the conjectured lower bound is 112.

There is also an 18-vertex counterexample. Take a bipartite chain graph on vertices 0, ..., 9, with parts {0, ..., 4} and {5, ..., 9}, a hub 10 adjacent to every core vertex, and leaves 11, ..., 17 attached at the hub. It has residue 10, b = 17, and largest induced forest 13. ⌈√170⌉ = 14, so it falsifies the bound.

theorem conjecture59 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_ : G.Connected),
      ⌈Real.sqrt ((residue G : ℝ) * b G)⌉ ≤ (G.largestInducedForestSize : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture59.lean, line 60.

Sources
LeanWrittenOnTheWallII.GraphConjecture59.conjecture59

TheoremWritten on the Wall II - Conjecture 61#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture61.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

WrittenOnTheWallII.GraphConjecture61.conjecture61

Open: stated without proof.

WOWII Conjecture 61

For a simple connected graph \(G\), the size \(f(G)\) of a largest induced forest satisfies \(f(G) \ge \mathrm{residue}(G) + \lceil \mathrm{diam}(G) / 3 \rceil\), where \(\mathrm{residue}(G)\) is the Havel-Hakimi residue and \(\mathrm{diam}(G)\) is the diameter of \(G\).

See: Favaron, Mahéo, Saclé (1991) for the residue; DeLaVina's Graffiti.pc for the conjecture.

theorem conjecture61 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    (residue G : ℝ) + ⌈(G.diam : ℝ) / 3⌉ ≤ (G.largestInducedForestSize : ℝ)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture61.lean, line 46.

Sources
LeanWrittenOnTheWallII.GraphConjecture61.conjecture61

TheoremWritten on the Wall II - Conjecture 63#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Counterexample

The conjecture is false for the lexicographic product \(C_5[K_4]\). This graph has minimum even-distance count \(9\), while its largest induced forest and largest induced bipartite subgraph both have order \(4\). The conjectured lower bound is therefore \(\lceil(9 + 4 + 1)/3\rceil = 5 > 4\).

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture63.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture63.conjecture63

Solved: stated here; a Lean proof is at https://github.com/Kuberwastaken/wowii-63-85-counterexample/blob/cba739842ec59adf7426c180009175b31935701d/lean/WOWII63.lean#L184-L195.

WOWII Conjecture 63 asked whether every simple connected graph \(G\) satisfies \(f(G) \geq \lceil(\min_v \operatorname{distEven}(v) + b(G) + 1)/3\rceil\). The answer is no, as witnessed by \(C_5[K_4]\).

theorem conjecture63 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) (_h : G.Connected),
      let minDistEven := (Finset.univ.image (G.distEven ·)).min' (by simp)
      ⌈((minDistEven : ℝ) + G.b + 1) / 3⌉ ≤ (G.largestInducedForestSize : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture63.lean, line 49.

Sources
LeanWrittenOnTheWallII.GraphConjecture63.conjecture63

TheoremWritten on the Wall II - Conjecture 64#

References: - E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc - J. J. Gebendorfer, Clique Blow-ups of the 5-Cycle and Written on the Wall II Conjecture 64

Gebendorfer recorded the disproof on 26 July 2026, crediting Kuberwastaken's earlier \(C_5[K_4]\) certificate for the graph and its induced-forest computation. The linked Lean certificate formalizes this 20-vertex counterexample.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture64.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture64.conjecture64

Solved: stated here; a Lean proof is at https://github.com/Kuberwastaken/c5-k4/blob/8c0a76079e5c7153bdc2dd6d97a9821ee25b2620/lean/GraphConjecture64.lean.

WOWII Conjecture 64 proposed that every finite simple connected graph \(G\) satisfies

\[ f(G) \geq \left\lceil\sqrt{\alpha(G)\bigl(1+(|V(G)|\bmod\Delta(G))\bigr)}\right\rceil, \]

where \(f(G)\) is the maximum order of an induced forest. For \(C_5[K_4]\), the forest number is \(4\), the independence number is \(2\), and the proposed lower bound is \(\lceil\sqrt{2(1+9)}\rceil=5\).

The remainder and product in the radicand are computed in \(\mathbb{N}\) before coercion to \(\mathbb{R}\). Nontriviality excludes the one-vertex graph, whose maximum degree is zero.

theorem conjecture64 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_h : G.Connected),
      ⌈Real.sqrt ((G.indepNum * (1 + Fintype.card α % G.maxDegree) : ℕ) : ℝ)⌉ ≤
        (G.largestInducedForestSize : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture64.lean, line 56.

Sources
LeanWrittenOnTheWallII.GraphConjecture64.conjecture64

TheoremWritten on the Wall II - Conjecture 65#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Counterexample

The conjecture is false. Start with the path \(v_0-v_1-\cdots-v_{12}\) and attach one triangle at \(v_1\) and another at \(v_{11}\). The resulting graph has \(17\) vertices. Its Graph_6 string is PhCGGC@?G?_@?@O?G?G?G?@C. Its only minimum-degree vertices are \(v_0\) and \(v_{12}\), at distance \(12\), while its only maximum-degree vertices are \(v_1\) and \(v_{11}\), at distance \(10\). Thus the conjectured lower bound is \(12 + \lceil 10/3 \rceil = 16\).

Every induced forest must omit at least one vertex from each of the two vertex-disjoint triangles, so it has at most \(15\) vertices. Conversely, deleting one non-path vertex from each triangle leaves a tree on \(15\) vertices.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture65.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved. It also has 8 API statements, counted here but not shown.

WrittenOnTheWallII.GraphConjecture65.conjecture65

Proved here.

WOWII Conjecture 65:

Does every simple connected graph \(G\) satisfy \(f(G) \ge \operatorname{dist\_min}(A) + \lceil \operatorname{dist\_min}(M) / 3 \rceil\), where \(A\) is the set of minimum-degree vertices, \(M\) is the set of maximum-degree vertices, and \(\operatorname{dist\_min}(S)\) is the minimum distance between two distinct vertices of \(S\) (see distMin).

The answer is no. Counterexample.graph has a conjectured lower bound of \(16\), but every induced forest in it has at most \(15\) vertices.

theorem conjecture65 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_hG : 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 : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture65.lean, line 175.

Sources
LeanWrittenOnTheWallII.GraphConjecture65.conjecture65

TheoremWritten 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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture72.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

WrittenOnTheWallII.GraphConjecture72.conjecture72

Open: stated without proof.

WOWII Conjecture 72

For a simple connected graph G, \(\operatorname{tree}(G) ≥ ⌈\operatorname{ecc}_{\mathrm{avg}}(G) + \max_v \lambda(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.

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 : ℝ)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture72.lean, line 53.

Sources
LeanWrittenOnTheWallII.GraphConjecture72.conjecture72

TheoremWritten 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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture84.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

WrittenOnTheWallII.GraphConjecture84.conjecture84

Open: stated without proof.

WOWII Conjecture 84 (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.

theorem conjecture84 (G : SimpleGraph α) [DecidableRel G.Adj]
    (h : G.Connected) (hδ : 0 < G.minDegree) :
    2 * (G.radius.toNat : ℝ) / (G.minDegree : ℝ) ≤ (largestInducedTreeSize G : ℝ)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture84.lean, line 58.

Sources
LeanWrittenOnTheWallII.GraphConjecture84.conjecture84

TheoremWritten on the Wall II - Conjecture 85#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Counterexample

The conjecture is false for the lexicographic product \(C_5[K_4]\). This graph has minimum even-distance count \(9\) and largest induced-tree order \(4\). The conjectured lower bound is therefore \(\lceil\sqrt{1 + 2 \cdot 9}\rceil = \lceil\sqrt{19}\rceil = 5 > 4\).

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture85.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture85.conjecture85

Solved: stated here; a Lean proof is at https://github.com/Kuberwastaken/wowii-63-85-counterexample/blob/cba739842ec59adf7426c180009175b31935701d/lean/WOWII85.lean#L171-L183.

WOWII Conjecture 85 asked whether every simple connected graph \(G\) satisfies \(\operatorname{tree}(G) \geq \lceil\sqrt{1 + 2\min_v \operatorname{distEven}(v)}\rceil\). The answer is no, as witnessed by \(C_5[K_4]\).

theorem conjecture85 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) (_h : G.Connected),
      let minDistEven := (Finset.univ.image (G.distEven ·)).min' (by simp)
      ⌈Real.sqrt (1 + 2 * (minDistEven : ℝ))⌉ ≤
        (G.largestInducedTreeSize : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture85.lean, line 50.

Sources
LeanWrittenOnTheWallII.GraphConjecture85.conjecture85

TheoremWritten 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

This conjecture is false: Max Talwar found an 11-vertex counterexample (graph6 JBza_CB?wF_): take K₃,₃ minus an edge together with a K₅, joined by two edges into one K₅-vertex. There the average neighbourhood independence number is exactly 2, the largest induced forest has 6 vertices, and the largest induced bipartite subgraph has 8, so the conjectured bound reads 8 ≤ 1 + 6·⌈2⌉/2 = 7.

References: - E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc - Counterexample certificate for WOWII 91 (Max Talwar)

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture91.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture91.conjecture91

Solved: stated here without proof.

WOWII Conjecture 91 (disproved, 2026):

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.

Disproved by an 11-vertex counterexample (Max Talwar, 2026; graph6 JBza_CB?wF_) with b(G) = 8, f(G) = 6 and l G = 2, violating 8 ≤ 1 + 6·⌈2⌉/2 = 7.

theorem conjecture91 :
    ¬ ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α],
      ∀ (G : SimpleGraph α) (_ : G.Connected),
        b G ≤ 1 + (G.largestInducedForestSize : ℝ) * ⌈l G⌉ / 2

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture91.lean, line 64.

Sources
LeanWrittenOnTheWallII.GraphConjecture91.conjecture91

TheoremWritten 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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture96.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

WrittenOnTheWallII.GraphConjecture96.conjecture96

Open: stated without proof.

WOWII Conjecture 96

For a simple connected graph G on at least two vertices, α(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.

We record the nontrivial-graph version: the literal source inequality fails on \(K_1\), where the independence number and even-distance count are both one, but the maximum local independence number is zero, giving \(1 ≤ 0\).

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)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture96.lean, line 56.

Sources
LeanWrittenOnTheWallII.GraphConjecture96.conjecture96

TheoremWritten on the Wall II - Conjecture 100#

Verbatim statement (WOWII #100, status O):

If G is a simple connected graph, then α(G) ≤ CEIL[(maximum of λ(v) + 0.5*length(Ḡ))/2]

Source: http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj100

The WOWII HTML uses length(Ḡ) (the bar denotes graph complement); the extracted JSON in our private repo previously dropped the overline. The formal statement below uses the Euclidean norm of the degree sequence of Gᶜ.

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Definition of graph length

The WOWII definitions popup defines length(H) as the square root of the sum of the squares of the vertex degrees. This is degreeL2Norm H in Lean. Combined with the overline above, the inequality reads: α(G) ≤ ⌈(max_v l(v) + 0.5 · degreeL2Norm(Gᶜ)) / 2⌉ where l(v) = indepNeighbors G v.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture100.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture100.conjecture100

Solved: stated here; a Lean proof is at https://github.com/DomTheDeveloper/formal-conjectures/blob/0a0d23bdfcea605892146b039dfbdd4896229b32/FormalConjectures/WrittenOnTheWallII/100.lean.

WOWII Conjecture 100 (status O):

For a simple connected graph G, α(G) ≤ ⌈(max_v l(v) + 0.5 · degreeL2Norm(Gᶜ)) / 2⌉ where α(G) = G.indepNum is the independence number, max_v l(v) is the maximum over all vertices of the independence number of the neighbourhood (in G), and degreeL2Norm(Gᶜ) is the square root of the sum of the squares of the degrees in the complement Gᶜ.

Proof outline. Choose a maximum independent set S, write A = |S|, let T be its complement, and let L be the maximum neighbourhood independence number. Connectedness gives at least one edge from every vertex of S into T, while each vertex of T has at most L neighbours in S; double counting therefore gives A ≤ |T|L. In the complement graph, S is a clique. The missing cross-edges force explicit lower bounds on the complement degrees of vertices in both S and T. Summing their squares gives a lower bound for degreeL2Norm(Gᶜ)², and the resulting quadratic inequality rearranges to the stated ceiling bound.

Provenance. Solved by Dominic Dabish.

ProofOrchestrator, using OpenAI GPT-5.6 Thinking, assisted with the mathematical argument and Lean formalization; all formal claims were checked by the pinned Lean compiler.

theorem conjecture100 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    let maxL := (Finset.univ.image (indepNeighborsCard G)).max' (by simp)
    (G.indepNum : ℝ) ≤ ⌈((maxL : ℝ) + (1 / 2) * (degreeL2Norm Gᶜ : ℝ)) / 2⌉

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture100.lean, line 83.

Sources
LeanWrittenOnTheWallII.GraphConjecture100.conjecture100

TheoremWritten on the Wall II - Conjecture 101#

References: - E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc - [LM11] V. E. Levit and E. Mandrescu, A Set and Collection Lemma, 2011, Corollaries 2.3–2.4. - [Li26] Wentao Li, Lean proof of WOWII 101, 2026.

Definitions

The \(\alpha\)-core of a graph \(G\), written alphaCore G, is the set of vertices \(v\) such that removing \(v\) strictly decreases the independence number:

\[\mathrm{alphaCore}(G) = \{v \mid \alpha(G - v) < \alpha(G)\}\]

where \(G - v\) is the subgraph of \(G\) induced on \(V(G) \setminus \{v\}\).

These vertices are also called "critical vertices for independence."

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture101.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture101.conjecture101

Solved: stated here; a Lean proof is at https://github.com/VictorLiwentao/lean-graph-proofs/blob/9ce66be23570e0a9c8a6ae3f19f52e642878a8a9/LeanGraphProofs/WOWII101.lean#L318.

WOWII Conjecture 101

For a simple connected graph \(G\), \(\alpha(G) \le \lfloor (n + |\mathrm{alphaCore}(G)|) / 2 \rfloor\) where \(\alpha(G) = G.\mathrm{indepNum}\) is the independence number, \(n\) is the number of vertices, and \(\mathrm{alphaCore}(G)\) is the set of vertices whose removal decreases the independence number.

This is Hajnal's inequality in its independent-set form; see [LM11].

Lean formalization by Wentao Li, with AI assistance; see [Li26].

theorem conjecture101 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    G.indepNum ≤ (Fintype.card α + (alphaCore G).card) / 2

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture101.lean, line 72.

Sources
LeanWrittenOnTheWallII.GraphConjecture101.conjecture101

TheoremWritten on the Wall II - Conjecture 103#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture103.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.

WrittenOnTheWallII.GraphConjecture103.conjecture103

Proved here.

WOWII Conjecture 103

For a simple connected graph \(G\), \(\alpha(G) \le \lfloor b(G) - \ln(\mathrm{ecc\_avg}(G)) \rfloor\) where \(\alpha(G) = G.\mathrm{indepNum}\) is the independence number, \(b(G)\) is the largest induced bipartite subgraph size, and \(\mathrm{ecc\_avg}(G) = G.\mathrm{averageEccentricity}\) is the average eccentricity of \(G\). Uses Real.log (natural logarithm).

This conjecture is false. The graph wowii103Counterexample has independence number \(9\), largest induced bipartite subgraph size \(10\), and average eccentricity \(30/11\). Since \(1 < \ln(30/11) < 2\), the proposed upper bound is \(8\).

theorem conjecture103 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) (_h : G.Connected),
      (G.indepNum : ℝ) ≤ ⌊b G - Real.log (averageEccentricity G)⌋

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture103.lean, line 96.

Sources
LeanWrittenOnTheWallII.GraphConjecture103.conjecture103

TheoremWritten on the Wall II - Conjecture 109#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture109.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture109.conjecture109

Solved: stated here; a Lean proof is at https://github.com/DomTheDeveloper/formal-conjectures/blob/cf59008ef1cd432bf9803275dcf5d62ab1f094a3/FormalConjectures/WrittenOnTheWallII/GraphConjecture109.lean; a Lean proof is at https://github.com/chelokot/wowii-109-counterexample/blob/543a66ee78565b553f4ba6dc7fd32b5610557913/lean/GraphConjecture109.lean#L29-L139.

WOWII Conjecture 109

For a simple connected graph \(G\), the independence number \(\alpha(G)\) was conjectured to satisfy \(\alpha(G) \le \lfloor (\mathrm{residue}(G) + 2 \cdot b(G)) / 3 \rfloor\), where \(\mathrm{residue}(G)\) is the Havel--Hakimi residue and \(b(G)\) is the size of a largest induced bipartite subgraph.

This is false. A connected graph on 21 vertices has an independent set of size 15, residue 8, and no induced bipartite subgraph with more than 18 vertices, so the conjectured right-hand side is at most 14.

A smaller counterexample is the connected 13-vertex graph \(\overline K_7 \vee (K_3 \sqcup K_3)\). It has independence number \(7\), residue \(2\), and largest induced bipartite subgraph size \(9\), so its conjectured right-hand side is \(6\).

theorem conjecture109 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_h : G.Connected),
      (G.indepNum : ℝ) ≤ ⌊((residue G : ℝ) + 2 * b G) / 3⌋

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture109.lean, line 56.

Sources
LeanWrittenOnTheWallII.GraphConjecture109.conjecture109

TheoremWritten on the Wall II - Conjecture 133#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture133.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

WrittenOnTheWallII.GraphConjecture133.conjecture133

Open: stated without proof.

WOWII Conjecture 133:

For a simple connected graph \(G\), \(\operatorname{path}(G) \ge \operatorname{rad}(G) + (\mathrm{avg}_v\, l(v))^{cC_4(G)}\), where \(\operatorname{path}(G)\) is the path number of the graph (number of vertices of a largest induced path), \(\operatorname{rad}(G)\) is the radius (minimum eccentricity, as a natural number), \(\mathrm{avg}_v\, l(v) = l(G)\) is the average independence number of vertex neighbourhoods, and \(cC_4(G)\) is the \(C_4\)-free characteristic function (1 if \(G\) is \(C_4\)-free, not necessarily induced, and 0 otherwise).

theorem conjecture133 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    let rad := G.radius.toNat
    let hasC4 := ∃ a b c d : α, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ∧
      G.Adj a b ∧ G.Adj b c ∧ G.Adj c d ∧ G.Adj d a
    let cC4 : ℕ := if hasC4 then 0 else 1
    (rad : ℝ) + l G ^ cC4 ≤ (path G : ℝ)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture133.lean, line 48.

Sources
LeanWrittenOnTheWallII.GraphConjecture133.conjecture133

TheoremWritten on the Wall II - Conjecture 141#

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture141.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

WrittenOnTheWallII.GraphConjecture141.conjecture141

Proved here.

WOWII Conjecture 141

For a simple connected graph \(G\), \(\mathrm{tree}(G) \ge (1/2) \cdot \mathrm{girth}(G) - 1 + \max_v l(v)\) where \(\mathrm{tree}(G)\) is the number of vertices of a largest induced tree subgraph, \(\mathrm{girth}(G)\) is the length of the shortest cycle (\(0\) if acyclic), and \(l(v)\) (indepNeighborsCard G v) is the independence number of the neighbourhood of \(v\).

theorem conjecture141 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    (G.girth : ℝ) / 2 - 1 + ((Finset.univ.sup (indepNeighborsCard G) : ℕ) : ℝ) ≤
    (largestInducedTreeSize G : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/WrittenOnTheWallII/GraphConjecture141.lean, line 45.

Sources
LeanWrittenOnTheWallII.GraphConjecture141.conjecture141

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.