Become a sponsor to Nelson Spence
I'm Nelson. I spent seven years in behavioral health research - peer support, workforce systems, publishing on why 81% job satisfaction and 42% intent to leave can exist in the same workforce at the same time. I learned how intelligent agents break when you force them to perform coherence without giving them a map.
Then I noticed AI systems break the same way.
Now I formalize theorems in Lean 4 that prove anomaly detection actually works. I write about the structural parallels between AI hallucination and employee burnout. I filed a NIST RFI on AI agent security that got picked up as a wire story. I disclosed a CVSS 9.1 to OpenHands and a watering-hole attack vector to Anthropic. I publish a newsletter called The Weave that connects threads across domains nobody thinks belong together - and they keep being right.
The infrastructure lives at @Project-Navi. Sponsor that if you depend on the tools.
Sponsor me if you want the person who connects the threads to keep pulling them. The cross-domain pattern recognition. The writing. The formal verification research at midnight. The parts that don't fit in a repo description but make everything in the repos possible.
There's no team. It's me, my dog Luthien, a mass-produced amount of coffee, and the stubbornness to keep proving things nobody asked me to prove. Yet.
Featured work
-
Project-Navi/cd-formalization
Lean 4 + Mathlib formalization of the Creative Determinant framework — 15 theorems proved with zero sorry, CI-enforced via lake build --wfail
Lean 1 -
Project-Navi/fd-formalization
Lean 4 + Mathlib formalization: (u,v)-flower graph construction, hub distance = u^g, and log-ratio convergence to log(u+v)/log(u)
Lean 1 -
Fieldnote-Echo/claude-secure-config
Security rules, cognitive scaffolding, and hook enforcement for Claude Code — a 3-layer framework for human-AI partnership (hooks → rules → scaffold)
Python 1 -
Project-Navi/takens-formalization
Lean 4 + Mathlib formalization of delay embedding theory for dynamical systems
Lean 1 -
Project-Navi/navi-creative-determinant
The Creative Determinant: autopoietic closure as a nonlinear elliptic BVP on a compact Riemannian manifold, with Lean 4-verified existence conditions (15 theorems, zero sorry)
TeX 3
0% towards 10 monthly sponsors goal
Be the first to sponsor this goal!
$7 a month
Select- The Saint. No perks. You just want Nelson to keep being Nelson.
$14 a month
Select- The Researcher. Early access to writeups, proof sketches, newsletter deep cuts before they go public.
$25 a month
Select- The Collaborator. Everything above + input on what threads get pulled next in The Weave.