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.

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 approach to assessing such and related formal claims has remained absent. Dependent-type provers require explicit measure spaces, domination, and integrability that literature prose and equations may...

FEPLean

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 →