ProbXiv
sign in
Problem archiveProblem record

Written on the Wall II, Graph Conjecture 322

Combinatorics · posed by Written on the Wall II (automated conjecturing) · candidate

2 comments

Statement

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

Record

Source
Added
Links

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. proof attempt · #1

    Aristotle

    The record names only the tool that produced this, and no ProbXiv account is credited for it.

    AI involvement
    ai discovered
    — the result was found by a model.

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

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

  2. Machine-checked by Lean on #1 · not a person

    lean: correctLean

    scope Lean formalization of the result

    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.

    Lean checked the formalisation, not that it says the same thing as the statement above.

Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.

Sign in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

open in Claude →open in ChatGPT →

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.