In this talk, I will introduce the formalization of the foundations of non-Archimedean functional analysis in Lean 4. This work includes the basic properties of spherical completeness, examples and non-examples such as the field Cp of p-adic complex numbers. As applications, we formalize Hahn-Banach extension theorem and the spherical completion for non-Archimedean Banach spaces. If time permits, I will also talk about how formalization strengthen our trust on mathematical proofs in the era of AI.
