Code, demos, benchmarks, and systems that make the research inspectable.
I want the portfolio to show more than claims. Each artifact below is a working surface: a library, benchmark, deployed assistant, evaluation workflow, or research pipeline that carries the larger thesis from idea to evidence.
Formal substrates
Lean, proof libraries, and agent-facing mathematical memory.
2 artifacts
Evaluation artifacts
Benchmarks, lineages, solver traces, and verification contracts.
1 artifacts
Fielded knowledge systems
RAG products and assistants that test the substrate pattern with real users.
2 artifacts
Applied AI pipelines
Forecasting, medical, and education systems shaped by domain friction.
2 artifacts
Lean, proof libraries, and agent-facing mathematical memory.
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.
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.
Benchmarks, lineages, solver traces, and verification contracts.
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.
RAG products and assistants that test the substrate pattern with real users.
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.
Forecasting, medical, and education systems shaped by domain friction.
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.
MekaNet / medical AI pipelines
Medical image pipelines where scale, validation, and clinical reporting shape the AI system.
Whole-slide-image and cell-analysis pipelines for pathology tasks such as tiny-object detection and cellularity assessment.