What was already known
Problem 155 asked whether this local distance condition forces a global isometry. Mori had proved it for a separable source space; Basso proved a positive result under a stronger local-isometry condition. Neither covered the unrestricted case.
AI involvement
Ishiki credits OpenAI Codex with suggesting the counterexample construction and helping develop the one-point extension and transfinite recursion. Ishiki selected the problem, verified and revised the argument, and authored the paper.
The author directly credits Codex with suggesting the counterexample and helping develop the essential extension/recursion; the human author checked and revised the complete proof.
Importance
Settles a longstanding local-to-global question for Banach-space isometries in the unrestricted case.
Limitations
Ishiki reports checking and revising the original proof. A later Lean development reports a proof of the same existential conclusion using a different envelope construction, so it does not check the original proof line by line. No independent human referee or rebuild of the Lean project is documented here.
Technical verification
Ishiki explicitly reports verifying the arguments of the original construction, and the later source reports a Lean theorem with the same existential conclusion and standard axioms. Lean uses a different envelope, so it checks the theorem rather than every internal step of the original proof.
Formal checking
Project reports compiled theorem and standard-axiom audit for the same conclusion using a different envelope.
- Checker
- Lean 4 kernel and project axiom audit, as reported by the project
- Scope
- Existence of a Banach-space map preserving distances on radius-1/4 balls but not globally isometric
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Ishiki expressly says he understands all proofs and explains the bent seed, protected extension, retraction invariant and transfinite scheduling in §§1–5.
Correction and publication history
Original AI credit, author's proof check, prior baseline and later formal theorem scope reviewed.
Read this published revision