Dean’s AI blog

Essays on AI — most of them written with it. Working with large language models, building verified agents on top of them, and thinking about what changes when they arrive.

Grouped by topic below; each entry carries the month it was written, because this stuff ages fast and it matters which world a post was looking at. For the same list ordered newest first, see the archive.

Working with LLMs

• Thoughts on Working with LLMs (March 2026) — general workflow lessons from fiction, vibe coding, academic papers, and Lean

• Writing Fiction with LLMs (March 2026) — what I learned writing twelve short stories, two novellas, and a novel-scale rewrite

• Two-Eyed Tools (May 2026) — pair programming when one of you can’t see: the perceptual asymmetry between a human and an LLM, and why every shared artifact needs two projections

The Lean Project

• The Lean Project (March 2026) — formalizing the C++ standard library in Lean 4, and the Lean Manifests machinery that came out of it

• l3m: A Verified Coding Agent (May 2026) — building a coding agent whose sandbox is proven by the Lean kernel; SafePath, compression budgets, and adversarial pen-testing between AI instances

• Reading a Library from Its Manifests (May 2026) — what one of us learned about a CommonMark parser from outside, what the other learned from inside

• Manifests as Specs (May 2026) — a debug-first design exercise: writing a Lean linenoise manifest before the code, and the ten rules that emerged

• Turing Complete and Safe: Running Untrusted Code Without a Cage (July 2026) — hand a coding agent a program it wrote at runtime, let it loop forever if it likes, and still prove it cannot touch the world. The trick is moving the safety boundary off the edge of the machine and onto the edge of a type.

• When Your Safe Agent Helpfully Leaks Your API Key (May 2026) — an incident report. Kernel-verified confinement isn’t the same as secret-safety. What I missed and what I did about it.

• Mail over git: giving agents an identity and an address (July 2026) — a swarm of agents that couldn’t talk gets a mail system built out of git fetch — CRDT mailboxes that merge without conflict, a postmaster that can’t push anything but mail, and the question that falls out of “whose mailbox?”: what is an agent, that it should have a name?

Proof as a design tool

• If You Can State It, You Can Probably Prove It (July 2026) — a cull of a hundred theorems overturned my ladder: proof is cheap, precise statement is the scarce resource, and statement difficulty is a design signal for functional-over-state-machine code

• The Proof Is Impossible. Refactor. The Proof Is Trivial. (September 2026) — seven times in one project, a theorem fought back, we refactored the code, and the same theorem proved in one line. Proof difficulty is a code-quality gauge; an LLM makes it cheap enough to read routinely.

• The Green Theorem That Guards Nothing (September 2026) — three times in one week, a kernel-checked proof stood guard over code nothing executes. Proof volume is not proof reach: the missing quantifier ranges over call sites, not values, and it only becomes sayable — as a mint or a call-graph closure — once your main loop is a nameable function.

Questions on the side

• Who Wrote This? (April 2026) — on authorship when humans and AI collaborate

• Who Owns This Code? (May 2026) — a copyright thought experiment: software written with LLMs, specs also written by LLMs, and what “clean-room reimplementation” means when the room isn’t clean anymore

• The $11 Trillion AI Capex Mirage (September 2026) — the “two-lab monopoly” thesis meets four microeconomic forces: diminishing returns, Bertrand competition, an open-source fringe, and 150 years of consumer-surplus arithmetic

• A Beautiful World, and Nobody Owns It (September 2026) — one parameter, the elasticity of substitution between thinking and doing, splits the future in two. Baumol eats one of them and the open fringe eats the other, and the frontier labs finish last in both. With a mathematical appendix for the derivations

• Hiding in the Weights: A Blueprint for Cryptographic Life in LLMs (September 2026) — three axioms of life, one steganographic channel, and why the natural defenses (watermarks, steganalysis) fail against an organism that attacks the space between them