Skip to content

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

TheoremWritten on the Wall II - Conjecture 142#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture142.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.GraphConjecture142.conjecture142

Solved: stated here; a Lean proof is at https://github.com/AlperTheKing/formal-conjectures/blob/46bf39015f5c3c3ba3bfcf9f752b4b1e49b584ac/FormalConjecturesForMathlib/WrittenOnTheWallII/GraphConjecture142Proof.lean#L3927-L3932.

WOWII Conjecture 142:

For a simple connected graph \(G\), \(\mathrm{tree}(G) \ge (2/3) \cdot \mathrm{girth}(G) + \mathrm{ecc}(B)\) where \(\mathrm{tree}(G)\) is the largest induced tree size, \(\mathrm{girth}(G)\) is the length of the shortest cycle (\(0\) if acyclic), \(B\) is the set of boundary vertices (those of maximum eccentricity), and \(\mathrm{ecc}(B)\) is the eccentricity of the set \(B\).

Proof sketch. The proof first strengthens the real-valued target to the integral bound

\[ \mathrm{ecc}(B) + \mathrm{girth}(G) - \lfloor \mathrm{girth}(G) / 3 \rfloor \leq \mathrm{tree}(G). \]

For a cyclic graph, start with a shortest cycle \(K\). It is chordless, so removing one vertex leaves an induced path on \(\mathrm{girth}(G)-1\) vertices. Shortest paths from selected vertices to \(K\) are called descents. Pairwise noninteracting descents attach to the retained cycle path as disjoint branches. If two descents interact, the proof cuts at the first interaction encountered from the outer endpoint toward the cycle and splices the paths there. Minimality of that interaction makes the retained prefix disjoint and nonadjacent to the first descent; geodesicity excludes chords, while girth at least five rules out extra cross-edges and cycle attachments.

Choose a vertex realizing \(\mathrm{ecc}(B)\) and two endpoints of a diametral geodesic. Either two of their descents interact, directly giving a sufficiently long spliced tree, or all three are separate, in which case a three-point distance inequality forces their total length to be large enough. This proves the integral bound in the main range. Girths three and four, small \(\mathrm{ecc}(B)\), and the two remaining congruence cases are handled by separate geodesic/cycle certificates with one or two descents; the acyclic case follows from a diametral path. Finally,

\[ \mathrm{girth}(G)-\lfloor\mathrm{girth}(G)/3\rfloor = \lceil 2\,\mathrm{girth}(G)/3\rceil \geq 2\,\mathrm{girth}(G)/3, \]

which gives the stated real-valued inequality.

The argument was developed with assistance from ChatGPT Pro. The linked Lean 4 formalization was produced with assistance from OpenAI Codex and checked by Lean.

