Skip to content

FEP_Lean v1.0.0 — Lean 4 Formalization of the Free Energy Principle

Choose a tag to compare

View all tags
@docxology docxology released this 24 Apr 18:09
· 532 commits to main since this release
v1.0.0
a32b452

FEP_Lean v1.0.0 — Lean 4 Formalization of the Free Energy Principle

DOI: 10.5281/zenodo.19699234
License: Creative Commons Attribution 4.0 International (CC BY 4.0)
Copyleft: DAF 2026

Cite this release

Friedman, D. A. (2026). Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics. In Active Inference Journal. Zenodo. https://doi.org/10.5281/zenodo.19699234

What is inside

  • 50-topic machine-checked catalogue spanning five theoretical pillars — FEP (14) · Active Inference (11) · Bayesian Mechanics (10) · Information Geometry (8) · non-equilibrium Thermodynamics (7).
  • 50 / 50 sorry-free compilation under the pinned stack: Lean 4.29.0 + Mathlib 4.29.0 (lake env lean).
  • Hermes / OpenGauss LLM-assisted pipeline with primary model moonshotai/kimi-k2.6, wall-clock deadlines, and a cache keyed to Lean source hashes; the Lean 4 kernel remains sole ground truth for every compilation claim.
  • Zero-mock test discipline: 347 tests, ≥89 % combined line+branch coverage on src/, exercised against real files, a real SQLite store, live compiler invocations, and real HTTP round-trips.
  • 168-page manuscript PDF (fep_lean_v1_04-24-2026.pdf, 1.82 MB) attached as a release asset.

Repository layout

  • src/ — Python pipeline (catalogue, Hermes, verification, orchestrator).
  • lean/ — Lake workspace with pinned toolchain and the 50-topic FepSketches module.
  • manuscript/ — markdown chapters, references, figures, manuscript variables.
  • tests/ — 347-test zero-mock suite.
  • scripts/ — analysis + maintenance entry points.
  • docs/ — API reference, configuration, troubleshooting, glossary.
  • CITATION.cff — machine-readable citation metadata.
  • LICENSE — CC BY 4.0.

Built from

This project is continuously re-verified from the docxology/template monorepo, which injects validated package- and manuscript-level metadata at render time.

Reproduction quick-start

git clone https://github.com/ActiveInferenceInstitute/FEP_Lean.git
cd FEP_Lean
uv sync --extra dev
uv run pytest tests/ --cov=src --cov-fail-under=89
bash scripts/_maint_bootstrap_lean_toolchain.sh   # Lean 4.29.0 + Mathlib 4.29.0
uv run python scripts/03_lean_verify_only.py      # native 50/50 sweep

© 2026 Daniel Ari Friedman · CC BY 4.0 · https://doi.org/10.5281/zenodo.19699234

Assets 5
Loading