{"id":"palomar/PALOMAR-2026-10-14-000004","url":"https://github.com/linrock/math-proofs/tree/2c2d2f773f1dde69452b0cde525ff6ee633c49d0/erdos-836","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-14-000004-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.CO","msc:05C15","msc:05C65","msc:05D05","extremal-set-theory","hypergraphs","chromatic-number","lean"],"score":0,"title":"Erdős 836: vertex counts and pairwise edge intersections in 3-chromatic intersecting uniform hypergraphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.CO","summary":"A complete Lean 4 resolution of both parts of Erdős problem 836 (posed by Erdős and Shelah; Erdős and Lovász, 1975) on 3-chromatic intersecting r-uniform hypergraphs, together with structural bounds on the Erdős–Shelah codimension-one avoidance question. For Part (i), it formalizes Noga Alon's equitable-partition construction with (2r - 2) + C(2r - 2, r - 1) / 2 active vertices to disprove the O(r²) vertex bound for all r ≥ 2. For Part (ii), it adapts and generalizes Liam Price's minimal-blue bipartite double-counting argument to prove the universal bound r ≤ 2t + 1 when distinct edges meet…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-14","reactions":{},"formalized":true,"formalizes":[{"title":"Problems and results on 3-chromatic hypergraphs and some related questions","identifier":"https://www.erdosproblems.com/836","relationship":"formalizes"},{"title":"A Linear Intersection Bound","identifier":"https://www.overleaf.com/read/bhnhxhswnjht#52529b","relationship":"adapts"}]}