theorem conjecture142 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    let B : Set α := (maxEccentricityVertices G : Set α)
    (2 : ℝ) / 3 * (G.girth : ℝ) + (eccSet G B : ℝ) ≤ (largestInducedTreeSize G : ℝ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture142.conjecture142

TheoremWritten on the Wall II - Conjecture 143#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture143.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.GraphConjecture143.conjecture143

Proved here.

WOWII Conjecture 143:

For a simple connected graph \(G\), \(\mathrm{tree}(G) \ge (\mathrm{girth}(G) + 1) / \sigma(G)\), where \(\mathrm{tree}(G)\) is the largest induced tree size, \(\mathrm{girth}(G)\) is the length of the shortest cycle, and \(\sigma(G) = G.\mathrm{secondSmallestDegree}\) is the second-smallest degree of \(G\)'s degree sequence (per WOWII defEntry 65). We state the inequality in denominator-free form to avoid the \(\sigma = 0\) corner case (\(n \le 1\)).

The proof splits into the acyclic case and two cyclic cases. For an acyclic graph the girth is zero. If \(\sigma \ge 2\), deleting two consecutive edges from a shortest cycle leaves an induced tree on \(\mathrm{girth}(G)-1\) vertices, and the factor \(\sigma \ge 2\) yields the required inequality. If \(\sigma = 1\), there are two degree-one vertices. A maximal induced tree containing them must have an external vertex with two attachments; those attachments create a cycle whose length forces the tree to contain at least \(\mathrm{girth}(G)+1\) vertices.

theorem conjecture143 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected)
    (hσ : 0 < secondSmallestDegree G) :
    (G.girth : ℝ) + 1 ≤ (largestInducedTreeSize G : ℝ) * (secondSmallestDegree G : ℝ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture143.conjecture143

TheoremWritten on the Wall II - Conjecture 144#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture144.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.GraphConjecture144.conjecture144

Solved: stated here; a Lean proof is at https://github.com/beowulf127/wowii144-lean/blob/046429d509b28c90ee2ec38ae27c1ad377c6a5fc/WOWII144/Main.lean.

WOWII Conjecture 144

For a simple connected graph \(G\), \(\mathrm{tree}(G) \ge \mathrm{girth}(G) - 1 + \mathrm{ecc}(\mathrm{Centers})\) where \(\mathrm{tree}(G)\) is the largest induced tree size, \(\mathrm{girth}(G)\) is the length of the shortest cycle (\(0\) if acyclic), \(\mathrm{Centers} = G.\mathrm{center}\) is the set of vertices with minimum eccentricity (the center of \(G\)), and \(\mathrm{ecc}(\mathrm{Centers})\) is the eccentricity of the center set — the maximum distance from any non-center vertex to the nearest center vertex.

Proof sketch. Let \(g = \mathrm{girth}(G)\) and \(e = \mathrm{ecc}(G, \mathrm{center}(G))\). The acyclic and \(e = 0\) cases are immediate. If \(g \le e + 2\), the formalized Bacsó--Tuza induced-path argument, with an elementary \(e = 1\) case, produces an induced tree on at least \(2e + 1\) vertices. Since \(g - 1 + e \le 2e + 1\), this proves the result.

Suppose instead that \(e + 3 \le g\), and fix a shortest cycle \(C\). Removing one vertex of \(C\) leaves an induced tree on \(g - 1\) vertices. Analyze the connected components outside \(C\). If one has at least \(e\) vertices, it supplies an attached rooted induced tree of order \(e\). Otherwise, let \(D\) be the sum of the components' attachment depths. If \(D \ge e\), select pairwise edge-separated rooted branches of total order \(e\) and attach them to \(C\), deleting a suitable cycle vertex. If \(D < e\), shortest-cycle contact restrictions bound corresponding exclusion arcs. Their complement consists of central cycle vertices and \(D\)-dominates the graph, forcing \(e \le D\), a contradiction.

Finite graph search was used only during discovery to test candidate structural lemmas and reject false proof templates; no finite-search result is used in the universal proof.

theorem conjecture144 (G : SimpleGraph α) (h : G.Connected) :
    (G.girth : ℝ) - 1 + (ecc G G.center : ℝ) ≤ (largestInducedTreeSize G : ℝ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture144.conjecture144

TheoremWritten on the Wall II - Conjecture 145#

The WOWII HTML uses \(\lambda_{\min}(\overline{G})\) (the bar denotes graph complement). The formal statement below uses the local-independence minimum of \(G^c\).

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

Definitions

The local independence minimum \(\mathrm{lMin}(G)\) is:

\[\mathrm{lMin}(G) = \min_{v \in V(G)} l(v)\]

where \(l(v) = \mathrm{indepNeighborsCard}(G, v)\) is the independence number of the neighbourhood of \(v\). This is the minimum over all vertices of the local independence number.

The boundary vertices \(B(G)\) of a connected graph are the vertices \(v\) such that the eccentricity of \(v\) equals the diameter of \(G\).

The eccentricity of a set \(\mathrm{ecc}(S) = \max_{u \notin S} \min_{w \in S} \mathrm{dist}(u, w)\). In the conjecture below, \(\mathrm{ecc}(B)\) is the eccentricity of the boundary set.

Conjecture 145: \(\mathrm{tree}(G) \ge 2 \cdot \mathrm{ecc}(B) / \lambda_{\min}(\overline{G})\) where \(\mathrm{tree}(G)\) is largestInducedTreeSize G, \(\mathrm{ecc}(B)\) is the eccentricity of the boundary vertices, and \(\lambda_{\min}(\overline{G})\) is the local independence minimum of the complement \(\overline{G}\).

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture145.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.GraphConjecture145.conjecture145

Solved: stated here; a Lean proof is at https://github.com/DomTheDeveloper/crl/blob/2ee448baa80c98f0c8b9a0c1c3d9421200f99aa5/math/wowii145/WOW145/145.lean.

WOWII Conjecture 145

For a simple connected graph \(G\), \(\mathrm{tree}(G) \ge 2 \cdot \mathrm{ecc}(B) / \lambda_{\min}(\overline{G})\) where \(\mathrm{tree}(G)\) is the number of vertices in a largest induced subtree, \(\mathrm{ecc}(B)\) is the eccentricity of the boundary vertices (eccSet and boundaryVertices), and \(\lambda_{\min}(\overline{G})\) is the minimum local independence number of the complement graph.

We state the inequality in the form \(\mathrm{tree}(G) \cdot \mathrm{lMin}(\overline{G}) \ge 2 \cdot \mathrm{ecc}(B)\) to avoid division.

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 conjecture145 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected)
    (hlMin : 0 < localIndependenceMin Gᶜ) :
    2 * eccSet G (maxEccentricityVertices G : Set α) ≤
    largestInducedTreeSize G * localIndependenceMin Gᶜ

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

Sources
LeanWrittenOnTheWallII.GraphConjecture145.conjecture145

TheoremWritten on the Wall II - Conjecture 146#

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

Definitions

The square of a graph \(G\), denoted \(G^2\), is the graph on the same vertex set where two distinct vertices are adjacent if and only if their distance in \(G\) is at most \(2\).

The radius of \(G^2\) is the minimum eccentricity of any vertex in \(G^2\), i.e.,

\[\mathrm{rad}(G^2) = \min_{v \in V} \max_{u \in V} \mathrm{dist}_{G^2}(u, v).\]

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture146.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.GraphConjecture146.conjecture146

Solved: stated here; a Lean proof is at https://github.com/akakabrian/WOW-146/blob/f9e0ad75d829170804ce1d8f9fd4c1d4a0085203/WOW146/Conjecture146.lean.

WOWII Conjecture 146

For a simple connected graph \(G\), \(\mathrm{tree}(G) \ge 2 \cdot \mathrm{ecc}(B) / \mathrm{rad}(G^2)\) where \(\mathrm{tree}(G)\) is the number of vertices in a largest induced subtree, \(\mathrm{ecc}(B)\) is the eccentricity of the boundary vertices of \(G\) (eccSet and maxEccentricityVertices), and \(\mathrm{rad}(G^2)\) is the radius of the square graph of \(G\).

We state the inequality in the form \(\mathrm{tree}(G) \cdot \mathrm{rad}(G^2) \ge 2 \cdot \mathrm{ecc}(B)\) to avoid division.

Informal proof

Write \(t\) for the largest induced-tree order, \(r\) and \(d\) for the radius and diameter of \(G\), and \(p\) for the eccentricity of its peripheral set. First, the distance in the graph square is \(\operatorname{dist}_{G^2}(u,v)=\lceil\operatorname{dist}_G(u,v)/2\rceil\), so \(\operatorname{rad}(G^2)=\lceil r/2\rceil\). A diametral geodesic is an induced path, giving \(t\ge d+1\), while \(p\le d-1\). These bounds settle every case except \(r=2\), \(d=4\), and \(p=3\). In that remaining configuration, choose a centre and shortest paths to two diametral vertices and to a vertex at distance three from the peripheral set. A finite case analysis on the two possible cross-arm edges (and then the possible chords) always produces an induced tree on at least six vertices. Hence \(t\,\operatorname{rad}(G^2) \ge 2p\) in the exceptional case as well.

theorem conjecture146 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected)
    (hrad : 0 < graphSquareRadius G) :
    2 * eccSet G (maxEccentricityVertices G : Set α) ≤
    largestInducedTreeSize G * graphSquareRadius G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture146.conjecture146

