Machine-checked Lean 4 proofs for "From Recursive Scaffolding to Admissibility-First Construction: Mechanism, Stability, and Failure-Mode Decomposition on OOLONG-Pairs" — filter recall preservation, oracle construction sufficiency, endpoint-factorization insufficiency, and pair-precision amplification under independence.
theorem-proving language-models formal-verification ai-safety mathlib lean4 llm long-context admissibility-dynamics pair-construction empirical-companion oolong-pairs
-
Updated
May 7, 2026 - Lean