Now imagine being able to 'recompile' a mathematical text as an AST for the derivation, so that you could dive down and see where all the terms and definitions were coming from, instead of having to try to search a PDF for some symbol you can't ctrl-F for.