Function extract_math_rust_from_source 

pub fn extract_math_rust_from_source(input: &str) -> String

Compile a Math-mode SOURCE program (the editor text) to a Rust module: split it into vernacular statements, run them into a fresh kernel, then extract every user-defined inductive/definition. This is the exact pipeline the Studio’s Math “🦀 Compile” button drives, exposed as one function so it is testable.