Interactive 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.

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.