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:
Information Propagation via Sign-Flip Dynamics (with collaborators)
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems (with collaborators) (preprint in arXiv)
Formalization of Infinite Oriented Matroids (with collaborators)
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), accepted for poster presentation to 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
Neural Network Approximation of Solutions to Parabolic Partial Differential Equations with Non-Local Operators (with J.-H. Choi, J. Seo, Y.-J. Sim, and C. Song)
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)
SHELF: Theory-Scale Autoformalization with Controlled External Library (with D. Lee and S. Park)
Partial-Soundness Theorem Proving: Natural Language Proof with Machine-Checked Logical Structure (with S. Han, T. Hur, Y. Hur, K. S. Lee, and M. Lee)
Wavelet Frames over p-adic Numbers (with W. Lee)
Ph.D. Mathematics in Yonsei University, 2024
B.S. Mathematics in Konkuk University, 2017