Brualdi's Question on Hamiltonicity of Interchange Graphs
The interchange graph has the -matrices with row sums and column sums as vertices, adjacent when they differ by a single interchange. Brualdi asked whether is always Hamiltonian. It satisfies more: it is maximally Hamiltonian, Hamilton-laceable when bipartite and Hamilton-connected when not.
- Result
- Proved
- Status
- Resolved
- AI contribution
- AI-assisted
- Method
- Argument
- Field
- Combinatorial matrix theory
- Posed by
- Richard A. Brualdi
- Year posed
- 1980
- Years open
- 46y
- Solved
- 2026-07-14
- Model
- Claude, GPT/Codex
- Vendor
- Anthropic / OpenAI
- Collaborators
- Jeffrey S. Baggett, Huiya Yan
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 15 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
The declaration says the computational search and verification programs and the Lean 4 formalization were developed with AI-assisted tools under author direction, and that no AI system is an author. The structural induction carrying the proof is the authors'.
Verification
The paper reports a Lean 4 formalization alongside computational search and verification programs. We have not compiled it. arXiv preprint, not yet peer-reviewed.
Source
arXiv:2607.13165 - Interchange graphs of (0,1)-matrices are maximally Hamiltonian