Add 16 WOWII open conjectures (batch 1)#3795
Merged
mo271 merged 3 commits intogoogle-deepmind:mainfrom Apr 20, 2026
Merged
Conversation
…h 1) Adds 16 open WOWII conjectures following the existing pattern in FormalConjectures/WrittenOnTheWallII/. Each file includes 1-2 fully-proved sanity-check examples testing the invariants used. ## Conjectures added ### Spanning tree leaves Ls (1) - Conjecture 3: Ls(G) ≥ γ_i(G) · max temp(v) ### Largest induced bipartite subgraph b(G) (5) - Conjecture 13: b(G) ≥ diam(G) + max l(v) - 1 - Conjecture 16: b(G) ≥ 2(rad(G)-1) + max l(v) - Conjecture 17: b(G) ≥ α(G) + ⌈diam(G)/3⌉ - Conjecture 20: b(G) ≥ n / ⌊deg_avg⌋ - Conjecture 22: b(G) ≥ ⌊α(G) + distavg(M)⌋ ### Longest induced path (2) - Conjecture 32: path(G) ≥ ⌈2·distavg(M,V)⌉ - Conjecture 33: path(G) ≥ ⌈distavg(C,V) + distavg(M,V)⌉ ### Induced tree (2) - Conjecture 141: tree(G) ≥ (girth-2)/2 + max l(v) - Conjecture 200: tree(G) = ⌈1 + λ_avg⌉ implies Hamiltonian path ### Hamiltonian path sufficient conditions (2) - Conjecture 194: α(G) ≤ 1 + λ_avg implies Hamiltonian path - Conjecture 198a: b(G) ≤ 2 + ecc_avg implies Hamiltonian path ### Well totally dominated (4) - Conjecture 315: α(G) = |pendants| implies well totally dominated - Conjecture 316: |pendants| ≥ deg_avg implies well totally dominated - Conjecture 322: n ≥ 5, max l(v) ≤ 1 implies well totally dominated - Conjecture 327: 3γ(G) = γ_i(G) implies well totally dominated ## New definitions added locally - largestInducedTreeSize (used in 141, 200) - averageEccentricity (used in 198a) - pendantVertices (used in 315, 316) - IsTotalDominatingSet, IsMinimalTotalDominatingSet, isWellTotallyDominated (shared across 315/316/322/327) Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc http://cms.dt.uh.edu/faculty/delavinae/research/wowII/ Assisted by Claude (Anthropic).
henrykmichalewski
added a commit
to henrykmichalewski/formal-conjectures
that referenced
this pull request
Apr 18, 2026
This branch accumulates all WOWII batches beyond batch 1 (google-deepmind#3795) and batch 2 (google-deepmind#3796). Total new files: 48, covering ~50 new invariants. Batches: - 3 (5 files): residue, distMin/Max — 18, 59, 61, 65, 109 - 4 (9 files): path/tree hard cases, C₄ — 31, 36, 100, 103, 133, 142, 143, 144, 314 - 5 (5 files): alphaCore, graphSquare, triangles — 101, 145, 146, 160, 291 - 6 (5 files): matching, circumference, oddGirth, etc. - 7 (8 files): length, toughness, distOdd, edgeConnectivity, mode, power, freqMaxL, residue2 - 8 (8 files): arboricity, degeneracy, metricDimension, geodeticNumber, modeMax, medianDegree, evenModeMin, girthComplement - 9 (8 files): achromaticNumber, bandwidth, boxicity, crossingNumber, isoperimetric, rainbowConnection, romanDomination, thickness Many have proved theorems (particularly classical results stated with sorry). Each file includes sanity-check tests. This is a staging branch for easier review / cherry-picking into smaller PRs. Assisted by Claude (Anthropic).
mo271
reviewed
Apr 20, 2026
Collaborator
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Thanks a lot, looks great in general. A few comments. I assume the status of these (if open or resolved) is in sync with the written-on-the-wall website?!
Comment on lines
+34
to
+68
| /- | ||
| ## Definitions for well totally dominated graphs | ||
|
|
||
| A *total dominating set* of `G` is a set `S` of vertices such that every vertex of `G` | ||
| (including vertices in `S`) has a neighbor in `S`. A total dominating set `S` is | ||
| *minimal* if no proper subset of `S` is also a total dominating set. | ||
|
|
||
| A graph `G` is *well totally dominated* if every minimal total dominating set | ||
| has the same cardinality; equivalently, the total domination number equals the | ||
| maximum cardinality of a minimal total dominating set. | ||
|
|
||
| The *pendant vertices* (also called *leaves*) of `G` are the vertices of degree 1. | ||
| -/ | ||
|
|
||
| /-- A set `S` is a total dominating set of `G` if every vertex has a neighbor in `S`. -/ | ||
| def IsTotalDominatingSet (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : Prop := | ||
| ∀ v : α, ∃ w ∈ S, G.Adj v w | ||
|
|
||
| /-- A total dominating set `S` is minimal if no proper subset of `S` is also a | ||
| total dominating set. -/ | ||
| def IsMinimalTotalDominatingSet (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : Prop := | ||
| IsTotalDominatingSet G S ∧ | ||
| ∀ T : Finset α, T ⊂ S → ¬IsTotalDominatingSet G T | ||
|
|
||
| /-- A graph `G` is well totally dominated if every minimal total dominating set | ||
| has the same cardinality. -/ | ||
| def isWellTotallyDominated (G : SimpleGraph α) [DecidableRel G.Adj] : Prop := | ||
| ∀ S T : Finset α, | ||
| IsMinimalTotalDominatingSet G S → | ||
| IsMinimalTotalDominatingSet G T → | ||
| S.card = T.card | ||
|
|
||
| /-- The set of pendant vertices (leaves) of `G`: vertices of degree 1. -/ | ||
| noncomputable def pendantVertices (G : SimpleGraph α) [DecidableRel G.Adj] : Finset α := | ||
| Finset.univ.filter (fun v => G.degree v = 1) |
Collaborator
There was a problem hiding this comment.
This should go into our FormalConjecturesForMathlib. And then you don't need to import 315 in any of the other files!
Comment on lines
+32
to
+35
| /-- `largestInducedTreeSize G` is the number of vertices in a largest induced subtree of `G`. | ||
| A tree is a connected acyclic graph; an induced tree is an induced subgraph that is a tree. -/ | ||
| noncomputable def largestInducedTreeSize (G : SimpleGraph α) : ℕ := | ||
| sSup { n | ∃ s : Finset α, s.card = n ∧ (G.induce (s : Set α)).IsTree } |
Collaborator
There was a problem hiding this comment.
is duplicated between files 141 and 200 ==> move to FormalConjecturesForMathlib
Comment on lines
+32
to
+35
| /-- `largestInducedTreeSize G` is the number of vertices in a largest induced subtree of `G`. | ||
| A tree is a connected acyclic graph; an induced tree is an induced subgraph that is a tree. -/ | ||
| noncomputable def largestInducedTreeSize (G : SimpleGraph α) : ℕ := | ||
| sSup { n | ∃ s : Finset α, s.card = n ∧ (G.induce (s : Set α)).IsTree } |
Collaborator
There was a problem hiding this comment.
is duplicated between files 141 and 200 ==> move to FormalConjecturesForMathlib
| -/ | ||
|
|
||
| import FormalConjectures.Util.ProblemImports | ||
| import FormalConjectures.WrittenOnTheWallII.GraphConjecture315 |
Collaborator
There was a problem hiding this comment.
Suggested change
| import FormalConjectures.WrittenOnTheWallII.GraphConjecture315 |
| -/ | ||
|
|
||
| import FormalConjectures.Util.ProblemImports | ||
| import FormalConjectures.WrittenOnTheWallII.GraphConjecture315 |
Collaborator
There was a problem hiding this comment.
Suggested change
| import FormalConjectures.WrittenOnTheWallII.GraphConjecture315 |
Comment on lines
+32
to
+35
| /-- The average eccentricity of a graph `G`: the mean of `eccentricity G v` over all vertices, | ||
| converted to a real number. Returns 0 if the graph has no vertices. -/ | ||
| noncomputable def averageEccentricity (G : SimpleGraph α) : ℝ := | ||
| (∑ v : α, (G.eccentricity v).toNat) / (Fintype.card α : ℝ) |
Collaborator
There was a problem hiding this comment.
averageEccentricity should go to Invariants.lean.
|
|
||
| /-- A graph `G` is well totally dominated if every minimal total dominating set | ||
| has the same cardinality. -/ | ||
| def isWellTotallyDominated (G : SimpleGraph α) [DecidableRel G.Adj] : Prop := |
Collaborator
There was a problem hiding this comment.
Suggested change
| def isWellTotallyDominated (G : SimpleGraph α) [DecidableRel G.Adj] : Prop := | |
| def IsWellTotallyDominated (G : SimpleGraph α) [DecidableRel G.Adj] : Prop := |
| @[category research open, AMS 5] | ||
| theorem conjecture315 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected) | ||
| (h : G.indepNum = (pendantVertices G).card) : | ||
| isWellTotallyDominated G := by |
Collaborator
There was a problem hiding this comment.
Suggested change
| isWellTotallyDominated G := by | |
| IsWellTotallyDominated G := by |
| @[category research open, AMS 5] | ||
| theorem conjecture316 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected) | ||
| (h : (averageDegree G : ℚ) ≤ (pendantVertices G).card) : | ||
| isWellTotallyDominated G := by |
Collaborator
There was a problem hiding this comment.
Suggested change
| isWellTotallyDominated G := by | |
| IsWellTotallyDominated G := by |
| theorem conjecture322 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected) | ||
| (hn : 5 ≤ Fintype.card α) | ||
| (h : ∀ v : α, indepNeighborsCard G v ≤ 1) : | ||
| isWellTotallyDominated G := by |
Collaborator
There was a problem hiding this comment.
Suggested change
| isWellTotallyDominated G := by | |
| IsWellTotallyDominated G := by |
…thlib Per mo271 review on google-deepmind#3795: 1. Move shared def out of WOWII files: - IsTotalDominatingSet, IsMinimalTotalDominatingSet, IsWellTotallyDominated, pendantVertices → FormalConjecturesForMathlib/.../WellTotallyDominated.lean - largestInducedTreeSize (dup in 141/200) → .../LargestInducedTree.lean - averageEccentricity → existing Invariants.lean 2. Rename isWellTotallyDominated → IsWellTotallyDominated (CamelCase per Mathlib). 3. GraphConjecture22: change category to research solved (listed resolved on website), ensure floor is used per WOWII statement. 4. Minor: remove empty lines and unused Classical opens in 316, 327. Assisted by Claude (Anthropic).
mo271
requested changes
Apr 20, 2026
Collaborator
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Can you check again for each problem the status of the problems?
I checked for"13" and it seems that it is also should be labeled research solved?
Which of these are actually open?
…bsite Per mo271's review on google-deepmind#3795: audited status of all 16 WOWII conjectures in batch 1 against the current DeLaVina WOWII website. Corrections: - google-deepmind#13: research open -> research solved (WOWII: T) - google-deepmind#16: research open -> research solved (WOWII: T) - google-deepmind#17: research open -> research solved (WOWII: T) - google-deepmind#20: research open -> research solved (WOWII: T*) - google-deepmind#32: research open -> research solved (WOWII: F, disproved) - google-deepmind#33: research open -> research solved (WOWII: F, disproved) Unchanged (already correct): - google-deepmind#3: research solved (WOWII: T) - google-deepmind#22: research solved (WOWII: F, disproved) - google-deepmind#141, google-deepmind#194, #198a, google-deepmind#200, google-deepmind#315, google-deepmind#316, google-deepmind#322, google-deepmind#327: research open (WOWII: O) Build passes. Assisted by Claude (Anthropic).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds 16 open conjectures from the WOWII (Written on the Wall II) database by E. DeLaViña, following the existing pattern in FormalConjectures/WrittenOnTheWallII/.
Reference: http://cms.dt.uh.edu/faculty/delavinae/research/wowII/
Scope
@[category research open, AMS 5])New definitions
largestInducedTreeSize(local, used in 141 and 200)averageEccentricity(local, used in 198a)pendantVertices(shared across 315, 316)IsTotalDominatingSet,IsMinimalTotalDominatingSet,isWellTotallyDominated(shared across 315/316/322/327, defined in 315 and imported)Batch strategy
This is batch 1 of ~4 batches covering 40 open WOWII conjectures. This batch targets the easiest formalizations (existing or trivial-to-add invariants). Subsequent batches will add residue, distmin/distmax, σ (2-domination), etc.
Checks
Assisted by Claude (Anthropic).