AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Counterexamples to the duality conjecture for metric entropy

Does the classical conjecture or property hold, or does there exist a counterexample as established in Counterexamples to the duality conjecture for metric entropy?

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 329)

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Counterexamples to the duality conjecture for metric entropy'. We disprove Pietsch's dimension-free duality conjecture for metric entropy. For every proposed pair of universal constants, we construct origin-symmetric convex bodies that violate the corresponding covering-entropy inequality, already when the covering body is a cube.

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