{"id":"arxiv/2601.21734","url":"https://arxiv.org/abs/2601.21734","tags":["math.NT","cs.LO","math.FA"],"score":0,"title":"Formalization of non-Archimedean functional analysis 1: spherically complete spaces","domain":"math.NT","source":"arxiv","authors":["Yijun Yuan"],"reviews":0,"subject":"math.NT","summary":"In this article, we present a formalization of spherically complete spaces, a fundamental notion in non-Archimedean functional analysis, using the Lean theorem prover (v4.31.0), building over Mathlib. This work includes the equivalent definitions of spherically complete spaces, their basic properties, examples and non-examples such as the field $\\mathbf{C}_p$ of $p$-adic complex numbers. As applications, we formalize the notion of Birkhoff-James orthogonality, the Hahn-Banach extension theorem and the spherical completion for non-Archimedean Banach spaces. URL of code:…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-01-29","reactions":{}}