No it was not that one. The question was just about the inductive proof of the
Sum[2 i, {i, 1, n} == n^2 + n
statement. It is really strange, unless I have serious hallucinations - not unheard of at the end of the working week - there was a question about using Mathematica to prove the statement above. It might have been from the same person as the thread you mention.
Anyway, I am not really familiar with automatic theorem proving, which is certainly not the main interest of the person who asked the question in the first place. There are approaches such as Theorema described in Buchberger's article. Do you have any experience with this type of software package? I recently attended a conference on automatic theorem proving which some interesting approaches, and it seems that Stephen Wolfram is also exploring ways of how Mathematica can be used for theorem proving, but he is coming from a different direction, I guess, a direction that might be more appealing to mathematicians.
Cheers,
Marco