Decision math, proved correct in Lean 4.

teleon.dev/docs/lean holds Lean 4 proofs, in fep_lean, about active inference: how expected free energy G(pi) scores the policies an agent can choose. Each proof holds for every run that uses its definitions.

v44.0teleon.dev/docs/leanFormal proofshttpsjson

Read the docs Copy the agent prompt

One theorem, checked

Definitionsgenerative model, policies, preferences

Theorem statedG(pi) = risk + ambiguity

Lean 4 kernel checkproof accepted, three standard axioms

Proof recordtheorem, revision and axioms in S215

The kernel accepted the proof, so the scoring rule it covers holds for every policy the runtime ranks.

What it does

Expected free energy

Each candidate policy gets a G(pi) score that balances reaching preferred outcomes with gaining information.

Stated and proved

The properties of G(pi) that the runtime relies on are written as Lean 4 theorems in fep_lean.

Checked by a small kernel

Lean's kernel rechecks every proof step, out of process from the solver, like every Teleon verifier.

The contract

A proof record names the theorem, the Lean 4 toolchain, the fep_lean revision, the axioms used and the kernel's verdict.

ProvesProperties of expected free energy G(pi)

Proverfep_lean on Lean 4

StoreS215 active inference proofs

Queuesaq651 to aq700, v44.0

Identifiers

fep_lean
G(pi)

Execution contracts

Request and responseCopy

POST /v1/lean/check
Host: api.teleon.dev
{
  "theorem": "efe_decomposition",
  "library": "fep_lean@3f9c2e1",
  "toolchain": "lean4"
}

# Response
{
  "theorem": "efe_decomposition",
  "statement": "G(pi) = risk(pi) + ambiguity(pi)",
  "status": "proved",
  "axioms": ["propext", "Classical.choice", "Quot.sound"],
  "checked_ms": 2140
}

Endpoints

Method	Path	Access	What it does
`POST`	`/v1/lean/check`	RING-2	Check a theorem with Lean 4
`GET`	`/v1/lean/theorems`	RING-3	Browse the proved theorems in fep_lean
`GET`	`/v1/lean/proofs/{id}`	RING-3	Read a proof record with its axioms

Listed paths appear in the service’s published files today. This surface comes from the Teleon Omnibus Codex v1.0 to v50.0, Oct 25, 2026. In the one-host plan every path here is served under api.teleon.dev/v1/lean.

How it connects

Reads from

World modelsteleon.dev/docs/worldmodel Verification sandboxteleon.dev/docs/sandbox

Feeds into

Confidence scoresteleon.dev/docs/confidence Assurance and evidenceteleon.dev/docs/assurance

Queuesaq651-aq700

StoresS215 Lean 4 Active Inference Proofs (fep_lean)

For agents

Give your agent the read-only guide first. It reports back before any write.

Agent prompt

Read https://teleon.dev/docs/lean.md and list the theorems proved about expected free energy. Read only.

Copy

llms.txt Agent card

Words on this page

Full glossary

Active inference: A theory of action in which an agent picks the policy with the lowest expected free energy.
Expected free energy: G(pi), a policy's score: expected risk, the distance from preferred outcomes, plus expected ambiguity. Lower is better.
Lean 4: A programming language and proof assistant whose small kernel checks every step of every proof.