{"id":"palomar/PALOMAR-2026-10-29-000015","url":"https://github.com/troyjlee/graph-iso-lean/tree/3991d5f767d718937a2e2fa5178e6637f35bebb2/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000015-v1.json","repo":"https://github.com/troyjlee/graph-iso-lean","tags":["cs.DS","cs.CC","math.CO","math.GR","msc:68Q25","msc:05C60","msc:20-08","msc:20B15","msc:68V20"],"score":0,"title":"Graph isomorphism in quasipolynomial time on a single-tape Turing machine","trust":"high","domain":"cs.DS","source":"palomar","authors":["Troy Lee"],"reviews":0,"subject":"cs.DS","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"Graph Isomorphism in Quasipolynomial Time","identifier":"arXiv:1512.03547","relationship":"adapts"},{"title":"Fixing the UPCC case of Split-or-Johnson","identifier":"","relationship":"adapts"},{"title":"A CFSG-free analysis of Babai's quasipolynomial GI-algorithm","identifier":"arXiv:1605.08266","relationship":"adapts"},{"title":"Graph isomorphisms in quasi-polynomial time","identifier":"arXiv:1710.04574","relationship":"adapts"}]}