{"id":"palomar/PALOMAR-2026-10-11-000008","url":"https://github.com/scottnarmstrong/DOZZ/tree/5d770d1a6d69fac6dbb63060e8a89861bf3ee330","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000008-v1.json","repo":"https://github.com/scottnarmstrong/DOZZ","tags":["math.PR","math-ph","math.MP","hep-th","msc:60G60","msc:60G57","msc:81T40","msc:60J65","msc:33C05","msc:33B15"],"score":0,"title":"Integrability of Liouville theory: the Kupiainen–Rhodes–Vargas proof of the DOZZ formula","trust":"high","domain":"math.PR","source":"palomar","authors":["Scott Armstrong","Amélie Loher"],"reviews":0,"subject":"math.PR","summary":"A Lean 4 / Mathlib formalization of the theorem of A. Kupiainen, R. Rhodes and V. Vargas (Annals of Mathematics, 2020) that the three-point structure constants of Liouville conformal field theory on the Riemann sphere are given by the DOZZ formula of Dorn–Otto and Zamolodchikov–Zamolodchikov. The structure constants are defined probabilistically: for 0 0 and charges satisfying the extended Seiberg bounds, C_gamma(alpha_1, alpha_2, alpha_3) = 2 mu^(-s) gamma^(-1) Gamma(s) E[rho^(-s)], where rho integrates explicit power weights against the Gaussian multiplicative chaos of the Gaussian free…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true,"formalizes":[{"title":"Integrability of Liouville theory: proof of the DOZZ formula","identifier":"","relationship":"formalizes"},{"title":"Liouville quantum gravity on the Riemann sphere","identifier":"","relationship":"formalizes"},{"title":"Local conformal structure of Liouville quantum gravity","identifier":"","relationship":"formalizes"},{"title":"An elementary approach to Gaussian multiplicative chaos","identifier":"","relationship":"adapts"},{"title":"Brownian motion in Lean","identifier":"","relationship":"adapts"}]}