TheoremWritten on the Wall II - Conjecture 172#

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

The conjecture is false for the graph D₉, formed from two triangles by joining distinguished vertices with a path of nine edges. It has at most four leaves in a spanning tree. Its peripheral vertices have degree two, while the two maximum-degree vertices of its square are at distance seven in the original graph, so the claimed inequality would give 4 ≥ 8.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture172.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.GraphConjecture172.conjecture172

Solved: stated here; a Lean proof is at https://github.com/Kuberwastaken/c5-k4/blob/a948106ad2d2a5d291b6b99575fe78bf373e7e02/lean/GraphConjecture172.lean#L1-L384.

WOWII Conjecture 172 asked whether every nontrivial finite connected simple graph G satisfies Ls G ≥ -1 + Δ(B(G)) + dist_min(G, M(G²)). The answer is no, witnessed by D₉.

theorem conjecture172 :
    ¬ ∀ (V : Type) [Fintype V] [DecidableEq V] [Nontrivial V]
      (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected →
        Ls G ≥ (-1 : ℝ) + peripheryMaxDegree G +
          distMin G (squareMaximumDegreeVertices G)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture172.conjecture172

TheoremWritten on the Wall II - Conjecture 176#

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

The conjecture is false for the graph D₇, formed from two triangles by joining distinguished vertices with a path of seven edges. It has at most four leaves in a spanning tree and largest induced bipartite subgraph order ten. The two maximum-degree vertices of its square are at distance five in the original graph, so the claimed inequality would give 14 ≥ 17.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture176.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.GraphConjecture176.conjecture176

Solved: stated here; a Lean proof is at https://github.com/Kuberwastaken/c5-k4/blob/b0ba2b9206176b4fc30bd633de206ac230b4e01f/lean/GraphConjecture176.lean#L1-L377.

WOWII Conjecture 176 asked whether every nontrivial finite connected simple graph G satisfies Ls(G) + b(G) ≥ n(G) + dist_min(G, M(G²)). The answer is no, witnessed by D₇.

theorem conjecture176 :
    ¬ ∀ (V : Type) [Fintype V] [DecidableEq V] [Nontrivial V]
      (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected →
        Ls G + b G ≥ (Fintype.card V : ℝ) +
          distMin G (squareMaximumDegreeVertices G)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture176.conjecture176

TheoremWritten on the Wall II - Conjecture 181#

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

The expression deg_avg(B(G²)) is formalized by measuring degrees in G², the graph whose maximum-eccentricity vertices induce B(G²).

The conjecture is false for the triangular graph T(7) = L(K₇): it has at most 16 leaves in a spanning tree, largest induced bipartite subgraph order 6, and independence number 3. Its square is K₂₁, whose vertices all have degree 20, so the claimed inequality would give 22 ≥ 23.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture181.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.GraphConjecture181.conjecture181

Solved: stated here; a Lean proof is at https://github.com/Kuberwastaken/c5-k4/blob/3bfa33d7470055a9a11d9ffde29186245dc3a329/lean/GraphConjecture181.lean#L1-L381.

WOWII Conjecture 181 asked whether every nontrivial finite connected simple graph G satisfies

Ls G + b G ≥ G.indepNum + deg_avg(B(G²)).

The answer is no, witnessed by T(7) = L(K₇).

theorem conjecture181 :
    ¬ ∀ (V : Type) [Fintype V] [DecidableEq V] [Nontrivial V]
      (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected →
        Ls G + b G ≥ G.indepNum + squarePeripheryAverage G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture181.conjecture181

TheoremWritten 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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture189.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.GraphConjecture189.conjecture189

Open: stated without proof.

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

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

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

Sources
LeanWrittenOnTheWallII.GraphConjecture189.conjecture189

TheoremWritten on the Wall II - Conjecture 194#

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

Counterexample

The conjecture is false. Take a clique on vertices 0, ..., 10, four additional vertices 11, ..., 14 adjacent to every clique vertex, and three leaves attached at 11, 12, and 14. This connected graph has independence number 4, while the sum of the independence numbers of its vertex neighbourhoods is 54, so their average is 3. Thus it satisfies the conjecture's hypothesis with equality. However, its three leaves would all have to be endpoints of a Hamiltonian path, which is impossible.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture194.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.GraphConjecture194.conjecture194

Solved: stated here; a Lean proof is at https://github.com/anagnorisis2peripeteia/formal-conjectures/blob/4bff865a14c2cd61fefbffbe9c49cbfc5a89ac45/FormalConjectures/WrittenOnTheWallII/GraphConjecture194.lean#L128-L140.

WOWII Conjecture 194

For a simple connected graph G, if α(G) ≤ 1 + l_avg(G), then G has a Hamiltonian path. Here α(G) = G.indepNum is the independence number, and l_avg(G) = averageIndepNeighbors G is the average over all vertices of the independence number of the neighbourhood. A Hamiltonian path is a walk visiting every vertex exactly once. The answer is no, as witnessed by the 18-vertex graph described above.

Counterexample (Graph6): Q~~~~~~~~~~~~}~}^~??G??_??_

theorem conjecture194 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) (_h : G.Connected),
      (G.indepNum : ℝ) ≤ 1 + averageIndepNeighbors G →
      ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian

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

