nteractive theorem provers (ITPs) are becoming crucial in mathematics, supporting the development of fully verified proofs and mathematically rigorous infrastructure. Their importance comes not only from catching mistakes that humans overlook, but also from enabling large-scale formalization projects that would be impossible to manage manually. In this talk, I will give an accessible overview of formalizing mathematics in Lean4 and outline how its underlying theory and tooling support modern proof development. In advance, I will present several mathematical projects that showcase the strengths of ITPs.

A fundamental problem in low-dimensional topology is to find the minimal genus of embedded surfaces in a 3-manifold or 4-manifold, in a given homology class. Ni and Wu solved a 3-dimensional minimal genus problem for rationally null-homologous knots. In this talk, we will discuss an analogous 4-dimensional minimal genus problem for rationally null-homologous knots. This is a joint work with Zhongtao Wu.

In doing mathematics, we often encounter beautiful identities and proofs, shining like a full moon in the night sky. Some of them have combinatorial flavors. This talk is an introduction to combinatorial proof methods using bijections and weight-preserving-sign-reversing involutions, with examples including Franklin's bijective proof of the Euler pentagonal number theorem, a combinatorial proof of the Cayley-Hamilton theorem, the Robinson-Schensted correspondence and recent combinatorial proofs of some identities involving secant and tangent numbers.

The phase-field (PF) model has been applied to a wide range of problems beyond its traditional scope in materials science. In this study, we reinterpret the Allen–Cahn (AC) equation, the governing equation of the PF model, as a mathematical framework for data classification. We develop an efficient numerical scheme to solve the AC equation with a fidelity term, employing an explicit-type approach based on the convex splitting method to ensure both energy stability and computational efficiency. Comparative experiments with conventional machine learning classifiers, such as support vector machines and artificial neural networks, demonstrate that our approach achieves competitive accuracy at significantly reduced computational cost. Moreover, the proposed PDE-informed framework exhibits superior performance on unbalanced datasets, where traditional classifiers often fail to generalize effectively.

(The is a PhD student reading seminar to be given by Mr. Jaehong Kim.)

A (positive definite and integral) quadratic form $f$ is called irrecoverable (from its subforms) if there is a quadratic form $F$ that represents all proper subforms except for $f$ itself, and such a quadratic form $F$ is called an isolation of $f$. In this talk, we present recent advances on irrecoverable quadratic forms and discuss their possible generalizations.

Khovanov homology is a knot homology theory, introduced by M. Khovanov in 2000 as a categorification of the Jones polynomial. Equivariant versions of Khovanov homology are also known, and they play an important role in understanding the Rasmussen invariant. In this talk, I will present the results established in my joint work with M. Khovanov in September 2025 (arXiv:2509.03785): (i) an order-two symmetry inherent in equivariant Khovanov homology, (ii) the existence of a signed Shumakovitch operator, and (iii) its relationship to the Rasmussen invariant.

We renormalize the Chern-Simons invariant for convex-cocompact hyperbolic 3-manifolds, finding the explicit asymptotics along an equidistance foliation. We prove that the divergent terms are completely expressed in terms of the data from the Weitzenböck geometry of hyperbolic ends and the conformal boundary. For this, it is essential to extend the framework of submanifolds in Riemannian geometry to Riemann-Cartan geometry, which addresses connections with torsion. This procedure naturally introduces a complex-valued geometric quantity consisting of mean curvature and torsion 2-form, which appears in the leading coefficient of the asymptotics. We also obtain several geometric results regarding the complex-valued quantity that generalize classical minimal surface theory.

---

심사위원장: 백형렬, 심사위원: 박진성(KIAS), 김현규(KIAS), 박정환, 최서영.

I will discuss recent progress on the vanishing-viscosity limit of the two-dimensional Navier–Stokes equation. Our approach is Lagrangian and probabilistic: 1. We develop a stochastic counterpart of the DiPerna–Lions theory to construct and control stochastic Lagrangian flows for the viscous dynamics. 2. We also establish a large-deviation principle that quantifies convergence to the Euler dynamics. This talk is based on joint work with Chanwoo Kim, Dohyun Kwon, and Jinsol Seo.