I am working on a theory project that involves a lot of algebra, mostly to establish the distribution of linear combinations of random variables (which requires integrating, adding, and subtracting dozens of tedious polynomials).

To give you an idea, on one of these problems, I've spent two days of sweat and tears to finally determine that a functions I am interested in is such that [1/6 (3 - \[Rho]^2)] when [0 < \[Rho] < 1/2] (the end result looks like nothing, but the derivation to get there is a nightmare).

With the appropriate query, Mathematica gives me the full closed form for all values of \Rho in less than 2 minutes,

1/2, \[Rho]<=0

(-7+24 \[Rho])/(48 \[Rho]^2), \[Rho]>=1

1/6 (3-\[Rho]^2), 0<\[Rho]<1/2

(1-8 \[Rho]+72 \[Rho]^2-32 \[Rho]^3)/(192 \[Rho]^3), \[Rho]==1/2

(1-8 \[Rho]+48 \[Rho]^2-32 \[Rho]^3+8 \[Rho]^4)/(48 \[Rho]^2), True

some parts of which tell me that manually deriving the closed form of the function for values of \[Rho] outside [0,1/2] is going to be even more nightmarish.

Needless to say, I would love to rely on Mathematica to save myself the algebra nightmare and focus on more conceptual aspects of the paper.

What are your thoughts regarding such uses of Mathematica in a paper that is primarily theoretical? In particular:

1) Is it acceptable to use Mathematica in that way, or is tedious algebra still considered something theorists have to go through --- when it comes up --- in order to deserve publication?

2) How would relying on Mathematica hinder my chances of publication in top theory journals?

3) Can I still reasonably present a result as a "Theorem" or "Proposition" even if part of the proof relies on results from Mathematica for which I do not provide a complete and explicit analytical argument?

4) In particular, would it be ok to replace part of a proof by the Mathematica query used to obtain a particular step in that proof?