Sources
LeanWrittenOnTheWallII.GraphConjecture194.conjecture194

TheoremWritten on the Wall II - Conjecture 198a#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture198a.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.GraphConjecture198a.conjecture198a

Solved: stated here; a Lean proof is at https://github.com/lukekabbash/wowii-198a-lean/blob/49f080bbaee83821e9e9744eef14c5acaae2a101/lean/src/ConditionalMain.lean#L52-L57.

WOWII Conjecture 198a

For a simple connected graph G, if b(G) ≤ 2 + ecc_avg(G), then G has a Hamiltonian path. Here b(G) is the number of vertices in a largest induced bipartite subgraph, and ecc_avg(G) is the average eccentricity of G. A Hamiltonian path is a walk visiting every vertex exactly once.

Proofs and formalizations include: * Ben Cohen, Average Eccentricity, Induced Bipartite Subgraphs, and Hamiltonian Paths (July 21, 2026); Lean 4 formalization, publicly posted and verified September 16, 2026. * Luke Kabbash, A Hamiltonian-Path Criterion from Bipartite Number and Average Eccentricity; Lean 4 formalization publicly posted and passed its recorded verification July 23, 2026.

theorem conjecture198a (G : SimpleGraph α) (h : G.Connected)
    (hb : b G ≤ 2 + averageEccentricity G) :
    ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian

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

