Oct 6, 2026
Lean formalization in OpenAI math repository (Result 148)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'The entropy-rate dimension formula for self-similar measures on the line'. We prove that the Hausdorff dimension of every finite real self-similar measure equals the minimum of one and its random-walk entropy rate divided by its Lyapunov exponent. Exact overlaps are allowed, and the contraction ratios may be unequal and negative. This resolves the entropy-rate dimension conjecture.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 148). The Lean development was not rebuilt locally.