Organizers: Heng Du(YMSC), Shanwen Wang(RUC)

Venue: C548, Shuangqing Complex Building A

Date: April 16, 2026

Zoom Meeting ID: 892 226 4912

Passcode: YMSC

Registration For the RUC-YMSC Workshop on Formalized Mathematics

https://docs.qq.com/form/page/DRXNUTU5WVUdHSkJU

Time: 10:00 - 11:00   Speaker: David Loeffler (UniDistance Suisse)

Title: Formalizing modular forms

Abstract: The theory of modular forms is a natural target for formalizing with proof assistants, both because of its inherent interest, and because its very wide prerequisites make it a good test of the available libraries. I will report on the progress so far in formalizing modular form theory in Lean, and explain how the formalization effort has led to some interesting new perspectives in "informal" mathematics along the way. (This is joint work with numerous authors, especially Chris Birkbeck.)

Time: 11:15 - 12:15   Speaker: Yijun Yuan (Westlake University)

Title: Formalization of non-Archimedean functional analysis

Abstract: In this talk, I will introduce the formalization of the foundation 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 an application, we formalize the Birkhoff-James orthogonality, Hahn-Banach extension theorem, and the spherical completion for non-Archimedean Banach spaces.