Is are there software package that can help one find a path between two mathematical statements?

Question

Sometimes when I am reading a mathematical text I will be unable to decipher the steps necessary to translate one mathematical statement into the next. Usually I have to ask for help, but I was wondering if there is a software package that would let me enter two mathematical statements and the it would find the steps necessary to get from the start to the finish.

I realize that this not tractable in general, however, it would seem with the right heuristics it could still be possible many times.

This is a response both to my own experience and this question: Question Relating Gamma Function to Riemann Zeta function evaluated at integers

Answer 1

It is probably not exactly on things You are looking for, but prover9-mace4 tries to find prof in FOL for given statements starting from given axioms ( prover9), or opposite, tries to find counterexample (mace4). I can imagine that for simple statements, like in group theory, it gives what You are looking for.

http://en.wikipedia.org/wiki/Prover9

Answer 2

There's only a handful of math software that deals with human solving/thinking process. Most apply some kind of normalization to more abstract concepts or more convenient data structures, run an algorithm on that, and then try to simplify the answer and present it in more human form.

If you were to get more into this, I suspect that you could use any powerful CAS to normalize both expressions and get the same canonical form, and from there you could trace back to both expressions.
This of course would be very painful process.

Answer 3

The likely outcome of applying software to the reading of ordinary proofs would be to discover that most proofs contain steps that are not formally correct. For example, in classical geometry many steps in the arguments are "generically true" but false for special degenerate configurations. Sometimes these configurations, such as a triangle with all three vertices the same point, are implicitly excluded from the cases considered in the theorem, or can be handled in the proof using additional steps that might be considered trivial and are not articulated in the written argument. In such cases the theorem would be correct in substance but some steps could not be filled in by a computerized proof assistant, because the steps are wrong.

Less often, there are more difficult cases, where the non-generic configurations and components can't be ignored, or the intuitive idea of what is generic behavior is incorrect. In this case a theorem may be correct, but a proof that doesn't deal with the special cases errs not only in the details but in its overall argument.

A similar thing happens in computational linguistics. When trying to process natural language with formal grammars, it turns out that simple sentences are multiply ambiguous, with a large number of unintended but correct interpretations. People constantly use additional knowledge to disambiguate the language they hear, but software does not yet have that capability.

Answer 4

I recommend the book "How to prove it" by Daniel Velleman. The associated (free) package for learning formal aspects of proof, called Proof Designer, gives the user some practice in learning how complicated finding such paths can be if one goes completely formal!