主持人：周国栋 教授

报告简介：
In this talk, I will introduce the formalization of the fundation of non-Archimedean functional analysis in Lean 4 with Mathlib. This work includes the equivalent definitions of spherical completeness, their basic properties, examples and non-examples such as the field Cp of p-adic complex numbers. As application, we formalize the Birkhoff-James orthogonality, Hahn-Banach extension theorem and the spherical completion for non-Archimedean Banach spaces.

主讲人简介：
袁轶君，现为西湖大学理论科学研究院博士后。2018年本科毕业于华东师范大学数学科学学院，获数学与应用数学专业本科学位。2021年硕士毕业于复旦大学数学科学学院，获基础数学硕士学位。2025年博士毕业于清华大学丘成桐数学科学中心，获基础数学博士学位。主要研究方向为p-进Galois表示，p-进超越数论及算术几何的形式化。