For Kristi Jacoby
The Traveling Salesman Problem, kernel-checked.
Eleven thousand declarations on approximation, complexity, and combinatorial structure. The first improvement to the 3/2 approximation ratio in 45 years, formally verified.
Crown Results
Shortcutting
Metric TSP shortcutting preserves the tour
Shortcutting a doubled MST Euler tour by skipping visited nodes never increases total distance. The triangle inequality is the only hypothesis.
No crossing
Optimal tours don't cross
In the Euclidean plane, an optimal TSP tour has no self-intersections. Uncrossing any crossing strictly reduces length.
Matroid bridge
MST structure via matroid intersection
The minimum spanning tree is the unique base of the graphic matroid with minimum weight. Bridges Christofides to matroid theory.
Live Application
17-Week Optimized Sales Route
505 medical accounts across California and Hawaii. TSP-optimized weekly routes: 494 visits, 5,935 miles, 97.8% compliance. The same algorithm the theorems prove.
View schedule →A commission for Kristi Jacoby. 569 theorems. 35 lemmas. 119 definitions. 18 open problems. Shortcutting and NoCrossing are both kernel-clean under #print axioms. Build status GREEN.