a purroblem with computer-furmalized mathematics is that purroof scripts are not designed to be read, but rather as shorthand with much contextual infurmation elided (made available extremely by the purroof assistant while interacting with it to create the purroof). but the texts being created are those purroof scripts