Skip to content

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

TheoremWritten on the Wall II - Conjecture 160#

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

Definitions

For a vertex \(v\) in \(G\), \(T(v)\) is the number of triangles incident to \(v\):

\[T(v) = |\{\{u, w\} \subseteq N(v) \mid u \sim w\}|\]

i.e., the number of pairs of neighbors of \(v\) that are themselves adjacent.

The invariant maxTrianglesAtVertex G is the maximum of \(T(v)\) over all vertices.

Conjecture 160 uses both \(\max_v T(v)\) and \(\chi_{C_4}(G)\), the \(C_4\)-free characteristic function: it is 1 when \(G\) contains no cycle of length four and 0 otherwise. The cycle need not be induced. These invariants lower-bound the WOWII invariant \(L_s(G)\), the maximum number of leaves over all spanning trees of \(G\) (exposed as SimpleGraph.Ls G : ℝ).

The earlier formalization used the number of induced four-cycles. The historical conjecture instead uses this binary \(C_4\)-free indicator.

Provenance. Statement corrected by Dominic Dabish.

Quoted from FormalConjectures/WrittenOnTheWallII/160.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.GraphConjecture160.conjecture160

Solved: stated here; a Lean proof is at https://github.com/anagnorisis2peripeteia/formal-conjectures/blob/f0d70dfa13f92a4b631289e44487690833be8798/WOWII160AltProof.lean#L714.

WOWII Conjecture 160

For a simple connected graph \(G\), \(L_s(G) \ge \max_v l(v) + \max_v T(v) \cdot \chi_{C_4}(G)\) where:

  • \(L_s(G) = \mathrm{SimpleGraph.Ls}\, G\) is the maximum number of leaves over all spanning trees of \(G\),
  • \(\max_v l(v)\) is the maximum local independence number over vertices,
  • \(\max_v T(v)\) is the maximum number of triangles incident to any vertex,
  • \(\chi_{C_4}(G)\) is 1 if \(G\) has no cycle of length four and 0 otherwise.

A formal proof uses the \(C_4\)-free neighborhood identity \(d(v) = \lambda(v) + T(v)\) with a star/geodesic case analysis, routed through the connected-seed spanning-tree bound developed for Conjecture 2. An independent second proof, via a closest maximizer pair joined by a shortest path, is linked from the pull request that recorded the solution.

theorem conjecture160 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    let maxL := (Finset.univ.image (indepNeighborsCard G)).max' (by simp)
    let maxT := maxTrianglesAtVertex G
    let cC4 : ℕ := if ∃ v : α, ∃ c : G.Walk v v, c.IsCycle ∧ c.length = 4 then 0 else 1
    (maxL : ℝ) + (maxT : ℝ) * (cC4 : ℝ) ≤ Ls G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture160.conjecture160

TheoremWritten on the Wall II - Conjecture 1#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture1.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.GraphConjecture1.conjecture1

Solved: stated here; a Lean proof is at https://github.com/MiskinAleksandr23/WOWII-1/blob/eda16f6e96b313bd112351ae9859133b77d537c9/WOWII1/GraphConjecture1.lean.

WOWII Conjecture 1

For a simple connected graph G the maximum number of leaves of a spanning tree satisfies Ls(G) ≥ n(G) + 1 - 2·m(G) where n(G) counts vertices and m(G) is the size of a maximum matching.

A formal proof reduces to a spanning tree T. If I is the set of non-leaves of T, Hall's theorem applied to a bipartition of T gives a matching M with |I| + 1 ≤ 2 * |M|. Since |V| is the sum of the numbers of leaves and non-leaves, and every matching and leaf count constructed in T is admissible for the corresponding supremum in G, the stated inequality follows.

