fep_formal/CITATION.cff at main · ActiveInferenceInstitute/fep_formal · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
cff-version: 1.2.0
message: "If you use this software, please cite it as below."
type: software
title: "fep_formal: Towards Lean 4 Formalization of the Free Energy Principle"
abstract: >-
  A catalogue of 168 Free Energy Principle topics spanning FEP foundations,
  Active Inference, Bayesian Mechanics, Information Geometry, and
  Thermodynamics. Each row has a canonical Lean 4 topic body, reviewed
  invariant, explicit assumptions, and a separate semantic maturity record.
  The Python package supports deterministic offline artifacts, native
  Lean verification, and configured Hermes/OpenGauss execution. The 2.1.0
  implementation uses the pinned Lean 4.35.0 / Mathlib 4.35.0 profile; fresh
  source-bound native acceptance requires zero warnings and proof holes.
  Historical evidence retains its original source and toolchain. Compilation
  alone does not establish semantic adequacy or empirical validity of the FEP.
authors:
  - &canonical-author
    family-names: Friedman
    given-names: Daniel Ari
    email: daniel@activeinference.institute
    orcid: "https://orcid.org/0000-0001-6232-9096"
    affiliation: Active Inference Institute
doi: "10.5281/zenodo.23196891"
version: "2.1.0"
date-released: "2026-10-24"
repository-code: "https://github.com/ActiveInferenceInstitute/fep_formal"
url: "https://github.com/ActiveInferenceInstitute/fep_formal"
license: CC-BY-4.0
keywords:
  - Free Energy Principle
  - Active Inference
  - Lean 4
  - Mathlib4
  - interactive theorem proving
  - formal verification
  - variational inference
  - Bayesian mechanics
  - information geometry
  - LLM-ITP integration
  - reproducible research
  - execution-integrity pipeline
  - measure theory
  - continuous-time Markov chains
preferred-citation:
  type: article
  title: "Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics"
  authors:
    - *canonical-author
  year: 2026
  journal: "Active Inference Journal"
  doi: "10.5281/zenodo.23607007"
  url: "https://doi.org/10.5281/zenodo.23607007"