An agent with a memory has a new way to be wrong. A chatbot that hallucinates says something false once. An agent that hallucinates into its memory says it again tomorrow, builds on it, and answers every later question on top of a contradiction nothing in the pipeline noticed. Retrieval cannot tell which of two contradictory notes is right, and asking a second model "is this consistent?" only moves the hallucination from the fact to the verdict.
This book builds the missing piece: a small, fixed checker that decides what an agent may remember and what it may claim. A fact enters memory only with a proof that the memory stays consistent, and an answer leaves it only with a proof from what is stored. The agent's ontology of people, places, organizations and events is written as types in Lean 4, its rules about the world as propositions, and every accepted fact carries a certificate checked by Lean's kernel. Rules and search come from λProlog, running inside Lean through lean-elpi, and when a search finds an answer, the kernel checks that too. The LLM proposes, Lean decides, and a rejection goes back to the model with the name of the broken rule.
The promise is narrow on purpose. A checker guarantees consistency with your axioms, not truth about the world, and every chapter says what its technique does not give you. You do not need to know Lean, Prolog, dependent types or formal logic, and you do not need to be deep in mathematics: both languages are taught from zero, with code first, then a picture, then notation. Every snippet is cut from a public repository that compiles, and every output and error message in the book is the one Lean actually prints.
What you will build
- A typed ontology for agent memory in which an ill-typed fact does not compile
- A certified store whose
insert returns a new store with a new proof, or names the axiom that blocks the fact - Hierarchies of places and events with type classes, subtypes and coercions
- Proofs about the ontology itself: invariants, safe updates and schema migrations
- Rules over the memory in λProlog, hypothetical questions that leave no trace, and search results turned into kernel-checked certificates
- An agent, written entirely in Lean, that turns away six kinds of hallucination, feeds each rejection back to the LLM, and answers only with certificates
Who it is for
Engineers who build AI agents: you know Python, you have built with LLMs, and you know roughly what RAG and a knowledge graph are. Logicians and type theorists will find familiar ideas applied to an unfamiliar problem, with reading lists to the deeper sources.
What you get
12 chapters in three parts, 33 diagrams, exercises with compiled solutions, a 60-term glossary, and the Apache-2.0 companion code at github.com/Volland/bulletproof-knowledge: Lean 4 v4.35.0 and lean-elpi v0.3.3, no Mathlib, one lake build.
