Hyojae Lim

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.

Contact Information

Address: 85 Hoegi-ro, Dongdaemun-gu, Seoul 02455, Republic of Korea

Email: hlim@kias.re.kr (My previous RICAM oeaw email will be deactivated).

Research

1. Curriculum Vitae (last updated in September 2026)

2. Research Interests:

   • Mathematical Theory of Neural Networks (Math for AI)

   • Formal Mathematics; LLM-Based Formalization and Theorem Proving (AI for Math)

   • Approximation Theory, especially Wavelet Frame Theory

   • Abstract Harmonic Analysis -- Unitary Representation Theory on Locally Compact Groups

3. Publications

• AI for Mathematics

• Mechanically Orchestrated LLM Sub-Agents for Theorem Proving in Lean 4 (with B.-H. Hwang, J. La, and C.-H. Lee), 3rd AI for Math Workshop at ICML 2026 (published ver.)

• 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. (published ver.) (preprint in arXiv and codes)

3. • Mathematics for AI

     • Information Propagation via Sign-Flip Dynamics (with H. Lee and D. Kwon), accepted at NeurIPS 2026

     • Provable Wavelet-Based Neural Approximation (with Y. Hur and M. Lim), Applied Mathematics and Computation, Volume 514, 2026, 129821. (published ver.) (preprint in arXiv)

   • Harmonic Analysis and Approximation Theory (Analysis)

     • Wavelet Series Expansion in Hardy Spaces with Approximate Duals (with Y. Hur), Analysis Mathematica, Vol. 50, No. 2, 2024, pp. 563-595. (published ver.) (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. (published ver.)

4. Submitted Manuscripts

• [AI for Math] Read First, Formalize Later: Source-Grounded Theory-Scale Autoformalization (with collaborators) 

• [Math for AI] Fractional Parabolic Partial Differential Equations in Anisotropic Spectral Barron Spaces: Regularity and Neural Approximation (with J.-H. Choi, J. Seo, Y.-J. Sim, and C. Song) (preprint in arXiv)

• [AI for Math] Partial Soundness: Natural Language Theorem Proving with Machine-Checked Logical Structure (with collaborators)

• [AI for Math] Lean-GAP: A Dataset of Formalized Graduate Algebra Problems (with collaborators) (preprint in arXiv)

• [AI for Math] Formalization of Infinite Oriented Matroids (with collaborators)

4. • [Analysis] New Tight Wavelet Frame Constructions Sharing Responsibility (with Y. Hur) (preprint in arXiv)

5. Work in Progress

• [Math for AI] WIREN: Spectral Bias Reduction using Gabor Wavelet (with Y. Hur and M. Lim)

• [Analysis] Deng-Han Wavelet Frames on Euclidean Spaces with the Scaling Relation (with S. Han and Y. Hur)

• • [Analysis] Wavelet Frames over p-adic Numbers (with W. Lee)

Education

• Ph.D. Mathematics in Yonsei University, 2024

• B.S. Mathematics in Konkuk University, 2017