/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilWritten 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.
namespace WrittenOnTheWallII.GraphConjecture2open SimpleGraphvariable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]open scoped Classical inWOWII 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.
@[category research solved, AMS 5,
formal_proof using lean4 at
"https://github.com/google-deepmind/alphaproof-nexus-results/blob/0647711a71183c1ea492ad60860776617ce1ea88/APNOutputs/AICollaborator/Graphs/GraphConjecture2.lean#L704",
formal_proof using formal_conjectures at
"https://github.com/kingcharlezz/formal-conjectures/blob/7d88e8b7946791ff53c322651f73de8d4df0ba53/FormalConjectures/WrittenOnTheWallII/Proofs/GraphConjecture2.lean#L622",
formal_proof using lean4 at
"https://github.com/KitaKen1/wowii-graph-conjecture-2-lean/blob/fc6cc1f5b857e9c3f9693b98587660eb09606abc/lean/GraphConjecture2.lean#L673"]
theorem conjecture2 (G : SimpleGraph α) (h : G.Connected) :
2 * (averageIndepNeighbors G - 1) ≤ Ls G := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial αG:SimpleGraph αh:G.Connected⊢ 2 * (G.averageIndepNeighbors - 1) ≤ G.Ls All goals completed! 🐙end WrittenOnTheWallII.GraphConjecture2