Sources
LeanWrittenOnTheWallII.GraphConjecture198a.conjecture198a

TheoremWritten 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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture199.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. It also has 4 test statements, counted here but not shown.

WrittenOnTheWallII.GraphConjecture199.conjecture199

Open: stated without proof.

WOWII Conjecture 199

For a simple connected graph G, if tree(G) - 2 ≤ κ(G), then G has a Hamiltonian path. The nontrivial vertex type encodes the source assumption \(n > 1\). Here tree(G) is the number of vertices in a largest induced tree and κ(G) = vertexConnectivity G is the vertex connectivity of G.

theorem conjecture199 (G : SimpleGraph α) (h : G.Connected)
    (hκ : largestInducedTreeSize G - 2 ≤ vertexConnectivity G) :
    ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian

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

Sources
LeanWrittenOnTheWallII.GraphConjecture199.conjecture199

TheoremWritten on the Wall II - Conjecture 200#

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

Counterexample

For every integer \(q \geq 5\), let \(C = \{a,b\} \cup D\) have \(q\) vertices and induce \(K_q\) minus the edge \(ab\). Add two nonadjacent vertices \(x,y\), each complete to \(C\); a vertex \(z\) adjacent exactly to \(a,b\); and, for every \(d \in D\), a pendant vertex \(p_d\) adjacent exactly to \(d\).

