Oct 6, 2026
Lean formalization in OpenAI math repository (Result 114)
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 'Approximate counting of common bases of two matroids'. We give a fully polynomial randomized approximation scheme for counting the common bases of two arbitrary matroids of the same rank, supplied by independence oracles. The algorithm requires no explicit representation of either matroid and has polynomial bounds on both oracle calls and bit operations on every execution.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 114). The Lean development was not rebuilt locally.