[asdf_snar]

Math formulae are not trivial to check formally using a computer. Mathematical software is in its infancy relative to the sophistication of mathematical objects defined in the literature.