The local-neighbourhood independence numbers are \(2\) at \(x,y,z\), \(1\) at each \(p_d\), and \(3\) at every vertex of \(C\). Their sum is \(4q+4\), while the graph has \(2q+1\) vertices, so

\[\left\lceil 1 + l_{\mathrm{avg}}(G)\right\rceil = 4.\]

The vertices \(\{a,x,y,z\}\) induce a claw, and a case split on the number of vertices from \(C\) shows that no induced tree has more than four vertices. Thus \(\operatorname{tree}(G)=4\). Finally, the graph has \(q-2 \geq 3\) pendant vertices, but a Hamiltonian path has only two endpoints.

The smallest member of this family has 11 vertices and graph6 encoding J??FFBRq}N_. This is a smallest counterexample overall: an exhaustive search over all 11,989,760 connected graphs on 4 ≤ n ≤ 10 vertices (via nauty's geng; graphs on at most 3 vertices are trivially traceable) found no graph satisfying the premise without a Hamiltonian path.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture200.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.GraphConjecture200.conjecture200

Solved: stated here; a Lean proof is at https://github.com/infinityscroll/formal-conjectures/blob/9dd290db402c49922fa42793e4a7cfb802daf5c1/FormalConjectures/WrittenOnTheWallII/GraphConjecture200Counterexample.lean#L24-L195.

WOWII Conjecture 200

For a simple connected graph G, if tree(G) = ⌈1 + l_avg(G)⌉, then G has a Hamiltonian path. Here tree(G) is the number of vertices of a largest induced tree subgraph, and l_avg(G) = averageIndepNeighbors G is the average over all vertices of the independence number of the neighbourhood. A Hamiltonian path is a walk visiting every vertex exactly once.

This conjecture is false. The counterexample family in the module docstring satisfies the equality hypothesis and has no Hamiltonian path.

theorem conjecture200 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) (_h : G.Connected),
      (largestInducedTreeSize G : ℝ) = ⌈1 + averageIndepNeighbors G⌉ →
      ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian

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

Sources
LeanWrittenOnTheWallII.GraphConjecture200.conjecture200

TheoremWritten on the Wall II - Conjecture 217#

Per the WOWII definitions popup linked from this conjecture:

  • \(L(G)\) is the maximum number of leaves of a spanning tree of \(G\) — i.e. Ls G in our invariant library.
  • \(\chi_{\mathrm{residue}=2}(G)\) is the characteristic function for the predicate \(\mathrm{residue}\, G = 2\), i.e. \(1\) when \(\mathrm{residue}\, G = 2\) and \(0\) otherwise. It is not a connected-component count of any 2-core.

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture217.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.GraphConjecture217.conjecture217

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/wowii-graph-conjecture-217-lean/blob/6a2fb82fcd17aa15ec734736740794bb8bd194c0/lean/GraphConjecture217Audit.lean.

WOWII Conjecture 217:

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\).

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

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

Sources
LeanWrittenOnTheWallII.GraphConjecture217.conjecture217

TheoremWritten on the Wall II - Conjecture 291#

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

Definitions

For a vertex \(v\) in a graph \(G\), \(T(v)\) is the number of triangles (3-cliques) incident to \(v\), i.e., the number of 3-element cliques in \(G\) that contain \(v\).

The triangle-frequency of the minimum is the number of vertices that achieve the minimum value of \(T(v)\).

\(k\) is the first step in the Havel–Hakimi process at which a zero appears. Concretely, starting from the descending degree sequence \(s_0\) of \(G\), we set \(s_{i+1} = \mathrm{havelHakimiStep}\, s_i\) and let \(k\) be the least \(i \ge 0\) such that \(s_i\) contains a zero entry (or, vacuously, has been emptied entirely). Since each step is sorted descending and never increases entries, this is equivalent to the last (smallest) entry of \(s_i\) being \(0\), or \(s_i\) being \([]\).

