Typed memory for AI agents with TypeDB and Lean
Model an agent's memory as a typed graph, with observations, beliefs, evidence, time, exact confidence and contradictions. Then ask the questions a vector store can't answer, with every query checked by Lean.
Five bugs the compiler catches for you
A write in a read transaction, an injectable query, a cursor that outlives its transaction, a row of the wrong shape and schema drift. When each one is caught, with the real error messages.
Introducing typedb-lean
A TypeDB 3 client for Lean 4 with typed transactions, typed queries and typed results, plus an ORM and migrations. It is as fast as the official Rust driver.
TypeDB for Edge AI AgentsVolodymyr Pavlyshyn
Want the long version?
TypeDB for Edge AI Agents covers TypeDB's model and TypeQL in depth, and how to use a typed knowledge graph as memory for AI agents. For a shorter path, start with the mini book.