Choiceless polynomial time with counting does not capture polynomial time

Lean formalization in OpenAI math repository (Result 243)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Choiceless polynomial time with counting does not capture polynomial time'. We prove that choiceless polynomial time with counting does not capture polynomial time on unordered finite structures, confirming the noncapture conjecture of Blass, Gurevich and Shelah. A linear-consistency query over 𝔽3 in a fixed binary vocabulary is decidable in polynomial time but not in the full counting formalism.

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

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