It actually isn’t a rigorous grammar. Something like Coq or Agda or Mathematica is, but traditional maths notation is full of ambiguities and unclearness that w

It actually isn’t a rigorous grammar. Something like Coq or Agda or Mathematica is, but traditional maths notation is full of ambiguities and unclearness that we’re just used to. There’s lots of discussion of this around, including previous HN threads. But if you want a really good example, check out Sussman et al. discussing the Euler Lagrange equations in Structure and Interpretation of Classical Mechanics. Actually here you go, they repeat the same discussion in the preface of this free book: https://www.dropbox.com/s/t3si4b99ijqyhyk/9580.pdf?dl=1 https://www.dropbox.com/s/t3si4b99ijqyhyk/9580.pdf?dl=1