Traveling Salesman Problem
Metric TSP, with two named Lean receipts.
Two pinned source theorems cover shortcutting under a triangle inequality and crossing exclusion under an explicit typeclass hypothesis. The manifest handlers are intentionally non-dispatchable, and the browser planner uses a fixed-seed synthetic normalized-plane fixture—not Lean-extracted code or real-world route records.
2
named receipts
105
source files
14
lexical sorry
Route receipts
These exact theorem names were checked locally at the pinned source. The browser planner is separately tested and is not extracted from Lean.