Machine-checked Lean 4 proofs for "Recursive Language Models Through the Admissibility-Dynamics Framework." Covers RLM sub-call architecture, three sufficient conditions for bounded-inconsistency deployment (safe abstention, bounded-decomposable predicates, runtime depth verification), training class closure, and the deployment-boundary synthesis.
theorem-proving language-models formal-verification ai-safety mathlib lean4 llm recursive-language-models machine-checked-proofs admissibility-dynamics recursive-scaffolding
-
Updated
May 19, 2026 - Lean