{"id":"palomar/PALOMAR-2026-10-21-000017","url":"https://github.com/mbucic4/Induced-Erdos-Sauer/tree/6990e58d8ec5f771ac3a3a76adfdfd341702bdfe","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000017-v1.json","repo":"https://github.com/mbucic4/Induced-Erdos-Sauer","tags":["math.CO","extremal-combinatorics","graph-theory","induced-subgraphs","lean"],"score":0,"title":"Induced Erdős–Sauer: an n log log n bound","trust":"high","domain":"math.CO","source":"palomar","authors":["Matija Bucic","Fankang He","Hyunwoo Lee"],"reviews":0,"subject":"math.CO","summary":"We formalize in Lean an O_k(n log log n) bound for the induced Erdős–Sauer problem. For every fixed integer k >= 3, there is a constant C_k > 0 such that every finite simple graph on n >= 1 vertices with more than C_k n log(log(4n)) edges contains a nonempty induced k-regular subgraph. The result is unconditional, and the constants depending on k are not optimized.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"On the induced Erdős–Sauer problem","identifier":"sha256:7c60f46a6c6d0d8036aa33fa97a4d6f4e018c63e69d98fb001f2c80da3e523fb","relationship":"adapts"},{"title":"A power-saving bound for k-sunflower-free sets via interpolation and slice rank","identifier":"sha256:86bea95dcae66f3c2d89f5d3935b6eba89f3df411e377b38690750f35fdf23cd","relationship":"adapts"},{"title":"Regular subhypergraphs of uniform hypergraphs","identifier":"sha256:3a142a3b454140149052a1009a67fd78b0f41d819fa5e131d421cbf7cd6b0378","relationship":"adapts"}]}