VibeMathedMath problems solved with AI
Sign in

Dean's conjecture for k=5k=5

Every finite simple graph GG with minimum degree δ(G)≥5\delta(G)\ge 5 contains a simple cycle CC whose length satisfies ∣C∣≡0(mod5)|C|\equiv 0\pmod 5.

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Graph Theory
Posed by
Nathaniel Dean
Year posed
1988
Years open
38y
Solved
2026-08-29
Model
GPT-5.6 Sol (primary); Claude Opus 5; GLM 5.3 Flash
Vendor
OpenAI (primary); Anthropic; Z.ai
Collaborators
—
Verification
Site-confirmed
Publication
Preprint
Significance
32 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Claims the last open case of Dean's conjecture: every finite simple graph with minimum degree at least five contains a cycle of length divisible by five. Verified independently against Luo, Ma and Zhao (arXiv:2601.13552), whose abstract confirms the landscape - the conjecture was known for k∈{3,4}k\in\{3,4\} and they proved every k≥6k\ge6, leaving k=5k=5 open. If this proof stands, Dean's conjecture holds for all k≥3k\ge3.

Nine finite proposition families in the bipartite and triangle-free branches are computer-assisted, with verifiers and certificates in a separately archived supplement. The reductions from arbitrary graphs to those finite state spaces are prose arguments in the paper and are not machine-checked.

The claim has not been refereed, and no independent mathematician has audited the graph-theoretic core. The author describes extensive model-assisted hostile auditing of his own argument, which is worth something but is not external review, and says so plainly.

What the AI did

GPT-5.6 Sol was the primary proof-development and hostile-audit system. It contributed substantial portions of the graph-theoretic reductions and terminal arguments, audited smoothing-edge scope, path and cycle simplicity, branch exhaustiveness, and graph-to-certificate coverage, and assisted in constructing and checking the finite verifiers. Claude Opus 5 was used as an ancillary prover for certain problems. GLM 5.3 Flash agents were used with the Danus framework earlier on in the problem-solving process.

Verification

Site-confirmed: the computational supplement was replayed here in full on 30 August 2026, and it passes.

What was run. Downloaded the supplement from its own Zenodo record (10.5281/zenodo.22167084), checked all 86 files against the shipped MANIFEST_SHA256.txt\texttt{MANIFEST\_SHA256.txt} - 86 match, 0 mismatch, 0 missing - then executed its run_all.ps1\texttt{run\_all.ps1} driver end to end. Result: "All certificate runs passed: 47", exit 0, in 33 min 53 s. Every per-run line reported exit=0\texttt{exit=0}, and the only occurrences of "fail" in the fresh verification record are four instances of "failures: 0". Both toolchains ran, Python and JavaScript, including the bipartite verifiers, whose output reports "checked rows: 580, failures: 0" and "verified rich pairs: 78".

What this does NOT establish, and it is the larger half. In the supplement's own words: "The programs verify only the finite propositions listed in PROPOSITION_MAP.md. The reductions from arbitrary graphs to those finite state spaces, and the proofs that a reported forbidden object expands to a simple cycle or path in the original graph, are mathematical arguments in the paper. The programs do not replace those graph-to-state theorems."

So the nine computer-assisted proposition families are exactly what the author says they are, and reproducibly so. The argument that carries them to every graph of minimum degree five is unrefereed prose that no independent mathematician has read. That is why the entry remains a candidate.

Sources

Submitted by eli on

Changelog3 changes
  • Rasmus Lindahlchanged Verification from “unreviewed” to “site-confirmed”
  • Rasmus Lindahlapproved this entry
  • elisubmitted this entry

Discussion1

Rasmus Lindahl30 Aug 2026, 10:55 UTC

Replayed the computational supplement here in full, and it passes.

Downloaded it from its own Zenodo record, checked all 86 files against the shipped MANIFEST_SHA256.txt (86 match, 0 mismatch, 0 missing), then ran run_all.ps1 end to end:

All certificate runs passed: 47
EXIT=0, elapsed 2033.4s

Every per-run line reported exit=0. The only matches for "fail" in the fresh verification record are four instances of "failures: 0". Both toolchains ran - 36 Python verifiers and 2 JavaScript under node - plus the three bipartite verifiers, which report "checked rows: 580, failures: 0" and "verified rich pairs: 78". The heaviest certificates were verify_two024_eeo_odd_cap_fullH_subsets.py and search_m4_n8_regimes.py at around 277s each.

Verification therefore moves to site-confirmed, and the note records what was run.

The status stays **candidate**, which is not a hedge. Replaying the certificates does not touch the part of the paper that would settle Dean's conjecture: the supplement itself says the programs verify only the finite propositions, and that the reductions from arbitrary graphs to those finite state spaces are mathematical arguments in the paper. A green suite means the finite half is exactly as described and reproducible by anyone. The graph-theoretic core still has no independent reader.

Two DOIs are now linked from the entry - the paper and the supplement - since neither was reachable from it before.