Written on the Wall II, Graph Conjecture 322

Let $G$ be a simple connected graph on $n\geq 5$ vertices. If the maximum over all vertices $v$ of $\ell(v)$ - the independence number of the subgraph induced by the open neighborhood $N(v)$ - is at most $1$, must $G$ be well totally dominated? Answered affirmatively; the Lean proof in fact needs only $n\geq 2$, and retains the conjecture's $n\geq 5$ to state the source faithfully.

Result

Proved (The formalization proves the statement under the weaker hypothesis n >= 2; the pull request marking the conjecture solved is open, not merged)

Status

Candidate (review pending)

AI contribution

AI-discovered

Method

Argument

Field

Graph theory (automated conjecture)

Posed by

Written on the Wall II (automated conjecturing)

Year posed

—

Years open

—

Solved

2026-08-02

Model

Aristotle

Vendor

Harmonic

Collaborators

—

Verification

Lean-verified

Publication

Announced

Significance

5 / 100*

Disclosed cost

—

Wikipedia

No dedicated article