I turn domain knowledge into systems that agents can use.
I build AI systems that turn domain knowledge into formal, searchable, and testable artifacts: Lean libraries for coding theory, auditable math benchmarks, RAG products, forecasting pipelines, and research memory for agents.
the working pattern
domain knowledge
papers, logs, textbooks, PDFs, datasets
structured substrate
Lean, graphs, vector memory, MCP, schemas
agent interface
retrieval, prover, evaluator, product workflow
artifact
paper, benchmark, deployed system, public tool
The prototype usually starts ugly.
A notebook. A pile of PDFs. A Lean theorem that will not compile. A dataset with missing values. A product log nobody wants to clean. If the idea survives that first mess, I try to turn it into something searchable, testable, and shareable.
Formalized mathematical AI
Coding theory, self-dual codes, Lean/Mathlib, and MCP-style memory for mathematical agents.
Auditable evaluation
EntropyMath and EntropyMaLean treat benchmarks as traceable processes, not frozen files.
Agent-readable knowledge
I keep asking what shape a domain must take before an agent, prover, or evaluator can use it.
Deployed AI systems
RAG chatbots, forecasting pipelines, medical AI tools, and education products keep the work grounded.
What I am sharpening now.
I keep a wide workshop, but the public portfolio should make the center of gravity clear: formalized mathematical AI, auditable evaluation, and applied systems that prove the substrate works.
Formalized Mathematical AI
CodingTheoryLib, Lean, MCP-style memory, and the 2026 KIIS LLM-Lean award thread are the spine of my long-term research direction.
target artifact
A reusable coding-theory and math-solving substrate that theorem-proving agents can search, inspect, falsify, and extend.
Auditable benchmark evolution
EntropyMath and EntropyMaLean connect generated math problems to solver traces, verifier contracts, and revision-ready evidence.
target artifact
Benchmark lineages that can be audited rather than treated as static download files.
Applied AI systems with real users
SOGAMBOT, MindBuddhi, water-level forecasting, and medical AI keep the research grounded in messy real-world data and users.
target artifact
Deployed assistants, forecasting workflows, and domain-specific pipelines with source-grounded outputs.
Papers are artifacts too.
I want the paper, the code, the benchmark, and the deployed system to point at the same underlying substrate whenever possible.
Proposal of an LLM-Lean Approach and Architecture for Automated Mathematical Problem Solving
Youngjik Lee, Jon-Lark Kim, Woo-Seok Jeong, Beom-Soo Kim, Jae-Hyun Baek
2026 KIIS Spring Conference — Best Paper Award
A closed-agent architecture for mathematical problem solving that compares a Single solver structure with a Dual structure where a falsifier participates in the reasoning loop, emphasizing token/compute efficiency and final solving performance.
Performance Improvement of LLMs for Regulatory Document Understanding based on Modified RAG Approach
Jae-Hyun Baek, Jon-Lark Kim
JKIIS
A modified retrieval augmented generation framework for regulatory documents. This is one of the applied roots of my current interest in turning domain documents into agent-readable memory.
Water Level Forecasting in the Gamcheon River, Korea, Using TimeGPT
Jon-Lark Kim, Jae-Hyun Baek, Keon-Hwi Kim, Tae Hyo Baek, Chang-Lae Jang
International Journal of Fuzzy Logic and Intelligent Systems
A study of foundation-model forecasting for river water levels. We compare TimeGPT with classical and linear baselines under rolling-origin evaluation on the Gamcheon River setting.
Hybrid Multimodal GenAI for Solving Math Problems Containing Various Figures
Sangsoo Lee, Jae-Hyun Baek, Jon-Lark Kim
Accepted manuscript
A hybrid pipeline combining visual retrieval and LLM reasoning for diagram-heavy mathematical problems, especially cases where OCR-only methods miss the actual structure of the figure.
A map of working artifacts.
The surface changes from theorem proving to medical AI to RAG products. The maker habit is the same: find the hidden structure, make it computable, and ship a usable artifact.
CodingTheoryLib / CodingTheoryLib-MCP
Formal coding-theory knowledge shaped into a reusable substrate for theorem-proving agents.
A formalized coding-theory substrate: Lean definitions, proof work, graph memory, and MCP-style access for agents.
EntropyMath / EntropyMaG / EntropyMaLean
Math benchmarks treated as auditable processes rather than static downloads.
A family of systems for evolving math problems with lineage, solver traces, and verification hooks instead of treating benchmarks as frozen files.
SolEvolve
An agentic search loop for proposing, mutating, testing, and preserving mathematical candidates.
An LLM-guided evolutionary discovery system for algorithmic and mathematical search, developed around coding-theory constructions.
SOGAMBOT
A deployed university assistant built from messy institutional documents and retrieval workflows.
A university RAG chatbot that turns scattered Sogang documents and administrative knowledge into a searchable assistant.
MindBuddhi
A source-grounded Buddhist/meditation assistant that turns texts into counseling-oriented interactions.
A Buddhist and meditation knowledge assistant built around source-grounded answers, counseling flows, and shareable artifacts.
Water-level forecasting pipeline
A real-world forecasting pipeline where event timing and hydrological context matter as much as aggregate error.
A hydrological forecasting workflow around TimeGPT, classical baselines, rainfall features, and rolling-origin evaluation.