Revision #1570 → #1795 · back to history
addedMetropolis–Hastings algorithm07d5c0d7e2ab
modifiedTSP neighbors as permutations2ee7bd611cac
| Field | From #1570 | To #1795 |
|---|
| mathlib.match_kind | — | generalization |
| note | Permutations are formalized as `Equiv.Perm`, but the TSP state space and its neighbor structure are not in Mathlib. | Permutations are formalized as `Equiv.Perm` (confirmed), but the TSP state space and its neighbor structure are not in Mathlib. |
addedReduction to greedy algorithm at T=035bc05eaa2bf
modifiedTSP state count for n=204b3889fc407f
| Field | From #1570 | To #1795 |
|---|
| mathlib.match_kind | — | generalization |
| note | The factorial function `Nat.factorial` is formalized (so 20! is computable), but the TSP state-counting example itself is not in Mathlib. | The factorial function `Nat.factorial` is formalized (confirmed) so 20! is computable, but the TSP state-counting example itself is not in Mathlib. |