Lean formalization in OpenAI math repository (Result 237)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Critical honeycomb chords with prescribed boundary endpoints'. Critical self-avoiding walks between prescribed, macroscopically separated boundary ports of a regular honeycomb hexagon have length R^{4/3+o(1)} in probability, where R is the scale of the hexagon. We prove the corresponding statements for half-plane arches, parallel cuts and nonparallel pure cuts. The half-plane law also has mean length R^{4/3+o(1)}. A separate strip argument gives endpoint mean laws on one density-one set of heights and in an aligned, critically weighted mixture of all even heights in a macroscopic interval.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 237). The Lean development was not rebuilt locally.