Part of the problem with this is that software like Mathematica or even SAGE is quite opaque. So you can teach folks what a derivative is, tell them that a black box called Mathematica/SAGE will calculate derivatives for them (as long as they don’t hit a bug in the implementation) but the connection between the two is lost, unlike with teaching the calculation algorithm as part of the course.
AFAICT, the best way of preserving this connection while mechanizing the calculational parts of math is to employ proof assistants such as Coq and Matita, which can extract a mathematical algorithm from a formally-verified construction, and run it on input data. However, both Coq and Matita are currently limited to rudimentary tasks, such as manipulating expressions in simple algebraic structures such as rings and fields. They are a long way from having even the equivalent of a simple CAS, partly because CAS themselves have little in the way of formal foundations—this is quite evident as soon as one tries to deal with such issues as branch cuts, real vs. complex quantities, provisos, dummy variables and the like.
In short, this idea has plenty of long-run potential but is not quite ready for prime time.
Is what you want more like the output of Wolfram Alpha? If you ask it to compute a derivative, integral, or limit, it shows you the steps it takes to get there.
Sort of. Ideally every algorithm would yield output which is formally proven to be correct wrt. the underlying mathematics. So you’d be able to select either a portion of the algorithm or a step in the printout, and see how that relates to the mathematical theory of e.g. derivatives. This is quite feasible for CAS tasks such as simplifying expressions, solving equations, computing derivatives and integrals. It is less so for numerics and graphics, but these are not a part of traditional ‘math’, so little is lost: these would be studied under numerical analysis and computer graphics.
Part of the problem with this is that software like Mathematica or even SAGE is quite opaque. So you can teach folks what a derivative is, tell them that a black box called Mathematica/SAGE will calculate derivatives for them (as long as they don’t hit a bug in the implementation) but the connection between the two is lost, unlike with teaching the calculation algorithm as part of the course.
AFAICT, the best way of preserving this connection while mechanizing the calculational parts of math is to employ proof assistants such as Coq and Matita, which can extract a mathematical algorithm from a formally-verified construction, and run it on input data. However, both Coq and Matita are currently limited to rudimentary tasks, such as manipulating expressions in simple algebraic structures such as rings and fields. They are a long way from having even the equivalent of a simple CAS, partly because CAS themselves have little in the way of formal foundations—this is quite evident as soon as one tries to deal with such issues as branch cuts, real vs. complex quantities, provisos, dummy variables and the like.
In short, this idea has plenty of long-run potential but is not quite ready for prime time.
Is what you want more like the output of Wolfram Alpha? If you ask it to compute a derivative, integral, or limit, it shows you the steps it takes to get there.
Sort of. Ideally every algorithm would yield output which is formally proven to be correct wrt. the underlying mathematics. So you’d be able to select either a portion of the algorithm or a step in the printout, and see how that relates to the mathematical theory of e.g. derivatives. This is quite feasible for CAS tasks such as simplifying expressions, solving equations, computing derivatives and integrals. It is less so for numerics and graphics, but these are not a part of traditional ‘math’, so little is lost: these would be studied under numerical analysis and computer graphics.