What was already known
Davila proposed the diamond-free bound as Conjecture 9 while proving a related claw-free statement.
AI involvement
Claude agents proposed the graph and checkers. John Erlbacher directed the campaign, audited its verification gates and accepts responsibility; individual-result autonomy is not documented.
The release credits AI agents with proposing retained constructions or proofs and Erlbacher with directing the campaign; AI-centered is the supported individual-result level.
Importance
A finite graph disproves the proposed universal zero-forcing bound.
Limitations
Independent exact Python and Rust checks cover the 14-vertex graph. Larger checked chain examples do not prove an unbounded Z−γ gap.
Technical verification
Independent exact Python and Rust checks reportedly certify the graph properties, domination number and zero-forcing number; larger chain examples are separate.
Formal checking
exact computation
- Checker
- checker_conj9.py and independent Rust checker
- Scope
- The 14-vertex graph with γ=4 and Z=7 against Conjecture 9
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Human direction and gate auditing are documented, but no named person explains the central reasoning of this individual AI result. Few is the evidence default, not a finding of inability to understand it.
Correction and publication history
A finite graph disproves the proposed universal zero-forcing bound.
Read this published revision