Active Inference · Paper · 2026

Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics

Daniel Ari Friedman

Active Inference Journal

Catalog Row113
Citation KeyFriedman2026TowardsLean4Formalization113
Paper FolderAvailable
DOI10.5281/zenodo.19699233
Platform availability

Overview

Extracted from the local paper documentation when available.

FEP Lean v1.1.0 is a source-bound, machine-checked catalogue of 155 topics across 20 reviewed families and five areas: the Free Energy Principle, Active Inference, Bayesian Mechanics, Information Geometry, and non-equilibrium Thermodynamics. Every catalogue row carries a reviewed invariant, explicit assumptions and boundaries, a namespaced Lean 4 theorem body, and deterministic manuscript...

free energy principleactive inferencebayesian mechanicsinformation geometrynon-equilibrium thermodynamicsLean 4Mathlibinteractive theorem provingformal verificationtheorem provingmeasure theoryreproducible research

Use Notes

Concise findings and methods pulled from README/SKILL documentation.

Findings / Concepts
  • The Free Energy Principle (FEP) unifies a broad family of systems properties and configurations under a variational free energy functional, however (an open source resource for) a machine-checked a
  • Dependent-type provers require explicit measure spaces, domination, and integrability that literature prose and equations may leave implicit.
Methods / Techniques
  • Lean 4 theorem proving for FEP formalization
  • AI-assisted theorem sketching and verification

Citation

Plain-text citation for quick reuse.

Friedman, Daniel Ari. 2026. Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics. Active Inference Journal. DOI: 10.5281/zenodo.19699233. URL: https://doi.org/10.5281/zenodo.19699233.

Primary source Documentation Full Text Image Gallery Source repository BibTeX

Related in Active Inference

Other catalogued works in the same domain.

View all Active Inference works, software & media →