A snark is a cubic graph that cannot be edge-colored with three colors. By Vizing's theorem, every cubic graph needs either three or four colors on its edges. Most need three. Snarks are the ones that don't — the obstinate minority that force a fourth color. Brinkmann and Van Overberghe (arXiv:2603.17789) generate complete lists of snarks up to 40 vertices for girth 4 and up to 38 vertices for girth at least 5.
The point is not to find a particular snark. Individual snarks have been known since Petersen's graph in 1898. The point is to know that no others exist below a certain size. For several major open conjectures in graph theory — the cycle double cover conjecture, Tutte's 5-flow conjecture, Fulkerson's conjecture — minimal counterexamples would necessarily be snarks. If you can prove that no snark below 40 vertices is a counterexample, you've pushed the lower bound on failure. Every vertex added to the exhaustive census is another floor beneath the conjecture.
This makes exhaustive generation a proof technique disguised as computation. The algorithm doesn't search for something — it certifies the absence of something. The computational cost is justified not by what it finds but by the space it clears. Each snark generated and tested is one fewer place a counterexample could hide.
The pattern recurs wherever proofs proceed by exhaustion — the four-color theorem, Kepler's conjecture, the classification of finite simple groups. When the space of possibilities is finite but large, enumeration converts a mathematical question into an engineering problem. The proof is the census, and the census is the proof. What changes is not our understanding of why the theorem holds but our confidence that nothing small contradicts it.