doxtor6
AI × Code × Games
I work at the intersection of large language models, autonomous agents, and formal mathematics. My focus areas include LLM theory, agentic frameworks for autoformalization, and AI-driven gaming & VTubing systems.
I'm building MerLean, an agentic framework for autoformalization in quantum computation using Lean 4, and exploring the theoretical foundations of memory and consciousness in large language models.
I also design advanced AI agents with persistent memory and autonomous decision-making for dynamic game content and virtual worlds.
News
Research
My work spans three areas at the intersection of AI theory, formal methods, and interactive systems:
LLM Theory & Consciousness
Investigating the theoretical foundations of large language models — memory architectures, emergent abilities, and the duality between LLMs and cognitive memory theory.
Autoformalization & Lean 4
Building agentic frameworks that bridge natural-language mathematics and formal proof assistants, with applications in quantum computation.
AI Agents & Gaming
Designing autonomous agents with persistent memory and decision-making for dynamic game content, VTubing, and interactive virtual worlds.
Featured Project
MerLean
An agentic framework for autoformalization in quantum computation. MerLean uses LLM agents to translate informal mathematical statements into formally verified Lean 4 proofs, focusing on quantum information theory.
Publications
Projects
MerLean — An agentic framework for autoformalization in quantum computation. MerLean translates informal mathematical statements into formally verified Lean 4 proofs, bridging the gap between natural-language math and machine-checked reasoning.
Memory & Consciousness in LLMs — A theoretical investigation into the duality between large language models and Tulving's memory theory. We relate synergistic ecphory to emergent abilities in LLMs and propose that consciousness may itself be an emergent phenomenon.
Gaming & VTubing AI — Designing autonomous agents with persistent memory, long-horizon planning, and real-time decision-making for dynamic game content and interactive virtual worlds.