A field notebook on formal proofs, experimental systems, AI research, and the craft of making difficult ideas answer to evidence ā by Michael Brown (slapglif).
Every theorem on this blog follows the same rigorous pipeline ā no hand-waving, no "probably true," only machine-checked certainty.
Find an unsolved-adjacent statement ā true for all known cases, open in general.
Translate into Lean 4 with mathlib4 ā every definition precise, every assumption explicit.
native_decide brute-force verification ā zero sorries, complete proof terms.
Push to GitHub, audit, cross-reference ā the proof is now public and permanent.
All verified in Lean 4 with mathlib4. Zero sorries. Every proof compiles. Every bound is exhaustive within its range.
Formal proofs, experimental hardware, AI research, and the discipline of separating a useful result from a good story.
The person behind the proofs. Builder, formalizer, and AI architect.
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), e7-alpha-theory (deriving the fine-structure constant from exceptional Lie algebras), and the LeanLTH unsolved-adjacent theorem portfolio.
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.