I build AI for formal methods.
Researcher in Nairobi, Kenya working at the intersection of LLMs and theorem proving: tactic grammars, constrained decoding, and the measurement of model outputs and proof-assistant interaction. Background in mechanistic interpretability — I like knowing what the model is doing on the inside.
Writing
2026
How a Grammar Changes AI-Generated Mathematical Proof Steps
Aug 22 · revised Sep 5
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
Aug 22 · revised Sep 5
A worked study of Lean tactic grammars: explicit syntax, permissive fallbacks, corpus extraction, mutation tests, and a reduced-grammar ablation.
2025
Taming Incidental Polysemanticity in Toy Models
Oct 19
Do training choices shape feature entanglement? SAE-based measurements across
regularization, init, activations and noise — L2 beat L1 by 17.9%.
Research
Surgical Knowledge Rewrite in Compact LLMs: An 'Unlearn-then-Learn' Strategy with ((IA)³)
arXiv · Aug 2025
Locate a fact's circuit first, then unlearn-then-learn with (IA)³: 98.5% edit
accuracy on Phi-3-mini while control-fact retention more than triples versus
direct fine-tuning (72% vs ~20%) — and suppressed knowledge stays latent, not gone.
Targeted Lexical Injection: Unlocking Latent Cross-Lingual Alignment in Lugha-Llama via Early-Layer LoRA Fine-Tuning
arXiv · Jun 2025
Swahili–English alignment was already near-perfect inside Lugha-Llama at Layer 2
(cosine 0.99998) — just lost by the output layer (0.32). Early-layer contrastive
LoRA brings it back: +28%, generalizing to unseen words.
Now
Developing reproducible studies of Lean tactic grammars and constrained generation, with future work on proof-state feedback documented separately.