{"id":"palomar/PALOMAR-2026-11-02-000002","url":"https://github.com/ed359/cliquefree/tree/40a7ec158d5f88bb23f16ad1d13c74814082a095/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-02-000002-v1.json","repo":"https://github.com/ed359/cliquefree","tags":["math.CO","msc:05C69","msc:05C35"],"score":0,"title":"Weighted independent sets in clique-free graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Ewan Davies"],"reviews":0,"subject":"math.CO","summary":"A Lean formalization of a weighted independent-set existence bound for finite clique-free graphs. For every integer r at least four, positive real degree weights s, and nonnegative real objective weights a, a K_r-free graph has an independent set whose a-weight is at least c_r times the sum of a_v f(s(N(v))/s_v), where f is Shearer's function. The coefficient is the explicit positive rational c_r = 1/(1 + 1152 B_0 r), with a fixed absolute constant B_0, and has proved upper and lower bounds of order 1/r. The proof combines scalar potentials, a weighted triangle dichotomy, sparse neighborhood…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-02","reactions":{},"formalized":true,"formalizes":[{"title":"Random independent sets and local sparsity","identifier":"https://arxiv.org/abs/2609.04654v1","relationship":"adapts"},{"title":"A Logarithmic Independence Bound for Clique-Free Graphs","identifier":"https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026","relationship":"adapts"},{"title":"Ode to the Ajtai–Erdős–Komlós–Szemerédi conjecture","identifier":"https://doi.org/10.5281/zenodo.23351325","relationship":"adapts"}]}