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.

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.

Overview source: Curated paper metadata.

Artifacts

Tracked documentation and PDFs served directly from this folder.

Documentation

README AGENTS SKILL Metadata Extracted text Citation metadata

Document Files
Extracted Content

Historical figures (edition Retained extraction before 2026-11-06; version record not inferred) (11) — GitHub +5 more Source PDF: fep_lean_v1_04-24-2026.pdf; extraction: full_text_before_2026-11-06.md.

Historical figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, edition Retained extraction before 2026-11-06; version record not inferred, source fep_lean_v1_04-24-2026.pdf, page 32Historical figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, edition Retained extraction before 2026-11-06; version record not inferred, source fep_lean_v1_04-24-2026.pdf, page 37Historical figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, edition Retained extraction before 2026-11-06; version record not inferred, source fep_lean_v1_04-24-2026.pdf, page 47Historical figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, edition Retained extraction before 2026-11-06; version record not inferred, source fep_lean_v1_04-24-2026.pdf, page 48Historical figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, edition Retained extraction before 2026-11-06; version record not inferred, source fep_lean_v1_04-24-2026.pdf, page 51Historical figure from Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, edition Retained extraction before 2026-11-06; version record not inferred, source fep_lean_v1_04-24-2026.pdf, page 77