{"id":"palomar/PALOMAR-2026-09-02-000006","url":"https://github.com/SamPetkov/Erdos625-formalization/tree/9702b5e734627e3fdaef8da0d65ad7394016f0a7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-02-000006-v1.json","repo":"https://github.com/SamPetkov/Erdos625-formalization","tags":["math.CO","math.PR","msc:05C15","msc:05C80","msc:60C05","random-graphs","graph-coloring","lean","erdos-problems"],"score":0,"title":"Erdős Problem 625: chromatic versus cochromatic number of a random graph","trust":"high","domain":"math.CO","source":"palomar","authors":["Samuil Petkov"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 formalization of the full-sequence quantitative theorem for G(n,1/2): with probability tending to one, the chromatic number minus the cochromatic number is at least ((log 2)^2/4) log(200/153) times n/(log n)^3. The formal statement uses the finite binomial random-graph measure, natural-valued chromatic and cochromatic numbers, real subtraction, and convergence along all natural n.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-02","reactions":{},"formalized":true}