Generating Readable Proofs and 
Step-By-Step Explanations 
for Education

Peter Barendse
Wolfram|Alpha Math Content

Overview

A main purpose of this talk is reach out to educators for ideas and feedback about how we can do better at this and how we can use these programs in new ways. (So feel free to interrupt)

This is a multidisciplinary effort involving two very different worlds: 
	- the highly abstract world of mathematical logic (and programming)
	  - the very practical world of education

I’ve been part of both worlds.
	These worlds really don’t interact much, and less and less. 
	One of the ironies here I think is that, as mathematicians, we mostly see the subtlety and ingenuity required when making mathematical discoveries, and sometimes only see the less creative side of education, although we know in fact their essential natures are the opposite.
	
	A personal view of Wolfram|Alpha, homework, and CBM: 
Although I’m very pro-CBM, I don’t see giving steps and proofs in W|A as making the teaching of these algorithms obsolete. Rather, I see it as possibly allowing students to better learn these algorithms and/or learn more algorithms. (recall the story about von Neumann). 
	But aren’t kids gonna say “why should I have to learn this if my computer can not only DO IT, but also understand and present and explanation that even I CAN UNDERSTAND!??”
	The answer is that it prepares you to understand other things

Technical overview

To actually make these programs, we basically "apply" one world's ideas to the other, in both ways (“pedagogical computation” and “computational pedagogy”). 
	The obvious direction is that we "make explanations/proofs computable", by programming the logic of existing methods in the pedagogy (many of which are distinct from the way computers actually do these computations)
	But the pedagogy also informs the actual logic of the program, and actually necessitates the creation of novel algorithms, as we’ll see.
	Finally, we need to use some tricks to prevent Mathematica from evaluating too quickly

Examples of the divergence of theory and best educational practices

1. Feynman diagrams

2. Geometry proving 
(synthetic v. analytic, and even theoretical synthetic v. 9th grade)

3. matrix multiplication: faster to not always do it the standard way

Basic observations (axioms):

1. The level of query indicates the level of response the user expects 
(think grade-level as a proxy).

In general, this means that queries involving lower-level (grade level) concepts will require a more intuitive (e.g. pictorial), less jargon-y (and longer, therefore), e.g.:

"5+9"

2. Steps and proofs should be complete explanations

(In terms of Axiom 1)

3. Steps should be as simple, direct, and standard as possible 
(given 1 and 2)

Examples

the most complex SBS functions involve a list of transformations that are applied according to a custom heuristic:

"\!\(\*ButtonBox[
RowBox[{
RowBox[{"limit", " ", "as", " ", "x"}], "->", 
RowBox[{
RowBox[{"0", " ", "of", " ", 
RowBox[{"1", "/", "x"}]}], " ", "+", " ", 
RowBox[{
RowBox[{"(", 
RowBox[{"x", " ", "-", " ", "1"}], ")"}], "/", 
RowBox[{"Sin", "[", "x", "]"}]}], " ", "+", " ", 
RowBox[{
RowBox[{"(", 
RowBox[{"1", " ", "+", " ", 
RowBox[{"1", "/", "x"}]}], ")"}], "^", "x"}]}]}],
BaseStyle->"Hyperlink",
ButtonData->{
URL["http://www.wolframalpha.com/input/?i=limit+as+x-%3E0+of+1%2Fx+%2B+(x+-+1)%2FSin%5Bx%5D+%2B+(1+%2B+1%2Fx)%5Ex"], None},
ButtonNote->"http://www.wolframalpha.com/input/?i=limit+as+x-%3E0+of+1%2Fx+%2B+(x+-+1)%2FSin%5Bx%5D+%2B+(1+%2B+1%2Fx)%5Ex"]\)"

"integrate e^(3x) cos(x)"

simple physics formulas have a common function:

"work of 4 lbs, 1 foot"

chemicals have some straightforward functions:

"tryptamine structure"

a proof is just a series of steps with a known destination:

"prove by induction that 3^k > k^6"

A basic steps program

A case where the Evaluator does the right sequence of steps: PEMDAS

query=Hold[3 2^2 - 3]

ReleaseHold[query] (* but no steps! *)

f/@Hold[3 (2^2),-3](*this is the basic way to manipulate stuff inside a head, without evaluating*)

Inactive - a better version of Hold for our purpose

Inactive[3 2^2 - 3]

query2=Inactive[Plus][3 2^2, - 3]

a little recursive voodoo to get query into the exact form we want

Attributes[inactivate]={(*HoldFirst*)};
Clear[inactivate]
inactivate[(Hold|HoldComplete)[h_[arg___]]]:= Inactive[h][Sequence@@(inactivate/@{Hold/@Hold[arg]})]
inactivate[(Hold|HoldComplete)[heldarg:(Hold[_]..)]]:=Sequence@@(inactivate/@{heldarg})
inactivate[(Hold|HoldComplete)[a_Integer]]:=a

Inactquery = inactivate[query]//FullForm

Inactive[Plus][Inactive[Times][3,Inactive[Power][2,2]],-3]

Now begin: First we can say “as there are no parentheses, we first we compute the exponents in the expression (E in PEMDAS)”

Inactquery = Activate[Inactquery,Power](*neeed to Evaluate twice for formatting*)

Inactive[Plus][Inactive[Times][3,4],-3]

then we say “now we do any multiplications in the expression (M in PEMDAS)”

Activate[Inactquery,Times](*neeed to Evaluate twice for formatting*)

Inactive[Plus][12,-3]

etc...

Ask : how to make a Problem Generator microsite

(*all you really need*)
q=HoldForm[2+2];

(*CloudDeploy@*)
AskFunction[
If[
Ask[{"sum", q}-> "Number"] == ReleaseHold[q], 
"correct", 
"wrong!"
]
][]

(*CloudDeploy@*)AskFunction[
Ask[{"n", "enter math"}->"HeldMathExpression"]; 


Inactquery = inactivate[Ask["n"]];

Column[{
HoldForm@@Ask["n"], (*xx=Inactquery; ToString[xx(*/.{Inactive->HoldForm}*)],*)
"as there are no parentheses, we first we compute the exponents in the expression ",
Activate[inactivate[Ask["n"]],Power],
"now we do any multiplications in the expression",
Activate[Activate[inactivate[Ask["n"]],Power], Times],
"\n...\n",
N[ReleaseHold[Ask["n"]]]
}]
][]

Thanks!