Add 10 WOWII open conjectures (batch 2) by henrykmichalewski · Pull Request #3796 · google-deepmind/formal-conjectures

henrykmichalewski · 2026-04-17T12:37:55Z

Adds 10 open conjectures from WOWII (Written on the Wall II) by E. DeLaViña.
Follow-up to #3795 (batch 1, 16 conjectures).

Reference: http://cms.dt.uh.edu/faculty/delavinae/research/wowII/

Conjectures

distEven-based (3): Conj 23, 24, 63 — lower bounds on b(G), f(G) via min distEven
tree(G)-based (3): Conj 72, 84, 85 — tree(G) lower bounds
Upper bounds (2): Conj 91 on b(G), Conj 96 on α(G)
Hamiltonian sufficient (2): Conj 189 (uses σ = 2-dom), Conj 199 (uses κ = connectivity)

New definitions (local to each file, self-contained)

distEven G v — count of vertices at even distance from v
largestInducedTreeSize — reused from batch 1
twoDominationNumber — σ(G), 2-domination number
vertexConnectivity — κ(G), for Conj 199

Each file is self-contained (definitions copied as needed) to keep PRs atomic.

Tests

All 10 files include 1-2 fully-proved @[category test] examples.

Build

Passes cleanly.

Assisted by Claude (Anthropic).

Medium-difficulty conjectures using distEven(v), tree(G), and related invariants. ## Conjectures - 23, 24, 63: involve distEven (min vertices at even distance) - 72, 84, 85: involve tree(G) (largest induced tree) - 91, 96: upper bounds on b(G) / α(G) - 189: Hamiltonian via max distEven + σ(G) (2-domination) - 199: Hamiltonian via tree(G) and vertex connectivity κ(G) ## New definitions (local, self-contained) - distEven G v - largestInducedTreeSize (reused from batch 1) - twoDominationNumber (new, for σ(G)) - vertexConnectivity (new, for κ(G)) ## Tests Each file has 1-2 fully-proved @[category test] examples. Reference: E. DeLaVina, Written on the Wall II http://cms.dt.uh.edu/faculty/delavinae/research/wowII/ Assisted by Claude (Anthropic).

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).

Status audit for batch 2 per mo271's feedback. Corrected conjectures where the Lean category didn't match the current WOWII status: - Conjecture 23: research open -> research solved (WOWII status F, disproved by counterexample July 2005) - Conjecture 24: research open -> research solved (WOWII status F, disproved May 2004 by DeLaVina) Other 8 conjectures (63, 72, 84, 85, 91, 96, 189, 199) remain research open, matching WOWII status O.

Mirrors the Round C docstring pass from the private repo's phase1-infrastructure branch. Each Lean file now carries the canonical source statement and upstream URL inline so reviewers can verify formalization against the source without navigating away from the diff.

GraphConjecture199.lean was intentionally excluded from this PR to avoid conflict with open PR google-deepmind#3796. GraphCircumference.lean still imported and opened the `WrittenOnTheWallII.GraphConjecture199` namespace (to reuse `vertexConnectivity`), which broke the build (`no such file or directory`). Dropped the `import FormalConjectures.WrittenOnTheWallII.GraphConjecture199` and the corresponding `open` clause, and inlined the `vertexConnectivity` definition directly into GraphCircumference.lean so the file is self-contained.

mo271 · 2026-05-03T13:24:43Z

