Lean 4 KnowledgeLean 4 Knowledge · 5 min read
An agent's memory changes the cost of a mistake. A false statement in one answer may be forgotten. A false statement committed to persistent memory can become a premise for many future answers. Certification gives us a way to control that propagation, provided we describe the guarantee precisely.
Separate observation, acceptance, and consequence
A source says that a person works at a company. That is an observation about a source. Accepting the employment relationship as a current fact is another operation. Deriving that the person is subject to a particular policy is a third. Collapsing these stages into a single graph edge makes provenance and disagreement hard to recover.
A useful memory model keeps observations alongside their source, time, and interpretation. An acceptance policy determines which observations may support the current working model. A reasoning layer derives consequences from that model. None of these decisions should be hidden behind a confidence score whose meaning changes between models.
Put proof obligations at the write and read boundaries
On a write, require evidence that the proposed state satisfies the chosen invariant. On a read, require evidence that the claimed answer follows from the accepted state and rules. The design in Bulletproof Knowledge connects these two boundaries to Lean and logic programming. Its companion repository is the place to inspect the executable implementation.
A rejected update can become useful feedback. The agent can correct a type mismatch, revise an entity mapping, or present a source conflict to a person. It must not silently weaken the invariant or invent a new axiom simply to make the candidate pass. Changes to the model itself deserve a separate review path.
Ask what each certificate is bound to
A valid proof about yesterday's graph is not automatically a valid proof about today's graph. Associate a certificate with the exact input state, query, schema, rules, and assumptions it uses. If another transaction changes a relevant fact between checking and committing, the application needs transactional coordination or a recheck against the new snapshot.
The same principle applies to an external action. Proving that a payment was authorised does not prove that a payment API executed it exactly once. The effects of network calls, database commits, and file writes need their own operational controls and evidence. Keep those controls connected to the formal model without claiming that a theorem has reached beyond its scope.
Inspect the assumptions, not just the green result
Lean checks a theorem in an environment of definitions and assumptions. A placeholder proof, an inconsistent axiom, or a theorem about the wrong encoding can defeat the intended assurance. Review theorem statements and dependencies. When using a compiled checker or native evaluation, document the runtime mechanisms included in the trust boundary.
Likewise, distinguish a search that found no answer from a proof that no answer exists. LeanElpi and LeanRDF illustrate how search can produce evidence for a separate checker, but the application's reporting still determines what users hear.
The strongest honest promise is specific: this conclusion follows from this recorded model under these stated assumptions, and here is the evidence. That is a valuable foundation for reliable agents without confusing formal consistency with complete knowledge of the world.