Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics

The Free Energy Principle (FEP) unifies a broad class of system properties under a variational free-energy functional, but a machine-checked substrate for assessing related formal claims has been missing. Dependent-type provers require explicit measure spaces, domination, and integrability that prose often leaves implicit. This work introduces a curated catalog of 50 topics across five pillars—14 FEP, 11 Active Inference, 10 Bayesian Mechanics, 8 Information Geometry, and 7 non-equilibrium Thermodynamics—each as a namespaced Lean 4 sketch against Mathlib4 , with natural-language statements, imports, ecosystem-maturity tags, and sorry-free theorem bodies maintained from a single source of truth. On the pinned stack leanprover/lean4:v4.29.0 / Mathlib4 v4.29.0 , the shipped catalog compiles 50/50 sorry-free under lake env lean. The manuscript describes an LLM-assisted drafting and commentar