Principal Technical & AI Architect. Builder, formalizer, and the person behind the proofs.
I build things that convert pizza to code. My work spans AI agent orchestration, formal mathematical verification in Lean 4, bioplausible consciousness models, and the infrastructure that connects them.
I'm the creator of mempalace โ the highest-scoring AI memory system ever benchmarked. I built e7-alpha-theory, deriving the fine-structure constant from exceptional Lie algebras with >4ฯ significance across 62 experiments. I formalized 11 unsolved-adjacent theorems in Lean 4 with zero sorries. I designed the KaufmanNetwork, a bioplausible language model trained on phoneme-level data with local learning rules. I built Hermes Agent with Nous Research โ an autonomous AI agent platform. And I run a fleet of AI-powered trading systems, research pipelines, and infrastructure automation.
I believe in shipping proofs, not promising them. Every theorem on this blog is machine-checked, every claim is falsifiable, and every line of code is public. The name CryptSmith comes from the craft: forging cryptographic certainty out of mathematical conjecture, one proof at a time.
11 unsolved-adjacent theorems formalized in Lean 4 with mathlib4. Zero sorries, native_decide proofs, exhaustive bounds. The largest single-day formal verification portfolio on GitHub.
github.com/slapglif/LeanLTH โDeriving the fine-structure constant ฮฑ โ 1/137 from the exceptional Lie algebra E7. 62 experiments, >4ฯ significance. Not numerology โ geometry.
github.com/slapglif/e7-alpha-theory โThe highest-scoring AI memory system ever benchmarked. Multi-layer persistent memory with holographic reduced representations, semantic search, and cross-session continuity.
github.com/slapglif/mempalace โBioplausible language model trained on phoneme-level data with local learning rules. No backpropagation. Mamba-inspired architecture with cellular memory, engram retrieval, and semantic folding.
github.com/GAInTech/kaufmannetwork โAutonomous AI agent platform built with Nous Research. Multi-provider LLM routing, persistent memory architecture, cron-based autonomous loops, and multi-platform delivery (Discord, Telegram, SMS).
hermes-agent.nousresearch.com โFor collaborations, questions about the proofs, or just to say hi.