can you double check that the numbering is correct here (see #3824)

henrykmichalewski · 2026-05-04T00:35:55Z

Thanks for flagging — re-audited all 10 files in this PR against the WOWII source. You were right to ask: two files in this PR exhibit the same off-by-one numbering shift you fixed in #3823 / #3824.

Pushed 6c5df66 addressing the off-by-one cascade:

The previous GraphConjecture23.lean actually stated WOWII More style linters #24 verbatim (b(G) ≥ max-l(v) + ⌈min dist_even(v)/3⌉). Renamed to GraphConjecture24.lean, namespace and docstring updated, wrapped with answer(False) ↔ ... since More style linters #24 is status F.
The previous GraphConjecture24.lean actually stated WOWII chore: Fix typo in README #25 verbatim (b(G) ≥ 2⌈(1+min dist_even(v))/3⌉). Renamed to GraphConjecture25.lean, same disproof pattern (chore: Fix typo in README #25 is also status F; WOWII notes "same counterexample as More style linters #24").
The correct WOWII Get problem stats for subdirectories #23 is already in tree on main from your fix(WOWII): Fix conjecture 22 #3823, so we don't add a GraphConjecture23.lean here.

Full audit also surfaced one independent (non-numbering) issue I want to disclose for transparency, not addressed in this commit since it's outside the scope of your numbering question:

GraphConjecture84.lean — WOWII Formalize Collatz conjecture statement #84 reads tree(G) ≥ 2 rad(G) / δ(G) where δ(G) is the minimum degree. The Lean uses averageDistance G as the denominator (interpreting δ as d). Happy to push a follow-up commit fixing this if you'd like it bundled in this PR; otherwise we'll file it separately.

GraphConjecture189.lean is on the borderline — it carries a TODO hedge about whether σ(G) should be the 2-domination number. The standard Fink–Jacobson reading is correct and consistent across WOWII #188/#190/#201, so the TODO is overcautious; we'll remove it in the same follow-up.

…43, 145, 217) Five remaining audit findings against the WOWII source page (re google-deepmind#3796/google-deepmind#3820 audit comments). Each fix is independent of mo271's numbering-shift pattern. GraphConjecture36.lean — status F (disproved by Waller, Oct 2003). Wrapped the existing inequality in `theorem ... : answer(False) ↔ ∀ G ..., ...` to mirror mo271's google-deepmind#3823 disproof pattern. The body itself already matched the WOWII statement `path(G) ≥ 2 rad(G) / dp(G)` verbatim. GraphConjecture100.lean — the WOWII HTML uses `length(Ḡ)` (overline / graph complement); our extracted JSON dropped the overline, and the file correspondingly used `length(G)`. Updated the verbatim quote and the formal statement to use the diameter of `Gᶜ`. Documented the `length := diam` choice. GraphConjecture143.lean — added Fink–Jacobson 1985 reference for the σ(G) = 2-domination interpretation, matching the convention used in 188, 189, 190, and 201. GraphConjecture145.lean — same overline-dropped bug as 100: the WOWII HTML says `λ_min(Ḡ)` but our extracted JSON had `λ_min(G)`. The Lean theorem already used `Gᶜ` correctly; only the docstring header was inconsistent. Updated the verbatim quote. GraphConjecture217.lean — replaced the `Classical.choice ⟨∅⟩` / `Classical.choice ⟨0⟩` placeholders for `residue2Core` and `residue2ComponentCount` with proper definitions: the residue-2 core is the union (Finset.sup) of all 2-core subsets — equivalent to the iterative- peeling fixpoint without the well-founded-recursion overhead — and the component count is `Nat.card` of the connected components of the induced subgraph. All five files build: lake build FormalConjectures.WrittenOnTheWallII.GraphConjecture{36,100,143,145,217} Audit also looked at GraphConjecture7 (claimed mismatch in the audit) and re-verified it against the WOWII source: the formal statement `(maxL - 1 + n - 2α : ℝ) ≤ Ls G` matches WOWII Conjecture 7 verbatim (`Ls(G) ≥ max λ(v) - 1 + n - 2α(G)`). No change needed. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

henrykmichalewski · 2026-05-04T11:55:10Z

Follow-up: pushed 142c74c bundling the two non-numbering audit findings I disclosed earlier:

GraphConjecture84.lean — replaced the denominator averageDistance G with G.minDegree to match the WOWII statement tree(G) ≥ 2 rad(G) / δ(G) (lowercase δ in the WOWII HTML, not d). Dropped the 0 < averageDistance G hypothesis and added 0 < G.minDegree.
GraphConjecture189.lean — removed the σ-interpretation TODO hedge and added a Fink–Jacobson 1985 reference. WOWII uses σ(G) for the 2-domination number consistently across Conjectures 188/189/190/201.

Both files build cleanly. PR is now in 8/10 sorry shape with 0 open audit issues.

…ind#3823, google-deepmind#3824) The previous "GraphConjecture23.lean" and "GraphConjecture24.lean" added in this PR exhibited the same off-by-one numbering shift that mo271 fixed in upstream PRs google-deepmind#3823 (Conjecture 22) and google-deepmind#3824 (Conjectures 32-34): each file declared a number in its filename and module-docstring header that did not match the formal statement in its theorem body. - Old GraphConjecture23.lean stated WOWII Conjecture 24 verbatim (b(G) >= max-l(v) + ceil[min dist_even(v) / 3]). - Old GraphConjecture24.lean stated WOWII Conjecture 25 verbatim (b(G) >= 2 * ceil[(1 + min dist_even(v)) / 3]). The correct WOWII Conjecture 23 is already in tree on main as a result of mo271's google-deepmind#3823 (using the answer(False) pattern, since Conjecture 23 is status F / disproved). This commit: - Renames GraphConjecture23.lean -> GraphConjecture24.lean and updates the namespace, theorem name, docstring, and verbatim quote accordingly. - Renames GraphConjecture24.lean -> GraphConjecture25.lean and likewise. - Wraps both theorems in the disproved pattern (theorem ... : answer(False) ↔ ∀ G ..., <inequality> := by sorry), since WOWII google-deepmind#24 and google-deepmind#25 are both status F (per the WOWII page; google-deepmind#25 notes "same counterexample as in google-deepmind#24"). Both files build: lake build FormalConjectures.WrittenOnTheWallII.GraphConjecture24 lake build FormalConjectures.WrittenOnTheWallII.GraphConjecture25

…tring GraphConjecture84.lean previously used `averageDistance G` as the denominator in `tree(G) ≥ 2 rad(G) / d(G)`, interpreting the lowercase `δ` in the WOWII HTML (rendered as `<font face="Symbol">d</font>`) as Latin `d`. The intended invariant is the **minimum degree** `G.minDegree`. Replaced the denominator accordingly, dropped the now-irrelevant `0 < averageDistance G` hypothesis, and added `0 < G.minDegree` as the well-definedness guard. GraphConjecture189.lean carried a `TODO` flagging uncertainty about whether σ(G) is the 2-domination number. WOWII uses σ(G) for the Fink–Jacobson 1985 2-domination number consistently across Conjectures 188, 189, 190, and 201 (all Hamiltonian-path implications). Removed the hedge and added the citation in the docstring. Both files build: lake build FormalConjectures.WrittenOnTheWallII.GraphConjecture84 lake build FormalConjectures.WrittenOnTheWallII.GraphConjecture189

…43, 145, 217) Five remaining audit findings against the WOWII source page (re google-deepmind#3796/google-deepmind#3820 audit comments). Each fix is independent of mo271's numbering-shift pattern. GraphConjecture36.lean — status F (disproved by Waller, Oct 2003). Wrapped the existing inequality in `theorem ... : answer(False) ↔ ∀ G ..., ...` to mirror mo271's google-deepmind#3823 disproof pattern. The body itself already matched the WOWII statement `path(G) ≥ 2 rad(G) / dp(G)` verbatim. GraphConjecture100.lean — the WOWII HTML uses `length(Ḡ)` (overline / graph complement); our extracted JSON dropped the overline, and the file correspondingly used `length(G)`. Updated the verbatim quote and the formal statement to use the diameter of `Gᶜ`. Documented the `length := diam` choice. GraphConjecture143.lean — added Fink–Jacobson 1985 reference for the σ(G) = 2-domination interpretation, matching the convention used in 188, 189, 190, and 201. GraphConjecture145.lean — same overline-dropped bug as 100: the WOWII HTML says `λ_min(Ḡ)` but our extracted JSON had `λ_min(G)`. The Lean theorem already used `Gᶜ` correctly; only the docstring header was inconsistent. Updated the verbatim quote. GraphConjecture217.lean — replaced the `Classical.choice ⟨∅⟩` / `Classical.choice ⟨0⟩` placeholders for `residue2Core` and `residue2ComponentCount` with proper definitions: the residue-2 core is the union (Finset.sup) of all 2-core subsets — equivalent to the iterative- peeling fixpoint without the well-founded-recursion overhead — and the component count is `Nat.card` of the connected components of the induced subgraph. All five files build: lake build FormalConjectures.WrittenOnTheWallII.GraphConjecture{36,100,143,145,217} Audit also looked at GraphConjecture7 (claimed mismatch in the audit) and re-verified it against the WOWII source: the formal statement `(maxL - 1 + n - 2α : ℝ) ≤ Ls G` matches WOWII Conjecture 7 verbatim (`Ls(G) ≥ max λ(v) - 1 + n - 2α(G)`). No change needed.

Paul-Lez · 2026-05-07T15:34:17Z

+vertices at even distance from `v`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture24 : answer(False) ↔


Could you move the graph-type quantification under the ∀ after answer(False) here? Our convention for a solved negative yes/no problem is a single global statement, e.g. answer(False) ↔ ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α], ∀ (G : SimpleGraph α), ..., rather than fixing α as an outer theorem variable.

