{"id":"palomar/PALOMAR-2026-10-23-000016","url":"https://github.com/jtraverso/mader-connectivity/tree/b471abcdfbb303aabc1af26f4531e080729bb469","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000016-v1.json","repo":"https://github.com/jtraverso/mader-connectivity","tags":["math.CO","msc:05C40","msc:05C35","graph-theory","connectivity","formalization"],"score":0,"title":"Mader's theorem on highly connected subgraphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Mader's 1972 theorem in the form of Diestel's Theorem 1.4.3: for k ≥ 1, every nonempty finite simple graph with average degree at least 4k has a (k + 1)-connected induced subgraph H with e(H)/|H| > e(G)/|G| − k. Vertex connectivity is defined by deletion of fewer than k vertices (same definition as in the Menger–Hamiltonicity entry). Mathlib does not contain vertex connectivity or this theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"Existenz n-fach zusammenhängender Teilgraphen in Graphen genügend großer Kantendichte","identifier":"doi:10.1007/BF02993903","relationship":"formalizes"},{"title":"Graph Theory","identifier":"","relationship":"formalizes"}]}