{"id":"palomar/PALOMAR-2026-10-23-000011","url":"https://github.com/ziqingxiang/dgs/tree/7499bbb80a966cb3abef8856a8cec183cb3c1d99","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000011-v1.json","repo":"https://github.com/ziqingxiang/dgs","tags":["math.CO","msc:05C50","msc:05C80","msc:15B52","msc:60B20","spectral-graph-theory","haemers-conjecture","formalization"],"score":0,"title":"Almost all graphs are determined by their generalized spectrum","trust":"high","domain":"math.CO","source":"palomar","authors":["Ziqing Xiang"],"reviews":0,"subject":"math.CO","summary":"A complete Lean 4 and Mathlib formalization of the theorem that almost all graphs are determined by their generalized spectrum, which is Haemers' conjecture for the generalized spectrum. The generalized spectrum of a graph is the spectrum of its adjacency matrix A together with the spectrum of the adjacency matrix J - I - A of its complement, and a graph is determined by its generalized spectrum (DGS) if every graph with the same generalized spectrum is isomorphic to it. The main theorem, DGSMain.almost_all_graphs_are_DGS, states that the proportion of the graphs on the vertex set {0, ...,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"Almost all graphs are determined by their generalized spectrum","identifier":"arXiv:2610.11047","relationship":"formalizes"}]}