Tag Archives: Formal verification

Wolfram|Alpha as a self-verification tool

Last week, I wrote about structuring class time to get students to self-verify their work. This means using tools, experiences, other people, and their own intelligence to gauge the validity of a solution or answer without uncritical reference an external authority — and being deliberate about it while teaching, resisting the urge to answer the many “Is this right?” questions that students will ask.

Among the many tools available to students for this purpose is Wolfram|Alpha, which has been blogged about extensively. (See also my YouTube video, “Wolfram|Alpha for Calculus Students”.) W|A’s ability to accept natural-language queries for calculations and other information and produce multiple representations of all information it has that is related to the query — and the fact that it’s free and readily accessible on the web — makes it perhaps the most powerful self-verification tool ever invented.

For example, suppose a student were trying to calculate the derivative of $y = \frac{e^x}{x^2 + 1}$. Students might forget the Quotient Rule and instead try to take the derivative of both top and bottom of the fraction, giving:

$y' = \frac{e^x}{2x}$

Then, if they’re conscientious students, they’ll ask “Is this right?” What I suggest is: What does Wolfram|Alpha say? If we type in derivative of e^x/(x^2+1) into W|A, we get:

The derivative W|A gets is clearly nowhere near the derivative we got,  so one of us is wrong… and it’s probably not W|A. Even if we got the initial derivative right in an unsimplified form, the probability of a simplification error is pretty high here thanks to all the algebra; we can check our work in different ways by looking at the alternate form and at the graphs. (Is my derivative always nonnegative? Does it have a root at 0? If I graph my result on a calculator or Winplot, does it look like the plot W|A is giving me? And so on.)

But how is this better than just having a very sophisticated “back of the book”, another authority figure whose correctness we don’t question and whose answers we use as the norm? The answer lies in the  “Show steps” link at the right corner of the result. Click on it, and we get the sort of disclosure that oracles, including backs of books, don’t usually provide:

Every step is generated in complete detail. Some of the details have to be parsed out (especially the first line about using the Quotient Rule), but nothing is hidden. This makes W|A much more like an interactive solutions manual than just the back of the book, and the ability given to the student to verify the correctness of the computer-generated solution is what makes W|A much more than just an oracle whose results we take on faith.

Using W|A as a self-checking tool also trains students to think in the right sort of way about reading — and preparing — mathematical solutions. Namely, the solution consists of a chain of steps, each of which is verifiable and, above all, simple. “Differentiate the sum term by term”; “The derivative of 1 is zero”. When students use W|A to check a solution, they can sit down with that solution and then go line by line, asking themselves (or having me ask them) “Do you understand THIS step? Do you understand THE NEXT step?” and so on. They begin to see that mathematical solutions may be complex when taken in totality but are ultimately made of simple things when taken down to the atomic level.

The very fact that solutions even have an “atomic level” and consist of irreducible simple steps chained together in a logical flow is a profound idea for a lot of students, and if they learn this and forget all their calculus, I’ll still feel like they had a successful experience in my class. For this reason alone teachers everywhere — particularly at the high school level, where mechanical fluency is perhaps more prominent than at the college level — ought to be making W|A a fixture of their instructional strategies.