Prove FKCRT (openai/math family 211: Geometry, diffusion, and spectra of random planar maps) in Lean 4 with…
Prove FKCRT (openai/math family 211: Geometry, diffusion, and spectra of random planar maps) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 211 of the release, Geometry, diffusion, and spectra of random planar maps…
The task
Context: this statement belongs to family 211 of the release, *Geometry, diffusion, and spectra of random planar maps* (Probability and statistical mechanics). The family as a whole: Critical Fortuin–Kasteleyn planar maps converge to Liouville quantum gravity spheres for $0<q\le4$ and to the Brownian continuum random…
Part of raising-heart/openai-math.