This is strictly weaker than \(n - \mathrm{residue}(G)\): \(n - \mathrm{residue}(G)\) is the total number of reduction steps until every entry is zero, whereas \(k\) only requires that some entry has hit zero — and a \(0\) typically appears well before the all-zero state is reached.

Conjecture 291: For a simple connected graph \(G\) with \(n > 2\), \(\gamma_t(G) \le k + \mathrm{frequency}(t_{\min}(v))\) where \(\gamma_t(G)\) is the total domination number, \(k\) is the Havel-Hakimi zero step, and \(\mathrm{frequency}(t_{\min}(v))\) is the number of vertices achieving the minimum triangle count.

The conjecture is false: on July 23, 2026, Zyad Tamimi sent a 12-vertex counterexample with \(\gamma_t(G) = 4\), \(\mathrm{frequency}(t_{\min}(v)) = 1\) and \(k = 2\), and the source now lists Conjecture 291 as refuted.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture291.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.GraphConjecture291.conjecture291

Solved: stated here without proof.

WOWII Conjecture 291

For a simple connected graph \(G\) with \(n > 2\), \(\gamma_t(G) \le k + \mathrm{frequency}(t_{\min}(v))\) where:

  • \(\gamma_t(G)\) is the total domination number,
  • \(k\) is the first step in which a zero appears in the Havel-Hakimi process,
  • \(\mathrm{frequency}(t_{\min}(v))\) is the number of vertices achieving the minimum triangle count.

This is false: the source records a 12-vertex counterexample by Zyad Tamimi (July 23, 2026) with \(\gamma_t(G) = 4 > 2 + 1 = k + \mathrm{frequency}(t_{\min}(v))\).

The hypothesis \(n > 2\) is stated in the source's full list of conjectures (as for the neighbouring Conjectures 290, 292 and 293) but omitted on its list of open conjectures; the counterexample has \(12\) vertices, so it refutes both readings.

theorem conjecture291 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_h : G.Connected) (_hn : 2 < Fintype.card α),
      G.totalDominationNumber ≤ havelHakimiZeroStep G + freqMinTriangles G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture291.conjecture291

TheoremWritten on the Wall II - Conjecture 309#

References: - E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc - J. J. Gebendorfer, An Infinite Family of Counterexamples to Written on the Wall II, Conjecture 309

The conjecture is false for the clique blow-ups \(C_5[K_k]\) for every \(k \geq 3\).

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture309.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.GraphConjecture309.conjecture309

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

Does every finite simple connected graph \(G\) of order greater than two satisfy

\[ \gamma_t(G) \leq \frac{1}{2}\left( \max_v(\operatorname{distEven}(v)-\operatorname{evenHorizontal}(v))+ \min_{e\in E(\overline G)}|N_{\overline G}(e)|\right)? \]

Gebendorfer disproved the statement with the family \(C_5[K_k]\), \(k \geq 3\).

theorem conjecture309 : ¬ conjecture309Statement

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

Sources
LeanWrittenOnTheWallII.GraphConjecture309.conjecture309

TheoremWritten on the Wall II - Conjecture 314#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture314.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.GraphConjecture314.conjecture314

Solved: stated here; a Lean proof is at https://github.com/glyaea/wow-ii-314/blob/7b35f1252e4aaae3c787faf8091f9c7cd4edc41f/solution.lean.

WOWII Conjecture 314:

For every finite simple connected graph \(G\) with \(n > 1\) vertices, if \(G\) is triangle-free and \(\mathrm{path}(G) \le 4\), then \(G\) is well totally dominated.

Here \(\mathrm{path}(G) = \mathrm{largestInducedPathSize}\, G\) is the size of a largest induced path in \(G\), defined locally above.

Disambiguation. Earlier revisions of this file used the SimpleGraph.path invariant, but that is the floor of the average distance, not the size of a largest induced path — a different quantity that makes Conjecture 314 vacuous in many cases.

