{"id":"palomar/PALOMAR-2026-10-27-000016","url":"https://github.com/methuku-git-hub/Independent-sets-in-hypergraphs-with-no-loose-triangle/tree/ea281d7cf047227e8fde38bfc124db1117ed7c37","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000016-v1.json","repo":"https://github.com/methuku-git-hub/Independent-sets-in-hypergraphs-with-no-loose-triangle","tags":["math.CO","msc:05C65","msc:05C69"],"score":0,"title":"Independent sets in hypergraphs with no loose triangle","trust":"high","domain":"math.CO","source":"palomar","authors":["Abhishek Methuku"],"reviews":0,"subject":"math.CO","summary":"Conditional Lean formalisation of “Independent sets in hypergraphs with no loose triangle” by Ayush Basu, Abhishek Dhawan and Abhishek Methuku. Assuming the explicitly stated normalized Li–Postle vertex-coloring bound for triangle-free hypergraphs with edges of sizes 3 and 4, for every fixed integer r >= 3 there are constants c > 0 and N such that every n-vertex hypergraph with n >= N, edge sizes between 3 and r, and no loose triangle has an independent set of size at least c n^(2/3) (log log n)^(1/3). The implication is proved in Lean; the Li–Postle premise and the manuscript's Ramsey…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"Independent sets in hypergraphs with no loose triangle","identifier":"https://github.com/methuku-git-hub/Independent-sets-in-hypergraphs-with-no-loose-triangle/blob/8c1ffa95ef08c6788434011dbb0bc794884e8bb8/manuscript/KMV_proof.tex","relationship":"formalizes"},{"title":"Hypergraph Ramsey numbers: Triangles versus cliques","identifier":"https://doi.org/10.1016/j.jcta.2013.04.009","relationship":"adapts"}]}