Closure properties of type-0 (general) grammars are typically proved via Turing machine arguments in the literature, which are potentially more difficult to formalize. These properties lacked machine-checked verification.

The authors formalize general grammars using the Lean 3 proof assistant, defining basic notions of rewrite rules and derived words. They show closure of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. For the Kleene star, the authors developed their own grammar-based construction since the literature's approach was unsuitable for formalization.

All four closure properties (union, reversal, concatenation, Kleene star) are formally verified in Lean 3. The Kleene star proof required an original grammar-based construction that diverges from the standard literature.