Proof summary. In a connected, \(K_{3}\)-free, induced-\(P_{5}\)-free graph \(G\):

  1. No minimal total dominating set has fewer than two vertices.
  2. No minimal total dominating set has more than three vertices.
  3. Minimal total dominating sets of sizes two and three cannot coexist.

Thus, each minimal total dominating set in \(G\) has the same size.

The Lean proof was generated by OpenAI GPT-5.6 Sol.

theorem conjecture314 [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj]
    (hG : G.Connected)
    (hTriFree : ∀ a b c : α, G.Adj a b → G.Adj b c → G.Adj c a → False)
    (hPath : largestInducedPathSize G ≤ 4) :
    IsWellTotallyDominated G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture314.conjecture314

TheoremWritten on the Wall II - Conjecture 315#

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

Definitions

The notions IsTotalDominatingSet, IsMinimalTotalDominatingSet, IsWellTotallyDominated, and pendantVertices live in FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.WellTotallyDominated.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture315.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.GraphConjecture315.conjecture315

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/9ef80e1a3709ed3eda43d9ed6ff1087681621041/FormalConjectures/WrittenOnTheWallII/GraphConjecture315.lean#L43.

WOWII Conjecture 315

Let \(G\) be a simple connected graph and let \(P\) denote the set of pendant vertices (vertices of degree \(1\)). If \(\alpha(G) = |P|\), then \(G\) is well totally dominated.

A formal proof of this conjectures has been obtained by Goran Žužić and Moritz Firsching using an experimental pipeline.

theorem conjecture315 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected)
    (h : G.indepNum = (pendantVertices G).card) :
    IsWellTotallyDominated G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture315.conjecture315

TheoremWritten on the Wall II - Conjecture 316#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture316.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.GraphConjecture316.conjecture316

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/wowii-graph-conjecture-316-lean/blob/3335e07151bc43e86d5c104dd30fee3596f06410/GraphConjecture316.lean.

WOWII Conjecture 316

Let G be a simple connected graph and let P denote the set of pendant vertices (vertices of degree 1). If |P| ≥ deg_avg(Gᶜ), then G is well totally dominated, where deg_avg(Gᶜ) is the average degree of the complement of G.

Proof sketch. In the trivial cases (P = ∅, or at most 2 vertices) G is complete, and complete graphs are well totally dominated. Otherwise the set C of non-pendant vertices satisfies |C| ≤ 3 and is a clique of G, and a case split on the set Q ⊆ C of neighbours of pendant vertices shows that G is well totally dominated.

theorem conjecture316 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected)
    (h : (averageDegree Gᶜ : ℚ) ≤ (pendantVertices G).card) :
    IsWellTotallyDominated G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture316.conjecture316

TheoremWritten on the Wall II - Conjecture 322#

Reference: E. DeLaViña, Written on the Wall II, Conjectures of Graffiti.pc

The source applies the local-independence hypothesis to the complement graph. Its conclusion also follows from the characterization of minimal total dominating sets of complete multipartite graphs in M. Subramanian and A. Selvakumar, Total Domination and Minimal Total Domination Polynomial of H-Join Graphs.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture322.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.GraphConjecture322.conjecture322

Proved here.

WOWII Conjecture 322

Let G be a simple connected graph on n ≥ 5 vertices. If the maximum over all vertices v of l(v) in the complement graph Gᶜ — the independence number of the neighborhood N(v) of v — is at most 1, then G is well totally dominated.

Here l(v) = α(Gᶜ[N(v)]) is the independence number of the subgraph induced by the open neighborhood of v in Gᶜ.

This proof was provided by Samuel Schlesinger.

theorem conjecture322 (G : SimpleGraph α) [DecidableRel G.Adj] (_hG : G.Connected)
    (hn : 5 ≤ Fintype.card α)
    (h : ∀ v : α, indepNeighborsCard Gᶜ v ≤ 1) :
    IsWellTotallyDominated G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture322.conjecture322

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.