The paper tackles a long-standing open problem in combinatorics about binary matrices, which are grids of zeros and ones where each row and column has a fixed number of ones. The set of all such matrices sharing the same row and column totals can be thought of as a network, where two matrices are connected if you can get from one to the other by a single "swap": picking a 2x2 subgrid with ones in opposite corners and flipping them. This network is called an interchange graph. A classical question, posed by mathematician Richard Brualdi decades ago, asks whether you can always find a route through this network that visits every matrix exactly once and returns to the start, a so-called Hamiltonian cycle.
The authors prove something stronger than Brualdi's conjecture: not only does such a route always exist, but the network has the richest possible connectivity of this kind. Depending on the structure of the network, this means either that any two vertices can be connected by a Hamiltonian path, or that the network satisfies an even stricter condition involving pairs of paths. The proof works by breaking each interchange graph into simpler building blocks using a kind of multiplication structure, then handling each type of building block separately. Some blocks are recognized as well-studied graphs like Johnson graphs, others are handled through a clever geometric construction, and the bipartite cases rely on a recent theorem about covering graphs with pairs of disjoint paths.
A particularly notable feature of the paper is that the entire proof has been formally verified by a computer using the Lean 4 proof assistant, meaning every logical step was checked from first principles by software. This is a significant achievement given the length and complexity of the argument, and even some intermediate results the proof depends on were themselves formalized as part of the project. The combination of resolving a decades-old conjecture with a machine-checked proof represents both a mathematical and a computational milestone.