Graph isomorphism in quasipolynomial time on a single-tape Turing machine
A Lean 4 and Mathlib formalization of Babai's quasipolynomial-time algorithm for graph isomorphism, without the classification of finite simple groups, carried down to Turing machines. There is a single-tape Turing machine (Mathlib's Turing.TM0) that decides whether two simple graphs on n vertices, given in a fixed encoding, are isomorphic within 2^(c (floor(log2 n) + 1)^8) transitions, and another that within the same bound outputs either "not isomorphic" or an isomorphism τ together with generators of a subgroup whose left coset by τ is exactly the set of all isomorphisms. The algorithm…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-29-000015
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-29-000015/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-29-000015/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'