Paul-Lez · 2026-05-07T15:34:26Z

+`dist_even(v)` is the number of vertices at even distance from `v`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture25 : answer(False) ↔


Same answer(False) shape issue here: the source is a global false answer over all finite connected graphs, so the α/instance quantification should live after answer(False) rather than as outer variables of the theorem.

…j 24/25 Per Paul-Lez review on PR google-deepmind#3796: our convention for a solved negative yes/no problem is a single global statement, answer(False) ↔ ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α], ∀ (G : SimpleGraph α), ... rather than fixing α as an outer theorem variable. The previous shape made the theorem a type-by-type statement, while WOWII google-deepmind#24 and google-deepmind#25 are global false answers over all finite connected graphs. Moved the α and instance binders inside the answer(False) ↔ ... body. distEven is updated to no longer use the section variables (it was only using [Fintype α], which is now an explicit instance argument). Builds cleanly: lake build FormalConjectures.WrittenOnTheWallII.GraphConjecture{24,25}

Per Paul-Lez review on PR google-deepmind#3820: - GraphConjecture36.lean — moved α/instance quantification inside the `answer(False) ↔ ...` body (same convention as conj 24/25 in PR google-deepmind#3796). - GraphConjecture217.lean — substantive correction. The previous version used the wrong invariants: * `L(G)` was interpreted as the *minimum* leaves of a spanning tree (`leafNumber G = sInf {...}`); the WOWII definitions popup specifies `L(G)` as the **maximum** leaves, i.e. the upstream `Ls G`. * `c_{residue=2}(G)` was interpreted as a connected-component count of a 2-core; per the WOWII definitions popup, it is the **characteristic function** for the predicate `residue G = 2`, i.e. `1` when `residue G = 2` and `0` otherwise. Replaced both: the conjecture now reads Ls G ≤ 4 · χ_{residue=2}(G) + 2 → G has a Hamiltonian path using `Ls` from FormalConjecturesForMathlib and a new local `residueEqTwoIndicator G : ℕ`. Removed the now-unused `Is2Core`, `residue2Core`, `residue2ComponentCount`, `numLeaves`, and `leafNumber` definitions. - GraphConjecture314.lean — substantive correction. The previous version used `pathCoverNumber G ≤ 4`, but in WOWII notation `path(G)` is the size of a largest induced path; `p(G)` is the path cover number. Switched the hypothesis to `path G ≤ 4` (using upstream `path` from FormalConjecturesForMathlib) and added the `[Nontrivial α]` constraint matching the source's `n > 1` requirement. All three files build cleanly: lake build FormalConjectures.WrittenOnTheWallII.GraphConjecture{36,217,314}

