{"id":"palomar/PALOMAR-2026-10-19-000018","url":"https://github.com/mkwn/triangle-free-probability/tree/2d3c19f579dc366a3cbe2083df58a51909a23af0","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-19-000018-v1.json","repo":"https://github.com/mkwn/triangle-free-probability","tags":["math.CO","math.PR","msc:05C80","msc:60F10","random-graphs","large-deviations","formalization"],"score":0,"title":"A certificate for the triangle variational problem","trust":"high","domain":"math.CO","source":"palomar","authors":["Matthew Kwan","Huy Tuan Pham"],"reviews":0,"subject":"math.CO","summary":"A Lean formalization of a technical lemma in the paper \"Nonlinear lower-tail large deviations at criticality\" by Matthew Kwan and Huy Tuan Pham. This lemma is used to solve a certain variational problem, which is necessary to characterise the probability that a random graph is triangle-free in the so-called \"critical regime\" where the edge probability is of order 1 / sqrt n. Specifically, this lemma defines a \"certificate function\" G and proves that it satisfies a certain inequality. This involves lots of interval arithmetic.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"Nonlinear lower-tail large deviations at criticality","identifier":"","relationship":"formalizes"}]}