Oct 6, 2026
Lean formalization in OpenAI math repository (Result 220)
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 'Directional transience implies ballisticity'. We prove that almost-sure transience in a fixed direction implies a deterministic limiting velocity with positive projection in that direction for nearest-neighbor random walks in independent and identically distributed uniformly elliptic environments on ℤd, d ≥ 2. This resolves the ballisticity conjecture positively.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 220). The Lean development was not rebuilt locally.