AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces

Can the mathematical statement in Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces 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 328)

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 'Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces'. Every nonexpansive selfmap of a nonempty closed bounded convex subset of a real reflexive Banach space has a fixed point. This resolves the reflexive-space fixed point problem for the given norm.

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