A browser walkthrough of TSP ideas plus a pinned, single-run Rust benchmark packet covering 14 to 7,397 cities. The browser demonstration is not generated from Lean and does not execute the Rust solver.
Click to add. Watch the possibilities explode.
Place a dot on the canvas. That is your first vertex. Add a second and there is one closed tour. This page counts symmetric tours after fixing the start and identifying a tour with its reverse: one tour for three vertices, three for four, and twelve for five.
Under that single convention, ten vertices give exactly 181,440 tours, twenty-five give about 3.1022 × 10^23, and fifty give about 3.0414 × 10^62. The underlying integer counts use exact factorial arithmetic; the displayed scientific notation is truncated to five significant digits.
Click to place your first city.
Any wasteful route can be tightened. The triangle inequality guarantees it.
Before you can solve the problem, you need a guarantee. Here is the simplest one: if you have a walk that visits every city but backtracks through some of them twice, you can always straighten it into a proper tour without making it longer.
The reason is the triangle inequality: the direct path between two points is never longer than the detour through a third. Every backtrack is a detour. Cut it out, and the walk gets shorter or stays the same.
This is the shortcutting lemma. The named Lean theorem checks the metric statement for a closed walk that visits every vertex. The canvas below is an independent browser illustration, not extracted proof code.
Always picking the closest city looks smart until the last five.
The most natural strategy is the simplest one: start somewhere, go to the nearest city you have not visited, repeat. This is the nearest-neighbor algorithm. The small fixed scene below runs locally in this browser; it supplies no general runtime bound.
Watch what happens. The first few moves look perfect. Short hops, tight connections. But around two-thirds of the way through, the algorithm starts to struggle. The remaining cities are scattered far from the current position. The last few edges are long, ugly cross-country jumps that undo all the early efficiency.
In this constructed scene, nearest neighbor can leave expensive closing edges. Its gap depends on the instance and starting vertex, so this illustration does not assign a typical percentage. The lesson is narrower: local choices do not guarantee a globally shortest tour.
Find an improving two-edge exchange. Reverse the intervening segment. Repeat until this implementation finds none.
Take the tour from nearest neighbor and inspect pairs of edges. Crossing edges are one visible source of improvement, but a two-opt exchange need not be a geometric uncrossing. The browser reverses a segment only when its computed Euclidean tour length strictly decreases.
Press the button below to watch one improving exchange at a time. The sparkline tracks the computed tour length. When the scan finds no improvement, the tour is locally optimal only with respect to the two-opt neighborhood and tolerance implemented here—not every possible move sequence.
The Lean corpus proves a conditional termination theorem when every improving move satisfies the stated realizable-tour weight identity. This browser implementation is separately tested and does not inherit that theorem automatically.
Sometimes you have to make the tour worse before you can make it better.
Two-opt can only see one move ahead. But some improvements require making things temporarily worse to reach something better. Lin-Kernighan explores these deeper moves: remove one edge, add a new one to a non-adjacent city, remove another, add another. A chain of swaps that looks bad at step two but pays off at step four.
Variable-depth search can examine move chains outside one two-opt exchange. The pinned packet labels its 22-to-442-city runs as a combined Christofides, two-opt, and LK pipeline, so it does not isolate LK's marginal effect.
Shen Lin and Brian Kernighan published their variable-depth TSP heuristic in 1973. This page uses that historical algorithm family as explanation, not as a claim about every competitive solver.
Break the tour into four pieces. Reassemble. Clean up. Keep the best.
A particular Lin-Kernighan implementation can stop when its permitted move search finds no improvement. That stopping point is local to its move class and implementation; it does not prove that no other edge-swap sequence or algorithm can improve the tour.
The double bridge is the escape hatch. It cuts the tour into four pieces and reassembles them in a different order. The tour gets abruptly worse. Then LK runs again from the new starting point, descending into a different local optimum. Sometimes that new optimum is better than anything found before.
Below, a fixed seed generates fifty illustrative restart cycles: each spike represents a perturbation and each descent represents local cleanup. The amber line tracks the synthetic best-so-far value. This canvas is explanatory animation, not solver output or benchmark evidence.
Each dot is a recorded TSPLIB result in the pinned benchmark packet. Green means the recorded tour matches the known optimum.
Each dot is one of 28 standard benchmark problems with a known optimal solution. The vertical position shows how far the packet's recorded tour is from that optimum. Four runs match the known optimum; 18 are within 2%, and the maximum recorded gap is 7.21%. These are experiments, not theorem conclusions.
Twenty-eight single runs, 14 to 7,397 cities—no extrapolation beyond the artifact.
The points copy wall-clock observations from solver/benchmarks/scientific_results.json at Kristi commit 4730fe1. The protocol records one deterministic, single-threaded release run per instance on the dated M3 Ultra environment, so the connecting line is only a visual guide—not a complexity fit, reproducibility interval, or hardware-independent forecast.