I build reinforcement-learning environments and tools for formal reasoning.
I'm a 20-year-old self-taught independent AI researcher working on reinforcement-learning environments, constrained generation, theorem-proving systems, and executable verification. I left college to focus on independent research.
Current work
native-verify
active project
An execution-as-verification RL environment where model outputs are sanitized,
tested, compiled into Lean, and rewarded from execution.
Grammars for AI-Generated Proof Steps
research + code
Lean tactic grammars, corpus extraction, mutation testing, and experiments
in grammar-constrained generation.
Selected writing
How a Grammar Changes AI-Generated Mathematical Proof Steps
formal methods · 21 min
How grammar masking changes Lean tactic outputs: a reproducible Qwen comparison, token-level mechanics, exact denominators, latency, and exploratory Goedel runs.
Building a Grammar for AI-Generated Mathematical Proof Steps
formal methods · 17 min
A worked study of Lean tactic grammars: explicit syntax, permissive fallbacks, corpus extraction, mutation tests, and a reduced-grammar ablation.
Taming Incidental Polysemanticity in Toy Models
interpretability · 25 min
A toy-model study of how training configurations affect feature-entanglement
proxies measured with sparse autoencoders.
Earlier research
Surgical Knowledge Rewrite in Compact LLMs: An 'Unlearn-then-Learn' Strategy with ((IA)³)
preprint
An exploratory two-stage (IA)³ pipeline that localizes a target association,
suppresses it, and then learns a replacement in Phi-3-mini.
Targeted Lexical Injection: Unlocking Latent Cross-Lingual Alignment in Lugha-Llama via Early-Layer LoRA Fine-Tuning
preprint
An early-layer LoRA study of Swahili–English lexical alignment in
Lugha-Llama, evaluated on trained and unseen word pairs.