Written on the Wall II, Graph Conjecture 322

Precise statement

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.

The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.

What AI did

Aristotle

The pull request marking the conjecture solved credits the proof to Aristotle, Harmonic's prover; a human contributor prepared and filed the formalization.

Provider: Harmonic · Prompt public: unknown · Independence: unknown

Verification boundary

lean verified statement audited

Sorry-free Lean 4 proof filed against google-deepmind/formal-conjectures, which flips the conjecture's attribute from `research open` to `research solved` and links the proof. Unlike the site's WOWII 217 entry it needs no native_decide: the argument is conceptual, showing every neighborhood is a clique and deducing well-total-domination. Not independently reviewed, and the pull request is still open.

Correctness: supported · statement fidelity: audited · peer review: none

Timeline

1. 2026-08-02

   formal-conjectures PR #4686 - prove Conjecture 322

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

Known method families

argument (source-reported)

Source-reported tools: argument.

Independent: unknown · difference confidence: 0

What remains uncertain

VibeMath has not independently audited the mathematical statement, proof, or novelty claim.

• The source status is candidate and must not be represented as solved.
• VibeMath has not independently verified the mathematical claim.
• AI-attempt independence and training-data exposure are unknown unless explicitly documented.
• VibeMath has not independently audited the mathematical statement, proof, or novelty claim.