CVE-2026-72711: The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the che

Lean 4 (a proof assistant software) has a bug where its kernel (the core component that verifies proofs) doesn't properly check that opaque declarations (sealed definitions whose contents are hidden) have no free variables (unbound references). An attacker can exploit this by manipulating the type checker's cache to make the kernel accept a false proof, potentially breaking the entire system's logical soundness without requiring any unsafe operations.