# Feasibility of a Latex “Computation Verifier”

This may be more appropriate on stackoverflow, but as it pertains specifically to the existence of a utility for LaTeX, I thought I should ask it here.

In my experience as an undergraduate, it's very common in problem sets to show (essentially) every step of a computation in problem sets. This is done by putting everything in some `align` environment, having `f(x) &= g(x)` at the top, and then reducing `g(x)` line-by-line until you get to whatever the desired, "simplified" answer is.

If this simplified answer disagrees with something a CAS would output, generally the error is in the transition from one line to another, and finding and fixing it is a pain.

It seems like it wouldn't be difficult to make a "computation verifier" for at least some subset of math LaTex is used for (initially, consider it just for single variable calculus, but of course this alone wouldn't be too useful). This verifier would:

1. Parse the `align` environment, and export the equalities `f(x) = g_1(x)`, `f(x) = g_2(x)`, ... into some other programming language

2. That programming language will call a CAS, to see if `g_1(x) == g_2(x)`, `g_2(x) == g_3(x)`, etc.

3. Write back some result, showing where the error occurs (maybe just which line doesn't follow from the previous).

Despite this utility seeming useful (for specifically undergraduates learning material, likely less useful the more adept someone gets at checking their own computations), I haven't been able to find anything like it. Does it exist for LaTeX? What difficulties exist in making it?

As a sidenote, I'm asking this question as I'm interested in spending the summer trying to tackle something like this, and wanted to get feedback on the feasibility of it before diving in head first. I can think of some difficulties myself, but am unsure if I should post them in the question statement.

• I would go the other way: start with the CAS to generate the steps and then convert the output to LaTeX. This is probably already in existence, I suspect that cocalc could do this. – Loop Space Apr 14 '18 at 21:00
• There have been similar systems eg scientific word typesets via latex and evaluates via a CAS (originally maple, I think then mupad) but it is easier to start with a more structured expression tree and generate latex and/or CAS input rather than parse free form hand written latex which is very hard to force into a computationally tractable format. – David Carlisle Apr 14 '18 at 21:14
• in the special case of polynomials (with numerical coefficients), package polexpr provides the means to check internally to LaTeX completely a polynomial identity. But exponents can not be "n" for example, only integers. Coefficients must be "real"... thus this is a long shot from what a full-fledged CAS offers. Nevertheless in this restricted setting one definitely could write based on `polexpr` facilities a `certifiedalign` environment... Currently sparse polynomial are poorly handled (all zero coefficients are stored and will influence computations). – user4686 Apr 14 '18 at 21:24
• @DavidCarlisle is there a more structured form that currently exists besides "syntax of whatever specific CAS"? One reason to target LaTeX is the ubiquity of use of it in math/physics, although I agree parsing hand written latex seems like it would be difficult. – Mark Apr 14 '18 at 22:40
• well at work we use mathml (check the editor of that spec:-) and generate documentation ans also executable C, Fortran, matlab, .. code some projects use very structured tex macros that they enforce with various tools, but if you allow arbitrary human written tex you end up with half a million lines of heuristics working out if `x\,y `is the same as `xy` – David Carlisle Apr 14 '18 at 22:49