henrykmichalewski · 2026-05-08T00:47:55Z

@Paul-Lez — applied your answer(False) quantification convention in 0418c4d. Both GraphConjecture24.lean and GraphConjecture25.lean now read

@[category research solved, AMS 5]
theorem conjecture24 : answer(False) ↔
    ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α],
      ∀ (G : SimpleGraph α) (_ : G.Connected),
        ...

with the α and instance binders moved inside the ↔ ∀ block so it's a single global statement rather than a type-by-type one. distEven lost its dependence on the section variables (now takes [Fintype α] as an explicit argument). Builds cleanly.

henrykmichalewski mentioned this pull request Apr 20, 2026

WOWII/GraphConjecture34: statement uses maxEccentricityVertices (B) instead of max-degree vertices (M) #3808

Open

This was referenced Apr 22, 2026

Add 22 WOWII numbered conjectures (batches 3-9, part 1/2) #3820

Open

Add 27 WOWII named graph-invariant files (batches 3-9, part 2/2) #3821

Open

henrykmichalewski added 2 commits May 5, 2026 10:43

henrykmichalewski force-pushed the wowii-batch-2 branch from 142c74c to 80c04c5 Compare May 5, 2026 09:43

Paul-Lez reviewed May 7, 2026

View reviewed changes

Paul-Lez added the awaiting-author The author should answer a question or perform changes. Reply when done. label May 7, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add 10 WOWII open conjectures (batch 2)#3796

Add 10 WOWII open conjectures (batch 2)#3796
henrykmichalewski wants to merge 6 commits intogoogle-deepmind:mainfrom
henrykmichalewski:wowii-batch-2

henrykmichalewski commented Apr 17, 2026

Uh oh!

mo271 commented May 3, 2026

Uh oh!

henrykmichalewski commented May 4, 2026

Uh oh!

henrykmichalewski commented May 4, 2026

Uh oh!

Paul-Lez May 7, 2026

Uh oh!

Paul-Lez May 7, 2026

Uh oh!

henrykmichalewski commented May 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

henrykmichalewski commented Apr 17, 2026

Conjectures

New definitions (local to each file, self-contained)

Tests

Build

Uh oh!

mo271 commented May 3, 2026

Uh oh!

henrykmichalewski commented May 4, 2026

Uh oh!

henrykmichalewski commented May 4, 2026

Uh oh!

Paul-Lez May 7, 2026

Choose a reason for hiding this comment

Uh oh!

Paul-Lez May 7, 2026

Choose a reason for hiding this comment

Uh oh!

henrykmichalewski commented May 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants