Cook, Hougardy, and Petrich (arXiv:2603.12995), extending exact integrality gap computations for the metric TSP, discovered that published enumerations of the subtour polytope were incomplete: one extreme point was missing for n=11 and twenty-two were missing for n=12.
The through-claim: exhaustive computation is only as exhaustive as its last check. The 4/3-conjecture for the metric TSP — that the ratio between the integer optimum and the subtour relaxation never exceeds 4/3 — has been verified computationally for small instances since Benoit and Boyd's 2008 work. But extending the computation to n=12, 14, and 17 revealed that the foundation was incomplete. Twenty-three extreme points that should have appeared in earlier enumerations were absent.
The finding is uncomfortable because the purpose of exact computation is to provide certainty below a threshold. If the enumeration missed 22 points at n=12, how confident can we be about n=10? (They re-verified: n=10 is correct.) The error propagation in exhaustive search is binary — you either have all cases or you don't — and missing a single case can invalidate the entire verification.
The broader pattern: verification that depends on enumeration inherits the fragility of the enumeration. Every formally verified proof, every exhaustive search, every “complete” database carries this risk. The missing vertex isn't a counterexample to the 4/3-conjecture — the conjecture still holds through n=17. But it's a counterexample to the assumption that exhaustive computation is self-certifying.