Is Maple's simplification assuming integer rigorous?

Question

I have a rather long and complicated expression that should be zero that I cannot work out by hand. But using Maple and assuming the variable is an integer, it simplifies to zero, as expected.

How can I verify this to use in a rigorous proof?

Does Maple have a way of showing steps? Or is the simplification command with integer variables rigorous? Perhaps some other way that I haven't thought of?

For some specifics, this is about using Zeilberger's algorithm on a hypergeometric function. So we also have the certificate, but we were hoping to verify this without having to appeal to the Zeilberger's.

Answer 1

Everything in Maple is supposed to be 'rigorous', but very little of it can actually be verified to be so.

The first thing to try would be to use the infolevel facility, and do

userinfo[all] := 3;

before your computation. You're going to see a lot of information about what Maple is doing. That might be enough. The 'level' can be made higher, to get more information still. Not all routines give information, so you might not get want you want. Some give too much...

If that doesn't do it, then printlevel is your next tool. This will print a full trace of all routines. printlevel works in increments of 5. So doing

printlevel := 15

will give you a trace of everything going on for the top 3 levels of calls. As things are deeply nested, you'll over need 100 or 200 to get to where the 'real' work is done. And you'll get flooded too. I pretty much always use printlevel with the TTY version of Maple in batch mode.

The printlevel output is nested: the { and } in its output match, to ease navigation with any decent programmer's editor.