Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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:

share|cite|improve this question
Good idea. I suppose this site is a sort of Mechanical Turk version of that software... – Christopher Edwards Aug 12 '10 at 19:59

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.

share|cite|improve this answer

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.

share|cite|improve this answer
Thanks for the link. I think like you alluded to it is geared to simple logical frameworks, which I think wouldn't work for my purposes. – Jonathan Fischoff Aug 12 '10 at 19:47

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.

share|cite|improve this answer

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!

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.