Worked solution: Gladkov–Pak–Zimin's explicit counterexample disproving the bunkbed conjecture (2024)
Having proved the inequality flips, the authors also worked out roughly how much it flips by — and the answer is startling: on their -vertex graph, the gap between the two probabilities is smaller than , a number so tiny it has no meaningful decimal representation and is utterly beyond reach of any computer simulation. This is why the earlier steps' careful, purely analytical chain of lemmas was essential — no amount of computing power could ever have detected a gap this small by direct experiment on a graph this size.
To get a feel for the effect at a scale computers actually can probe, the authors also tried much smaller versions of the same construction: an -vertex graph already shows a gap of about , and a further, differently weighted -vertex version shows a gap around — both still far too small to see by simulating individual random outcomes, but small enough to be confirmed by exact computer calculation.
Gladkov, Pak and Zimin (2024, Remark 4.2) note that because of the multiple layers of conditioning involved in substituting six copies of the gadget into Hollom's hypergraph, the actual gap on their -vertex counterexample is smaller than — far too small ever to detect computationally, and a striking illustration of why the disproof had to be, and is, purely analytic rather than experimental.
To make the phenomenon experimentally visible, the authors separately computed (Section 7 of the paper) that using a smaller gadget parameter, , gives a graph on only vertices with a computationally detectable gap of order ; using the closely related weighted bunkbed conjecture (an equivalent formulation allowing edge-dependent probabilities) with a further-optimised small gadget (, ) gives a -vertex graph with a gap of order . These experiments, run and cross-checked by computer, do not replace the analytic proof of Theorem 1.2, but they confirm the qualitative mechanism at a human-comprehensible scale and were used to search for and validate smaller instances of the phenomenon.
This combination — an unconditional analytic proof for the large, explicit counterexample, supplemented by targeted computer experiments on smaller relatives to build intuition and probe how small a counterexample might ultimately be possible — reflects a proof style increasingly common in modern combinatorics, even though (unlike the four colour theorem or the aperiodic monotile results) no step of the core proof here actually depends on computer verification.