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

Documentation folder for catalog row 113 · Canonical work page

Paper folder on GitHub
Primary Work PageFriedman2026TowardsLean4Formalization113
DOI / Source10.5281/zenodo.19699233
Folderpapers/2026_FEPLean/

Overview

Curated abstract 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 metadata.

The release is pinned to Lean 4.33.1 and Mathlib 4.33.1 (locked Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474). Its native receipt verifies 155/155 topic closures with zero errors, warnings, or sorry. The schema-4 formalism audit covers all 823 required formal-resource declarations, including 699 evidence declarations, and reports no sorryAx or untrusted project axioms. The canonical Python acceptance run collected 1,203 tests: 1,080 passed, 123 skipped, zero failed or errored, with 89.81% line coverage (8,808/9,807 statements). The schema-4 Chrome 151 browser receipt replays six source-bound screenshots covering 155 topics, 20 families, 133 relations, 48 satisfied capabilities, and 15 typed numerical witnesses.

These checks establish the exact shipped formal statements and reproducible software evidence; they do not prove the Free Energy Principle as a physical theory. Provider-backed Hermes commentary is optional and unavailable for this release cut, and no historical provider report is promoted to current full-mode evidence.

Source and release: github.com/ActiveInferenceInstitute/fep_lean (https://github.com/ActiveInferenceInstitute/fep_lean) and GitHub release v1.1.0 (https://github.com/ActiveInferenceInstitute/fep_lean/releases/tag/v1.1.0). The exact deterministic 232-member evidence bundle has SHA-256 0009447598ecd3bbf68548eab360704a2539480379791eb0128186fa230884ea and binds release commit d7b6f8b15ea9dc451b191e3674a1fd72b5e586b4.

Overview source: Curated paper metadata.

Artifacts

Tracked documentation and PDFs served directly from this folder.

Documentation

README AGENTS SKILL Metadata Extracted text Citation metadata

PDF Files
Extracted Content

Extracted Images (11) — GitHub +5 more

Figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, page 32Figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, page 37Figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, page 47Figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, page 48Figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, page 51Figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, page 77