GraphConjecture2.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

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.

Imports (1)

theorem WrittenOnTheWallII.GraphConjecture2.conjecture2 sorry line 64 source
depends on sorry what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Connected, LE.le, Real, HMul.hMul, OfNat.ofNat, Nat, HSub.hSub, SimpleGraph.averageIndepNeighbors, SimpleGraph.Ls, Classical.propDecidable, SimpleGraph.Adj
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.