Nonexpansive fixed points in reflexive Banach spaces

Proves that every nonexpansive map of a closed bounded convex set in a reflexive Banach space has a fixed point.

1 paper September 24, 2026 Explained by AI

A nonexpansive map moves points without ever pulling two of them further apart. A fixed point is a point the map leaves where it is. In some infinite-dimensional spaces such maps can move every point. This paper proves that this cannot happen in real reflexive Banach spaces, a broad class that includes all Hilbert spaces. Lean checks the main theorem.

First step

1965

Browder, Göhde and Kirk, who proved fixed point theorems for uniformly convex spaces and for sets with normal structure

Significance

Landmark

It answers, with a Lean check, the reflexive-space question that fixed point theory had left open since the 1960s.

Trust

Formal proof listed

Field

Functional analysis

1 paper

The explanation

Turn a round disk by a quarter turn about its centre. The point (1, 0) goes to (0, 1). Any two points keep their distance; for (1, 0) and (0, 1) it stays √2, about 1.414. The centre does not move. A point a map leaves in place is a fixed point. A map that never pulls two points further apart is nonexpansive.

In ordinary finite-dimensional space, every nonexpansive map of a closed bounded convex set has a fixed point. Convex means the set contains the straight segment between any two of its points. In infinite dimensions this can fail. Take the space c0 of number sequences that tend to 0, with length the largest entry. Let C be the decreasing sequences between 0 and 1. Let F put a 1 in front: F(0.5, 0.2, 0, …) = (1, 0.5, 0.2, 0, …). F keeps all distances. A fixed point would have to be (1, 1, 1, …), which does not tend to 0. So F moves every point.

The question is which spaces avoid such examples. A Banach space is a space of vectors with a length, called a norm, where limits behave well. It is reflexive if its double dual, the space of linear measurements of linear measurements, is the space itself. Browder and Göhde proved the fixed point property for uniformly convex spacesSource 1. Kirk proved it for reflexive spaces with an extra shape condition called normal structureSource 2. Later work covered more classesSource 3. Alspach found a weakly compact convex set in the space L1 with a fixed-point-free nonexpansive mapSource 4. So compactness of that kind alone is not enough. A 2026 paper still records the reflexive question as unresolvedSource 5. An earlier claimed proof by Hanebaly exists, and this paper treats it as separateSource 6.

The paper proves the reflexive case in the given normSource 7. Every nonexpansive self-map of a nonempty closed bounded convex set in a real reflexive Banach space has a fixed point. As usual, the proof supposes a counterexampleSource 8. A classical reduction shrinks it to a small set of diameter one. There, nearly fixed points are almost as far as possible from every point of the set, by the Goebel–Karlovitz lemmaSource 9. The obstacle is turning this spread into a contradiction without any extra geometry. The paper builds an anchor point and a tree of nearly fixed images. A weighted bound on differences along the tree finds one vector that a whole branch of linear measurements detects. Yet those measurements tend to zero on the space, which is impossibleSource 10. A corollary extends the result to any family of commuting nonexpansive mapsSource 11.

How sure is this? Lean, a computer proof checker, has a formal statement of the main theorem. It covers every real reflexive Banach space, with no uniform convexity or normal structure assumed. So the paper proves this, as far as the Lean statement matches the paper. No specialist review is published.

What it doesn't show. This does not extend to non-reflexive spaces: weakly compact convex sets in L1 can still carry a nonexpansive map with no fixed point.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Landmark-level claim with a Lean check of the main theorem. It is about the original norm on reflexive spaces only; non-reflexive spaces such as L1 can still fail. No specialist review is published.

Words used

Banach space: A space of vectors with a length rule, called a norm, in which limits of sequences behave well.
Nonexpansive map: A map that never makes the distance between two points larger.
Fixed point: A point that the map sends to itself.
Convex set: A set that contains the straight segment between any two of its points.
Reflexive: A Banach space that equals its double dual, the space of linear measurements of its linear measurements.
Uniformly convex: A norm where the midpoint of two far-apart unit vectors is shorter than 1 by a fixed margin.
Normal structure: A shape condition: every convex piece with two or more points has a point closer than the diameter to all of the piece.

The original paper

Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces (PDF, opens in a new tab)
September 24, 2026 Formal proof listed

Lean notes

All quoted lines (11)

The classical results of Browder and G\"ohde prove the fixed point property for uniformly convex spaces.
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
The classical results of Browder and G\"ohde prove the fixed point property for uniformly convex spaces. Kirk's theorem applies when the closed bounded convex domain $C$ in a reflexive space has normal structure: every convex subset $D\subseteq C$ with more than one point must contain a point $a$ with $\sup_{z\in D}\norm{a-z}<\diam D$ .
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
Further results established the property for substantial classes beyond the uniformly convex case. Maurey proved it for reflexive subspaces of $L^1$ in the inherited norm.
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
Two other results distinguish the hypotheses of Theorem …. Alspach constructed a weakly compact convex subset of $L_1[0,1]$ with a fixed-point-free nonexpansive selfmap.
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
More recent discussion of the general question appears in, who records it as unresolved. These statements of the literature are distinct from the argument given here.
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
Hanebaly previously proposed a proof of this same original-norm assertion, and subsequently announced a further proof.
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
Every nonexpansive selfmap of a nonempty closed bounded convex subset of a real reflexive Banach space has a fixed point.
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
Suppose a counterexample exists. The classical minimal invariant set method reduces the problem to a separable weakly compact convex set $K$ of diameter one.
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
This is the Goebel–Karlovitz lemma, proved in Lemma … below.
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
Finally, weak compactness of the unit ball of $\overline{\operatorname{span}}(K-K)$ gives one vector detected along an infinite branch, while the same functionals tend pointwise to zero on that space.
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text
For any pairwise commuting family $\mathcal S$ of nonexpansive selfmaps of $C$ , the common fixed set $\operatorname{Fix}(\mathcal S) =\{x\in C:T(x)=x\text{ for every }T\in\mathcal S\}$ is nonempty and is a nonexpansive retract of $C$ . That is, there is a nonexpansive map $R:C\to\operatorname{Fix}(\mathcal S)$ that is the identity on $\operatorname{Fix}(\mathcal S)$ .
Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces Back to text

Other sources

openai/math, Lean scope note for family 328 every nonexpansive self-map of a nonempty closed bounded convex subset of a real reflexive Banach space has a fixed point in the original norm
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

323Independence of the separable quotient problemFunctional analysis
327Markov type characterizes superreflexivityFunctional analysis
329A counterexample to metric-entropy dualityFunctional analysis
326The cotype–cotype conjecture under the approximation propertyFunctional analysis
330A uniformly discrete counterexample to bounded approximation in Lipschitz-free spacesFunctional analysis

Browse Functional analysis Open since the 1960s Lean-checked results Landmark results