I am an AI fellow in the Center for AI and Natural Sciences (CAINS) at Korea Institute for Advanced Study (KIAS).
Previously, I was a research scientist (postdoctoral researcher) in the Group of Inverse Problems and Mathematical Imaging (IPMI) at Johann Radon Institute for Computational and Applied Mathematics (RICAM), Austrian Academy of Science (ÖAW), working with Otmar Scherzer. I obtained my Ph.D at Yonsei University under the supervision of Youngmi Hur.
Address: 85 Hoegi-ro, Dongdaemun-gu, Seoul 02455, Republic of Korea
Email: hlim@kias.re.kr (My previous RICAM oeaw email will be deactivated).
Curriculum Vitae (last updated in July 2026)
Research Interests:
Mathematical Theory of Neural Networks
Formal Mathematics; LLM-Based Formalization and Theorem Proving
Approximation Theory, especially Wavelet Frame Theory
Abstract Harmonic Analysis -- Unitary Representation Theory on Locally Compact Groups
Publication Lists:
Read First, Formalize Later: Source-Grounded Theory-Scale Autoformalization (with collaborators) (submitted)
Neural Network Approximation of Solutions to Fractional Parabolic Partial Differential Equations (with J.-H. Choi, J. Seo, Y.-J. Sim, and C. Song) (submitted) (preprint in arXiv)
Partial Soundness: Natural Language Theorem Proving with Machine-Checked Logical Structure (with collaborators) (submitted)
Information Propagation via Sign-Flip Dynamics (with collaborators) (submitted)
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems (with collaborators) (submitted) (preprint in arXiv)
Formalization of Infinite Oriented Matroids (with collaborators) (submitted)
New Tight Wavelet Frame Constructions Sharing Responsibility (with Y. Hur) (submitted) (preprint in arXiv)
Mechanically Orchestrated LLM Sub-Agents for Theorem Proving in Lean 4 (with B.-H. Hwang, J. La, and C.-H. Lee), the 3rd AI for Math Workshop, International Conference on Machine Learning (ICML) 2026 (preprint)
Provable Wavelet-Based Neural Approximation (with Y. Hur and M. Lim), Applied Mathematics and Computation, Volume 514, 2026, 129821. (preprint) (preprint in arXiv)
Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques (with S. Han, T. Hur, Y. Hur, K. S. Lee, and M. Lee), Intelligent Computing: Proceedings of the 2025 Computing Conference, Volume 2, pp. 205-222. Part of the Lecture Notes in Networks and Systems book series (LNNS, volume 1424). Springer. (preprint) (preprint in arXiv and codes)
Wavelet Series Expansion in Hardy Spaces with Approximate Duals (with Y. Hur), Analysis Mathematica, Vol. 50, No. 2, 2024, pp. 563-595. (preprint) (preprint in arXiv)
Understanding the Scattering Transform using Univariate Signals (with Y. Hur), Proceedings of 11th International Congress on Image and Signal Processing, BioMedical Engineering and Informatics (CISP-BMEI), 2018, pp. 1-7. (preprint)
Work in Progress
WIREN: Spectral Bias Reduction using Gabor Wavelet (with Y. Hur and M. Lim)
Deng-Han Wavelet Frames on Euclidean Spaces with the Scaling Relation (with S. Han and Y. Hur)
Wavelet Frames over p-adic Numbers (with W. Lee)
Ph.D. Mathematics in Yonsei University, 2024
B.S. Mathematics in Konkuk University, 2017