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

Catalog Row113

Citation KeyFriedman2026TowardsLean4Formalization113

Paper FolderAvailable

DOI10.5281/zenodo.19699234

Overview

Extracted from the local paper documentation when available.

The Free Energy Principle (FEP) unifies a broad class of system properties under a variational free-energy functional, but a machine-checked substrate for assessing related formal claims has been missing. Dependent-type provers require explicit measure spaces, domination, and integrability that prose often leaves implicit. This work introduces a curated catalog of 50 topics across five pillars—14 FEP, 11 Active Inference, 10 Bayesian Mechanics, 8 Information Geometry, and 7 non-equilibrium Thermodynamics—each as a namespaced Lean 4 sketch against Mathlib4 , with natural-language statements, imports, ecosystem-maturity tags, and sorry-free theorem bodies maintained from a single source of truth. On the pinned stack leanprover/lean4:v4.29.0 / Mathlib4 v4.29.0 , the shipped catalog compiles 50/50 sorry-free under lake env lean. The manuscript describes an LLM-assisted drafting and commentar

Free Energy PrincipleActive InferenceLean 4Mathlib4interactive theorem provingformal verificationvariational inferenceBayesian mechanicsinformation geometryLLM-ITP integrationreproducible researchmeasure theory

Use Notes

Concise findings and methods pulled from README/SKILL documentation.

Findings / Concepts

A 50-topic formal catalog of FEP-related mathematics with explicit Mathlib4-facing statements and a reproducible, version-pinned verification story.
Axiomatization vs. problem-solving : positions LLM+ITP work as building shared formal structure, not just benchmark solving.
Hermes / OpenGauss pipeline: LLM drafts and explains sketches while native Lean verifies; compilation remains the non-negotiable check.
Zero-mock testing policy in the software stack (real files, real SQLite, live compiler, real HTTP) as stated in the manuscript.
A Lean primer and Mathlib4 / measure-theoretic probability guidance aimed at Active Inference researchers entering formal methods.

Methods / Techniques

Theoretical and systems paper: YAML → manuscript → Lake pipeline; per-topic modules with LaTeX-adjacent statement signatures.
Open-source : https://github.com/ActiveInferenceInstitute/FEP Lean (manuscript build uses the docxology template approach for validated metadata injection).
Archived manuscript (v1): https://doi.org/10.5281/zenodo.19699234 · Zenodo record https://zenodo.org/records/19699234

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.

Primary source Documentation BibTeX