Kirk's fixed point problem for reflexive spaces
From OpenAI Aftermath
Kirk's fixed point problem for reflexive spaces asks whether every nonexpansive selfmap of a nonempty closed bounded convex subset of a reflexive Banach space has a fixed point, with nonexpansiveness measured in the given norm. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 24 September 2026, claims a positive answer. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Browder and Göhde proved the fixed point property for uniformly convex spaces, and Kirk proved it for closed bounded convex sets with normal structure in reflexive spaces. Karlovitz proved the property for a norm on ℓ2 without normal structure, so normal structure is not necessary.
- Maurey proved the property for reflexive subspaces of L1, Lin proved the weak fixed point property for spaces with a 1-unconditional basis, and García-Falset, Llorens-Fuster and Mazcuñán-Navarro proved it for uniformly nonsquare spaces.
- Alspach constructed a weakly compact convex subset of L1[0, 1] with a fixed-point-free nonexpansive selfmap, so weak compactness of the domain alone is not enough, and Domínguez Benavides proved that every reflexive space has an equivalent norm with the fixed point property. The manuscript notes an earlier proposed proof by Hanebaly and a recent account by Nourouzi recording the question as unresolved.
The original result
- Claim. Theorem 1.1 of Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces states that if X is a real reflexive Banach space and C is a nonempty, norm-closed, bounded, convex subset of X, then every map F from C to itself with ‖F(a) − F(b)‖ ≤ ‖a − b‖ has a fixed point. The manuscript states that this resolves the reflexive-space fixed point problem for the given norm.
- Further claims. A corollary, through Bruck's theorem, states that the common fixed point set of any commuting family of nonexpansive selfmaps of such a set is nonempty and is a nonexpansive retract of the set.
- Method, as described: the minimal invariant set method reduces a counterexample to a separable weakly compact convex set of diameter one, on which approximate fixed points are asymptotically diametral by the Goebel–Karlovitz lemma. A compact semigroup of nonexpansive maps provides an anchor point, approximate fixed point images label an ordered tree, and replacing blocks of leaves from right to left gives telescoping root outputs. Weighted estimates produce one vector detected by all functionals along a branch, and weak compactness of the unit ball of the relevant span gives the contradiction.
- Source (openai/math repository, commit
7ef5c0c): Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces, dated 24 September 2026. - Formalization, as described by the repository. The scope note lean/docs/328.md states that the formalization proves the fixed point theorem in the original norm for every real reflexive Banach space, including the zero space and nonseparable spaces, without uniform convexity, normal structure or weak continuity, and links the comparator statement ReflexiveFixedPoints.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 28 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | Nonexpansive fixed points in reflexive spaces, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains the claimed answer to Kirk's question: norm and weak compactness, approximate fixed points, minimal invariant sets and diametral behavior, one functional detecting a compact family, the adaptive tree argument, and the consequence for commuting maps. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | Formal Conjectures pull request #6989 | Statement (proposed) | Proposes adding Theorem 1.1 of the manuscript, pinned at commit adc7f12, to the repository, with reflexivity stated as surjectivity of the canonical map into the bidual. The description states that the statement matches the Comparator challenge after unfolding the definition, that the external proof was not built, so no formal-proof attribute is added, and that the commuting-family consequence is not included. |
Open pull request, approved by a reviewer on 10 October 2026 and not merged when checked on 28 October 2026; the description discloses AI assistance. |
| 2026-10-09 | Fixed points of nonexpansive maps, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public) | Reading (exposition) | Four lessons: minimal invariant sets and diametral sequences; resolvents and an anchor point; a tree of predicted outputs; and Kirk's problem. | The lessons state that they were written by Claude Opus 5.5 (Anthropic) in October 2026 and self-checked by the writing AI; the course lists its status as author self-checked. |
| 2026-10-16 | Reading OpenAI's fixed-point argument in reflexive Banach spaces: Ordered trees, finite switching, and an RNP extension, an expository note of Exact Mathematics with AI, version 1 | Extension (exposition) | Reconstructs the manuscript's anchor, ordered tree and finite-switching argument in 35 pages, and records the same mechanism for Banach spaces with the Radon–Nikodým property: every nonexpansive selfmap of a nonempty weakly compact convex subset of such a space has a fixed point, with a final step that uses small slices instead of weak compactness of the unit ball. The note derives the reflexive theorem and the commuting-family consequence from this statement. | Expository note, version 1, published 16 October 2026; the site names Ryotaro Tanaka as responsible for publication and states that the note was drafted and revised using ChatGPT. The note makes no priority claim for the extension to the Radon–Nikodým property and claims no peer review, independent verification or Lean verification. Checked at the source 28 October 2026. |
| 2026-10-19 | AI Proved What?, episode 328 Always a fixed point?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of the claim 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, answering Kirk's question. The episode states that the converse, anything about non-reflexive spaces and a way to find the fixed point are not claimed, and that an earlier claimed proof from 2019 is cited by the paper, which says its argument is different. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 19 pages, dated September 24, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the main theorem. The page also states that the Lean formalization of the main theorem has 86 files and about 11,500 lines, not run by the site, that the corollary is not formalized, that three outside projects re-ran the check and accepted it, that no specialist has publicly assessed the proof, that one site posted a ChatGPT-drafted reconstruction claiming no independent verification, and that OSVerify has not reviewed the paper. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
