Report
THEO team presents a Lean 4 formalization of Babai’s graph isomorphism algorithm
THEO’s researchers say they found 90-plus corrections and proved an explicit exp(O(log^5 n)) running-time bound.
TLDR
THEO’s researchers say they formalized László Babai’s quasipolynomial-time graph isomorphism algorithm in Lean 4, which mechanically checks mathematical proofs. They report finding 90-plus corrections in Babai’s incomplete 2018 paper and proving an explicit exp(O(log^5 n)) running-time bound down to a random-access machine model. They also shared a corrected paper and 22,000-plus Lean 4 declarations.
Combined views
—
2 Sources, first seen ago
