Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces

Formalization

• OpenAI, Nonexpansive fixed points in reflexive Banach spaces: Lean scope notes (lean/docs/328.md, family 328, 6 October 2026 release). The release's scope note says the formalized original-norm fixed-point theorem covers the zero space and nonseparable real reflexive Banach spaces, assumes neither uniform convexity, normal structure nor weak continuity, and links the comparator statement. [AI-generated per source] [family-level]
• OpenAI, ReflexiveFixedPoints.lean (openai/math comparator challenge, 2026-10). The comparator file states exists_fixedPoint_of_canonicallyReflexive for complete real normed spaces with CanonicallyReflexive X; the file gives the statement only, with the proof left as sorry.
• anxkhn, Add nonexpansive fixed points in reflexive Banach spaces (google-deepmind/formal-conjectures issue #6984, 2026-10-08). This issue proposes adding Theorem 1.1 to formal-conjectures as a statement only, with reflexivity expressed as surjectivity of the canonical map into the continuous bidual.
• anxkhn, feat(Paper): add reflexive nonexpansive fixed points (google-deepmind/formal-conjectures PR #6989, opened 2026-10-08, open at time of collection). This PR adds the Lean statement of Theorem 1.1 without a formal_proof attribute; in the review thread (mo271, anxkhn) reviewers discuss whether formal-conjectures should add problems the release reports as solved, and one reviewer approved the statement as matching the manuscript.

Possibly relevant literature (found by the agent, not checked)

• Faruk Alpay and Hamdi Alakkad, On the Fixed Point Property in Reflexive Banach Spaces (arXiv:2509.13121, 2025-09-16). An earlier preprint on the same reflexive-space question that proposes quantitative "diametral ℓ1 pressure" criteria; the paper's survey of prior attempts (Hanebaly, Nourouzi) does not cite it.
• Kazimierz Goebel and W. A. Kirk, Topics in Metric Fixed Point Theory (Cambridge Studies in Advanced Mathematics 28, 1990). Standard monograph treatment of the minimal invariant set reduction and the Goebel–Karlovitz lemma, which the paper's argument starts from (Introduction, "The argument").

Digests and expositions

• Exact Mathematics with AI (publication responsibility: Ryotaro Tanaka), Reading OpenAI’s fixed-point argument in reflexive Banach spaces: Ordered trees, finite switching, and an RNP extension (Expository Note, version 1, 16 October 2026). This 35-page ChatGPT-drafted note reconstructs the paper’s ordered-tree and finite-switching argument and states an extension to the weak fixed point property for Banach spaces with the Radon–Nikodým property, without claiming independent verification or priority for the extension. [AI-generated per source]
• Open Mathematics Courses, Fixed points of nonexpansive maps (four-lesson online course, undated). Written and self-checked by Claude Opus 5.5, the course develops the paper’s minimal invariant set reduction, resolvent anchor, predicted-output tree, and switching argument through proofs and exercises, with independent review described as incomplete. [AI-generated per source]