> Sometimes I wonder why LaTeX math mode doesn't do some fancy static analysis. Considering how much math is just a language, and we know how to prove (and chec

> Sometimes I wonder why LaTeX math mode doesn't do some fancy static analysis. Considering how much math is just a language, and we know how to prove (and check) things about languages It wouldn't be practical beyond some basic checks. Turning a paper proof from even the standard you'd find in a journal publication into a formalised (e.g. Coq) proof is a research grade task. The automation required to justify each step in a typical paper proof back to your axioms isn't close to being practical for casual use.