Quadratic stabilization of the canonical Foulkes–Howe map

Lean formalization in OpenAI math repository (Result 210)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Quadratic stabilization of the canonical Foulkes–Howe map'. For every finite-dimensional complex vector space V, we prove that the canonical Foulkes–Howe map \mathop{\mathrm{Sym}}\nolimits ^b(\mathop{\mathrm{Sym}}\nolimits ^a V)\longrightarrow\mathop{\mathrm{Sym}}\nolimits ^a(\mathop{\mathrm{Sym}}\nolimits ^b V) is surjective whenever a ≥ 2 and b\ge a(a-1). This gives a quadratic stabilization bound independent of \dim V.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 210). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository