{"id":"palomar/PALOMAR-2026-10-28-000014","url":"https://github.com/scottnarmstrong/Critical2DKPZ/tree/f1c98dacb2a83737096bd976019dfa2c5986ee5a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000014-v1.json","repo":"https://github.com/scottnarmstrong/Critical2DKPZ","tags":["math.PR","math-ph","msc:60H17","msc:60F17","msc:60G60","msc:82D60"],"score":0,"title":"The Critical 2D KPZ Process","trust":"high","domain":"math.PR","source":"palomar","authors":["Scott Armstrong"],"reviews":0,"subject":"math.PR","summary":"A Lean 4 formalization of \"The Critical 2D KPZ Process\" by Berger, Caravenna, Clark, Dunlap, Gu, Liu, Nakajima, Sun, Tsai, Xie and Zygouras (arXiv:2610.31614, version 1), together with selected inputs and adaptations in the form these proofs need. For directed polymers on Z^2 in a Gaussian environment at critical disorder, it proves the existence of a critical 2D stochastic heat flow, defined as the joint limit in law of the rescaled partition functions (Theorem A). The centred log-partition function converges in law, in the local negative Sobolev spaces H^{-a}_loc and jointly in finitely…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"The Critical 2D KPZ Process","identifier":"","relationship":"formalizes"},{"title":"Four results on the critical 2D KPZ process","identifier":"","relationship":"formalizes"},{"title":"The Parisi formula has a unique minimizer","identifier":"","relationship":"adapts"},{"title":"Concentration functions and entropy bounds for discrete log-concave distributions","identifier":"","relationship":"adapts"},{"title":"Quasi-critical fluctuations for 2D directed polymers","identifier":"","relationship":"adapts"}]}