主讲人：袁轶君 博士（西湖大学）
主持人：周国栋 教授
时 间：2026年4月9日 10:00
地 点：数学楼102报告厅
报告内容介绍：
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-进超越数论及算术几何的形式化。