theorem conjecture1 {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
    (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn : G.Connected) :
    (Fintype.card α : ℝ) + 1 - 2 * matchingNumber G ≤ (Ls G : ℝ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture1.conjecture1

TheoremWritten on the Wall II - Conjecture 2#

References: - E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture2.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.GraphConjecture2.conjecture2

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/alphaproof-nexus-results/blob/0647711a71183c1ea492ad60860776617ce1ea88/APNOutputs/AICollaborator/Graphs/GraphConjecture2.lean#L704; a Lean proof is at https://github.com/kingcharlezz/formal-conjectures/blob/7d88e8b7946791ff53c322651f73de8d4df0ba53/FormalConjectures/WrittenOnTheWallII/Proofs/GraphConjecture2.lean#L622; a Lean proof is at https://github.com/KitaKen1/wowii-graph-conjecture-2-lean/blob/fc6cc1f5b857e9c3f9693b98587660eb09606abc/lean/GraphConjecture2.lean#L673.

WOWII Conjecture 2

For a simple connected graph \(G\), \(Ls(G) \ge 2 \cdot (l(G) - 1)\) where \(l(G)\) is the average independence number of the neighbourhoods of the vertices of \(G\).

A formal proof has been found with the methods described in arxiv/2605.22763, where an informal proof is also provided.

Another formal proof combines a spanning-tree leaf bound from connected domination with an ordered-pair double-counting argument for adjacent neighbourhoods.

A third formal proof starts from a triangle-free spanning subgraph of \(G\) with the maximum number of edges. Maximality bounds the neighbourhood independence number of each vertex by its degree in that subgraph; an edge whose endpoint degrees sum to at least \(2 \cdot l(G)\) then carries a double star, which is acyclic and extends to a spanning tree with at least \(2 \cdot (l(G) - 1)\) leaves.

theorem conjecture2 (G : SimpleGraph α) (h : G.Connected) :
  2 * (averageIndepNeighbors G - 1) ≤ Ls G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture2.conjecture2

TheoremWritten on the Wall II - Conjecture 3#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture3.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.GraphConjecture3.conjecture3

Solved: stated here without proof.

WOWII Conjecture 3

For a connected simple graph G, the number of leaves in a maximum spanning tree satisfies Ls(G) ≥ G.indepDominationNumber * MaxTemp(G), where G.indepDominationNumber is the independent domination number and MaxTemp(G) is max_v deg(v)/(n(G) - deg(v)).

theorem conjecture3 {G : SimpleGraph α} [DecidableRel G.Adj] [Nontrivial α] (h_conn : G.Connected) :
    G.indepDominationNumber * MaxTemp G ≤ Ls G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture3.conjecture3

TheoremWritten on the Wall II - Conjecture 4#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture4.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.GraphConjecture4.conjecture4

Solved: stated here without proof.

WOWII Conjecture 4

If G is a connected graph then the maximum number of leaves over all spanning trees satisfies Ls(G) ≥ NG(G) - 1 where NG(G) is the minimal neighbourhood size of a non-edge of G.

theorem conjecture4 (G : SimpleGraph α) [DecidableRel G.Adj] [Nontrivial α] (h_conn : G.Connected) :
    NG G - 1 ≤ Ls G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture4.conjecture4

TheoremWritten on the Wall II - Conjecture 5#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture5.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.GraphConjecture5.conjecture5

Solved: stated here without proof.

WOWII Conjecture 5

For a simple connected graph G, Ls(G) is bounded below by the maximal size of a sphere of radius radius(G) around the centres of G.

theorem conjecture5 (G : SimpleGraph V) (h_conn : G.Connected) :
    letI centers := { v : V | G.eccent v = G.radius }
    letI r_nat := G.radius.toNat
    letI sphere_verts (v : V) : Set V := { w | G.dist v w = r_nat }
    letI sphere_size (v : V) : ℝ := ↑(Finset.univ.filter (fun w => w ∈ sphere_verts v)).card
    letI max_sphere_size := sSup (sphere_size '' centers)
    max_sphere_size ≤ Ls G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture5.conjecture5

TheoremWritten on the Wall II - Conjecture 6#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture6.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.GraphConjecture6.conjecture6

Solved: stated here without proof.

WOWII Conjecture 6

For a connected graph G we have Ls(G) ≥ 1 + n(G) - m(G) - a(G) where a(G) is defined via independent sets.

theorem conjecture6 (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn : G.Connected) :
    1 + (Fintype.card α : ℝ) - matchingNumber G - α(G) ≤ Ls G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture6.conjecture6

TheoremWritten on the Wall II - Conjecture 7#

References: - E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc - [DFW03] E. DeLaVina, S. Fajtlowicz and B. Waller, On Some Conjectures of Griggs and Graffiti, 2002, revised 2003. - [Li26] Wentao Li, Lean proof of WOWII 7, 2026.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture7.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.GraphConjecture7.conjecture7

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

WOWII Conjecture 7

For a simple connected graph \(G\), \(L_s(G) \ge \max_v \lambda(v) - 1 + n - 2 \alpha(G)\), where \(L_s(G)\) is the maximum number of leaves over all spanning trees of \(G\), \(n = |V(G)|\), \(\alpha(G) = G.\mathrm{indepNum}\) is the independence number, and \(\lambda(v) = \mathrm{indepNeighborsCard}\, G\, v\) is the independence number of the neighbourhood of \(v\).

Proved by DeLaVina, Fajtlowicz, Waller (2002); see [DFW03].

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

theorem conjecture7 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    let maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
    ((maxL : ℤ) - 1 + (Fintype.card α : ℤ) - 2 * (G.indepNum : ℤ) : ℝ) ≤ Ls G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture7.conjecture7

TheoremWritten on the Wall II - Conjecture 13#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture13.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.GraphConjecture13.conjecture13

Solved: stated here without proof.

WOWII Conjecture 13

For a simple connected graph G, the size b(G) of a largest induced bipartite subgraph satisfies b(G) ≥ diam(G) + max_{v ∈ V} l(v) - 1, where diam(G) is the diameter of G and l(v) = indepNeighborsCard G v is the independence number of the neighbourhood of v.

theorem conjecture13 (G : SimpleGraph α) (h : G.Connected) :
    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
    (G.diam : ℝ) + (maxL : ℝ) - 1 ≤ b G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture13.conjecture13

TheoremWritten on the Wall II - Conjecture 16#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture16.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.GraphConjecture16.conjecture16

Solved: stated here without proof.

WOWII Conjecture 16

For a simple connected graph G, the size b(G) of a largest induced bipartite subgraph satisfies b(G) ≥ 2 * (rad(G) - 1) + max_{v ∈ V} l(v), where rad(G) is the radius of G (the minimum eccentricity) and l(v) = indepNeighborsCard G v is the independence number of the neighbourhood of v.

theorem conjecture16 (G : SimpleGraph α) (h : G.Connected) :
    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
    letI r := G.radius.toNat
    2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture16.conjecture16

TheoremWritten on the Wall II - Conjecture 17#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture17.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.GraphConjecture17.conjecture17

Solved: stated here without proof.

WOWII Conjecture 17

For a simple connected graph G, the size b(G) of a largest induced bipartite subgraph satisfies b(G) ≥ α(G) + ⌈diam(G) / 3⌉, where α(G) is the independence number of G and diam(G) is the diameter of G.

theorem conjecture17 (G : SimpleGraph α) (h : G.Connected) :
    (G.indepNum : ℝ) + ⌈(G.diam : ℝ) / 3⌉ ≤ b G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture17.conjecture17

TheoremWritten on the Wall II - Conjecture 18#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture18.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.GraphConjecture18.conjecture18

Solved: stated here without proof.

WOWII Conjecture 18

For a simple connected graph \(G\), the size \(b(G)\) of a largest induced bipartite subgraph satisfies \(b(G) \ge \alpha(G) + \lceil \sqrt{\mathrm{dist}_{\max}(M)} \rceil\), where \(\alpha(G)\) is the independence number, \(M\) is the set of maximum-degree vertices, and \(\mathrm{dist}_{\max}(M) = \max\{\mathrm{dist}_G(u,v) \mid u, v \in M\}\) is the maximum distance between two maximum-degree vertices (DeLaVina's dist_max(M)). Proven by Benny John (Feb. 2006), generalizing Schindl's proof of conjecture 17.

theorem conjecture18 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    let M : Set α := {v | G.degree v = G.maxDegree}
    (G.indepNum : ℝ) + ⌈Real.sqrt (distMaxSet G M : ℝ)⌉ ≤ b G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture18.conjecture18

TheoremWritten on the Wall II - Conjecture 19#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture19.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.GraphConjecture19.conjecture19

Open: stated without proof.

WOWII Conjecture 19

If G is connected then the size b(G) of a largest induced bipartite subgraph satisfies b(G) ≥ FLOOR((∑ ecc(v))/(|V|) + sSup (range (l G))), where ecc(v) denotes eccentricity and l(G) is the independence number of neighbourhoods.

theorem conjecture19 (G : SimpleGraph α) [Nontrivial α] (h_conn : G.Connected) :
    ⌊(∑ v ∈ Finset.univ, ((G.eccent v).toNat : ℝ)) / (Fintype.card α : ℝ) +
      sSup (Set.range (indepNeighbors G))⌋ ≤ b G

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

Sources
LeanWrittenOnTheWallII.GraphConjecture19.conjecture19

TheoremWritten on the Wall II - Conjecture 20#

References: - E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc - [AKS87] N. Alon, J. Kahn and P. D. Seymour, Large Induced Degenerate Subgraphs, Graphs and Combinatorics 3 (1987), 203–211. - [Li26] Wentao Li, Lean proof of WOWII 20, 2026.

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture20.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.GraphConjecture20.conjecture20

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

WOWII Conjecture 20

For a simple connected graph G, b(G) ≥ n(G) / ⌊deg_avg(G)⌋, where b(G) is the size of a largest induced bipartite subgraph, n(G) is the number of vertices, and deg_avg(G) = (∑ v, deg(v)) / n(G) is the average degree.

Follows from the weighted induced-subgraph bound of Alon, Kahn and Seymour [AKS87]. Lean formalization by Wentao Li, with AI assistance; see [Li26].

theorem conjecture20 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    let deg_avg : ℝ := (∑ v : α, (G.degree v : ℝ)) / (Fintype.card α : ℝ)
    (Fintype.card α : ℝ) / (⌊deg_avg⌋ : ℝ) ≤ (b G : ℝ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture20.conjecture20

TheoremWritten on the Wall II - Conjecture 23#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture23.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.GraphConjecture23.conjecture23

Solved: stated here without proof.

WOWII Conjecture 23

For a simple connected graph G, b(G) ≥ ⌊α(G) + dist_avg(M) / 2⌋, where b(G) is the size of a largest induced bipartite subgraph, α(G) is the independence number, M is the set of maximum-degree vertices, and dist_avg(M) is the average distance between distinct vertices of M.

This conjecture is false; there is a counterexample with b(G) = 19, α(G) = 15, and dist_avg(M) = 10.

theorem conjecture23 :
  ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
    (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected),
    let M : Set α := {v | G.degree v = G.maxDegree}
    ⌊(G.indepNum : ℝ) + distAvgSet G M / 2⌋ ≤ (b G : ℝ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture23.conjecture23

TheoremWritten 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

The WOWII page records this conjecture as disproved (status F).

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture24.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.GraphConjecture24.conjecture24

Solved: stated here without proof.

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

theorem conjecture24 :
    ¬ ∀ {α : 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

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

Sources
LeanWrittenOnTheWallII.GraphConjecture24.conjecture24

TheoremWritten 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

The WOWII page records this conjecture as disproved (status F), with the same counterexample as Conjecture 24.

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture25.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 1 test statement, counted here but not shown.

WrittenOnTheWallII.GraphConjecture25.conjecture25

Solved: stated here without proof.

WOWII Conjecture 25 (status F, disproved):

For every finite simple connected graph \(G\), \(b(G) ≥ 2⌈(1 + \min_v \operatorname{dist}_{\mathrm{even}}(v))/3⌉\), where \(b(G)\) is the size of a largest induced bipartite subgraph and \(\operatorname{dist}_{\mathrm{even}}(v)\) counts the vertices at even distance from \(v\).

The nontrivial vertex type excludes graphs with fewer than two vertices. The source gives the same counterexample as for Conjecture 24.

theorem conjecture25 :
    ¬ ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α],
      ∀ (G : SimpleGraph α) (_ : G.Connected),
        let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
        2 * ⌈(1 + (minDistEven : ℝ)) / 3⌉ ≤ (b G : ℝ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture25.conjecture25

TheoremWritten on the Wall II - Conjecture 31#

The WOWII page records this as Chung's theorem. This radius bound is proved in Section 2 of P. Erdős, M. Saks, and V. T. Sós, Maximum Induced Trees in Graphs, J. Combin. Theory Ser. B 41 (1986), 61–79; the authors credit Fan Chung for the proof. We state it here as a theorem; the formal proof is left as sorry pending a Lean port of the argument.

Here \(\mathrm{path}(G)\) is the maximum number of vertices in an induced path, and \(\mathrm{rad}(G)\) is the graph radius.

References: - E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc - P. Erdős, M. Saks, V. T. Sós, Maximum Induced Trees in Graphs

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture31.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.GraphConjecture31.conjecture31

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/wowii-graph-conjecture-31-lean/blob/a948e9fc07e11b786aee8dadb1376b4d938454d6/lean/GraphConjecture31.lean.

WOWII Conjecture 31 (Chung):

For every simple connected graph \(G\), \(\mathrm{path}(G) \ge 2 \cdot \mathrm{rad}(G) - 1\), where \(\mathrm{path}(G)\) is the maximum number of vertices in an induced path and \(\mathrm{rad}(G)\) is the graph radius.

theorem conjecture31 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    2 * (G.radius.toNat : ℤ) - 1 ≤ (path G : ℤ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture31.conjecture31

TheoremWritten on the Wall II - Conjecture 32#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture32.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.GraphConjecture32.conjecture32

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

WOWII Conjecture 32

For a simple connected graph \(G\), \(\operatorname{path}(G) \ge \operatorname{dist}\_{\operatorname{avg}}(A) + 0.5 \cdot \operatorname{ecc}\_{\operatorname{avg}}(M)\), where \(\operatorname{path}(G)\) is the number of vertices of a largest induced path of \(G\), \(A\) is the set of minimum-degree vertices, \(M\) is the set of maximum-degree vertices, \(\operatorname{dist}\_{\operatorname{avg}}(A)\) is the average of all nonzero distances \(\operatorname{dist}\_G(u, v)\) with \(u, v \in A\) (i.e. the average over ordered pairs of distinct vertices of \(A\); it is taken to be \(0\) when \(A\) has fewer than two vertices), and \(\operatorname{ecc}\_{\operatorname{avg}}(M)\) is the average eccentricity of the vertices in \(M\).

The conjecture is false, the authors present a counterexample: "The path on 5 vertices is a counterexample, path = 5, distavg(A) = 4 and the average of eccentricity of maximum degree vertices is 8/3."

Independent Lean formalization by Wentao Li, with AI assistance. An earlier Lean proof is recorded in the Epoch review archived in tadamcz/fc-review-results.

theorem conjecture32 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected),
      let A : Finset α := Finset.univ.filter (fun v => G.degree v = G.minDegree)
      let M : Finset α := Finset.univ.filter (fun v => G.degree v = G.maxDegree)
      let distavgA : ℝ := (∑ p ∈ A.offDiag, (G.dist p.1 p.2 : ℝ)) / (A.offDiag.card : ℝ)
      let eccavg (S : Finset α) : ℝ := (∑ v ∈ S, (G.eccent v).toNat) / (S.card : ℝ)
      distavgA + (1 / 2 : ℝ) * eccavg M ≤ (path G : ℝ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture32.conjecture32

TheoremWritten on the Wall II - Conjecture 33#

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

Quoted from FormalConjectures/WrittenOnTheWallII/GraphConjecture33.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.GraphConjecture33.conjecture33

Solved: stated here without proof.

WOWII Conjecture 33

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

The conjecture is false: the source records an October 2005 counterexample with \(\operatorname{path}(G) = 7\) and \(\operatorname{dist}\_{\operatorname{avg}}(M, V) = 3.56\).

theorem conjecture33 :
    ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected),
      let M : Set α := {v | G.degree v = G.maxDegree}
      let distAvg : ℝ :=
        open scoped Classical in
        let pairs := (M.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 (2 * distAvg) ≤ (path G : ℤ)

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

Sources
LeanWrittenOnTheWallII.GraphConjecture33.conjecture33

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.