Always a fixed point?
An AI preprint claims a positive answer to Kirk’s fixed-point problem for reflexive spaces
Covers result 328 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
3:50. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
A map is nonexpansive if it never pulls two points farther apart. Rotate a square by a quarter turn: plain iteration cycles forever, but averaging each step with where you were spirals in to the fixed centre. Whether a map counts as nonexpansive depends on the norm: our computer finds one map of the unit square that never stretches distances in the max norm but doubles some in the sum norm.
In 1965 Browder, Göhde and Kirk showed that every nonexpansive map of a closed, bounded, convex set into itself has a fixed point if the space is uniformly convex, or is reflexive and the set has normal structure. In 1981 Alspach found a map on a weakly compact convex set in L₁ with no fixed point at all; our computer checks, on 300 random pairs, that it preserves distances exactly, and that the first 8 points of one orbit are all at distance 1 from each other. Kirk asked whether every reflexive space has the property, in lectures in 1995, and a paper posted on October 7, 2026, still called it open.
Result 328 is one OpenAI paper, 19 pages, dated September 24 and made public October 6, 2026. It claims that every nonexpansive selfmap of a nonempty, closed, bounded, convex subset of a real reflexive Banach space has a fixed point, in the space’s own norm, with no extra geometric hypothesis.
What it doesn’t claim
Not claimed: the converse, that every space with the property is reflexive, which is false, since a renormed ℓ₁ has it; anything about non-reflexive spaces; or a way to find the fixed point. An earlier claimed proof, from 2019, was reviewed as quite doubtful; the paper cites it and says its argument is different.
Where it stands
- Posted as a preprint
- OpenAI, 19 pages, dated September 24, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- The main theorem (docs)
Last checked October 19, 2026. The paper is unrefereed and unchanged since release. Lean formalizes the main theorem, in 86 files and about 11,500 lines, not run by us; the corollary is not formalized. Three outside projects re-ran it and it was accepted. No specialist has publicly assessed the proof; one mathematician’s site posted a ChatGPT-drafted reconstruction that claims no independent verification. OSVerify has not reviewed it.
How the proof goes
- A minimal set, and points on its rim. Suppose a map has no fixed point. Shrink to a minimal invariant set of diameter 1. There, approximate fixed points drift to the rim, ever closer to distance 1 from every point of the set. Averaged steps called resolvents, each the fixed point of a contraction, give approximate fixed points with error at most 1/n; on the c₀ shift our computer finds exactly 1/n, while no true fixed point exists. A compactness argument then produces an anchor point that is approached by averages of ever better approximate fixed points.
- A tree, and a contradiction. From the anchor the proof grows an infinite tree of approximate fixed points, with a functional at each node that sees its point far from everything predicted. Switching the leaves one by one gives, at each depth, a vector that the functionals along one path detect. Reflexivity, through the weak compactness of the whole unit ball, turns these into one vector for an infinite branch, while those functionals tend to zero: a contradiction. This last step has no counterpart for Alspach’s map: there the set is weakly compact, but the whole ball is not. Our computer checks the tree bookkeeping on 200 random trees.
The numbers in the video
- Ours: a quarter turn of the square; plain iteration cycles, while averaging each step with the previous point spirals in to the centre.
- Ours: one map of the unit square has stretch factor 1 in the max norm and 2 in the sum norm.
- Ours, exact: Alspach’s L₁ map preserves distances on 300 random pairs, and the first 8 points of the orbit of 1 are pairwise at distance 1.
- Ours: on the c₀ shift, the paper’s resolvents have error exactly 1/n; the paper’s tree bookkeeping holds on 200 random trees.
- Lean: 86 files and 11,540 lines in the import closure (counted by us; not run by us).
Read the source
- Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces (PDF), 19 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 328.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
A map is nonexpansive if it never pulls two points farther apart. Rotate a square by a quarter turn: plain iteration cycles forever, but averaging each step with where you were spirals in to the fixed centre. Whether a map counts as nonexpansive depends on the norm: our computer finds one map of the unit square that never stretches distances in the max norm but doubles some in the sum norm. In 1965 Browder, Göhde and Kirk showed that every nonexpansive map of a closed, bounded, convex set into itself has a fixed point if the space is uniformly convex, or is reflexive and the set has normal structure. In 1981 Alspach found a map on a weakly compact convex set in L₁ with no fixed point at all; our computer checks, on 300 random pairs, that it preserves distances exactly, and that the first 8 points of one orbit are all at distance 1 from each other. Kirk asked whether every reflexive space has the property, in lectures in 1995, and a paper posted on October 7, 2026, still called it open.
1:06The claim
Result 328 is one OpenAI paper, 19 pages, dated September 24 and made public October 6, 2026. It claims that every nonexpansive selfmap of a nonempty, closed, bounded, convex subset of a real reflexive Banach space has a fixed point, in the space’s own norm, with no extra geometric hypothesis. Not claimed: the converse, that every space with the property is reflexive, which is false, since a renormed ℓ₁ has it; anything about non-reflexive spaces; or a way to find the fixed point. An earlier claimed proof, from 2019, was reviewed as quite doubtful; the paper cites it and says its argument is different.
1:52How the proof goes
Suppose a map has no fixed point. Shrink to a minimal invariant set of diameter 1. There, approximate fixed points drift to the rim, ever closer to distance 1 from every point of the set. Averaged steps called resolvents, each the fixed point of a contraction, give approximate fixed points with error at most 1/n; on the c₀ shift our computer finds exactly 1/n, while no true fixed point exists. A compactness argument then produces an anchor point that is approached by averages of ever better approximate fixed points. From the anchor the proof grows an infinite tree of approximate fixed points, with a functional at each node that sees its point far from everything predicted. Switching the leaves one by one gives, at each depth, a vector that the functionals along one path detect. Reflexivity, through the weak compactness of the whole unit ball, turns these into one vector for an infinite branch, while those functionals tend to zero: a contradiction. This last step has no counterpart for Alspach’s map: there the set is weakly compact, but the whole ball is not. Our computer checks the tree bookkeeping on 200 random trees.
3:06Where it stands
The paper is unrefereed and unchanged since release. Lean formalizes the main theorem, in 86 files and about 11,500 lines, not run by us; the corollary is not formalized. Three outside projects re-ran it and it was accepted. No specialist has publicly assessed the proof; one mathematician’s site posted a ChatGPT-drafted reconstruction that claims no independent verification. If it holds, every nonexpansive map of a closed, bounded, convex set in a reflexive Banach space has a fixed point, answering Kirk’s question for the space’s original norm, the half that was still open.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.