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

Zenodo

Download PDF Publication source Paper folder on GitHub Read extracted text

Overview

The selected FEP_Formal 2.1.0 manuscript describes 168 stable Lean topics across five areas, using Lean 4.35.0 and Mathlib 4.35.0. It reports a semantic audit with 149 directly formalized rows at narrowed scopes and separates compilation maturity from scientific adequacy. Native receipt-backed compilation and optional Hermes/OpenGauss execution remain different evidence contracts. The manuscript does not prove the empirical FEP, generic Markov blankets or equivalence of its motivating formalisms; this catalog refresh does not rerun Lean, numerical examples or provider workflows.

free energy principleactive inferencebayesian mechanicsinformation geometrynon-equilibrium thermodynamicsLean 4Mathlibinteractive theorem provingformal verificationtheorem provingmeasure theoryreproducible researchmathematical positioningtheorem statement analysissemantic visualization

Overview source: Curated paper metadata.

Methods and contributions

Read the source for the full argument, qualifications, and evidence.

Findings and contributions

  • The manuscript reports 149 of 168 rows as directly formalized at deliberately narrowed scopes, independently of compilation maturity.
  • The manuscript expressly declines empirical FEP, generic-blanket and broad-equivalence conclusions.

Methods

  • Typed catalog with explicit assumptions and semantic dispositions — Described in the selected deposited manuscript; source-text review does not re-execute or independently validate this method.
  • Separate native and optional provider evidence contracts — Described in the selected deposited manuscript; source-text review does not re-execute or independently validate this method.

Summary sources: Paper metadata and evidence · Extracted source text.

Document downloads

PDFs are hosted here; supporting sources may use pinned archives.

These files may be different versions or companion documents. The archive does not identify a latest edition.

Citation

Citation metadata follows the unified bibliography.

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. Zenodo. DOI: 10.5281/zenodo.19699233. URL: https://doi.org/10.5281/zenodo.19699233.
Download bibliography Add to reading list Explore connections

Catalog details and resources

Catalog row113
Citation keyFriedman2026TowardsLean4Formalization113
DOI10.5281/zenodo.19699233
Platform availability
Paper documentation Historical figures (edition Retained extraction before 2026-11-06; version record not inferred) on GitHub Image source: fep_lean_v1_04-24-2026.pdf; full_text_before_2026-11-06.md. Associated software repository

Related works

Ranked by recorded methods, topics, contributors and associated software, with contributor roles and domain-only matches labelled. Metadata overlap is not a citation or a scientific equivalence.

View all Active Inference works, software & media →