AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Nontrivial Markov Type Forces Superreflexivity

Can the mathematical statement in Nontrivial Markov Type Forces Superreflexivity be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 327)

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 'Nontrivial Markov Type Forces Superreflexivity'. We prove that every real Banach space with Markov type p > 1 is superreflexive. Together with the known converse, this characterizes superreflexivity by nontrivial Markov type. This answers Naor's question: every real Banach space with nontrivial Markov type admits an equivalent uniformly smooth norm.

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