Lean Programming for AI Agents

An AI agent proposes an action. Something has to be able to say no, for a reason the model cannot talk its way around. This book shows you how to make Lean’s kernel that something.

Lean Programming for AI Agents is a practical guide to Lean 4 in two roles: as a programming language you can ship, and as a checker that sits inside an agent’s loop and rejects what it cannot verify. The first half teaches the language. The second half puts it to work next to an agent, ending with a complete worked example. All code is pinned to Lean 4.32.0, so the examples match the toolchain you install.

What you will learn

• Lean 4 as a working language: types and the kernel, inductive types and structures, typeclasses, do notation and monads, and Lake projects with a pinned toolchain
• How to read goal states and write proofs with tactics, extend Lean with macros, elaborators and custom tactics, and automate with grind, Aesop, simp and mvcgen
• How to drive Lean from an agent through the community REPL and Pantograph, and connect it to Python through the REPL, compiled executables or C FFI
• How proof-writing agents work, from a small best-first prover to sample-and-repair, and how to check that an autoformalized statement really says what was claimed
• How to use the kernel as a referee: typed tool contracts, checkers that accept, reject or abstain, #print axioms, and agent loops specified with Hoare-style predicates and trajectory replay
• How it all fits together in a worked agent package with a compiled checker, a Python driver and CI, plus a frank account of what you can and cannot ship today

Who it is for

Software engineers, researcher-engineers and technical leads who build, check or specify AI agents. If you are comfortable with types in any language, such as Rust, TypeScript, Haskell, OCaml or Kotlin, you have enough background. You do not need a mathematics degree.

What makes it different

Every example is agent-shaped. The same ToolCall, ToolResult and Trace types run from the early chapters to the final worked agent. The book is also strict about what a proof does and does not guarantee, keeping three levels of trust apart: a term the kernel has checked, a statement that matches the informal claim, and an assumption you have chosen to admit. Eighteen chapters are followed by five appendices, including a command and tactic cheat sheet, REPL and LeanInteract API cards, and lakefile templates.