> I'm sure my request isn't unique: one of the major goals of Sage is to
> provide a platform that allows people to _verify_ it, which is par for
> the course for any mathematician. I'd like to see the steps Sage uses
> to convert the sum I give it (or what not) to the form it chooses.
I think there are two distinct issues raised in your request:
1. You want to verify that an answer Sage provides is correct.
2. You want to know how Sage got the answer that it provides.
It may be much easier to check Sage's answers than to follow the
algorithms that it (or Maxima) uses to find the answers. You mention
that you were using Sage to compute a symbolic sum. In essence, you
were asking Sage to solve a recursion. In order to check that Sage's
solution is valid, you just need to check that its solution satisfies
the appropriate difference equation and that it has the appropriate
initial value. Here are the steps for a simple example of this sort:
sage: var('m n')
(m, n)
sage: h = sum(m^5, m, 1, n); h
1/6*n^6 + 1/2*n^5 + 5/12*n^4 - 1/12*n^2
sage: h - h.subs(n=n-1)
-1/6*(n - 1)^6 - 1/2*(n - 1)^5 - 5/12*(n - 1)^4 + 1/12*(n - 1)^2 +
1/6*n^6 + 1/2*n^5 + 5/12*n^4 - 1/12*n^2
sage: _.simplify_full()
n^5
sage: h.subs(n = 1)
1
Those steps have Sage find a closed-form expression for $\sum_{m=1}^n
m^5$ and verify that this expression works by checking that it
satisfies the desired recursion and that it has the desired initial
value. Since it is so easy to check Sage's answer, it is probably not
important to know exactly how it got the answer. (For all I know,
someone programmed that particular sum directly into Sage.)
For many algebraic problems (e.g. factorization, symbolic integration,
and Groebner-basis calculations), the solutions that Sage provides are
easy to verify, assuming that one trusts Sage to do basic algebraic
calculations as in the example above. On the other hand, if one asked
Sage, say, to find a minimal spanning tree in a graph, then one would
not have a similar simple verification of Sage's work. It would be
nice if one could use only code compiled from certified Coq (a proof
assistant) scripts for calculations, but the difficulties of
formalizing mathematics sufficiently for machine certification suggest
that it may be a long wait for such certainty.
Regards,
James Parson
--
To post to this group, send email to sage-support@googlegroups.com
To unsubscribe from this group, send email to
sage-support+unsubscr...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/sage-support
URL: http://www.sagemath.org
