Constructive proof of transcendence of $e$ and $\pi$? Someone asks to me that can we prove the transcendence of $\pi$ without using proof by contradiction. I find some proofs of transcendence of $\pi$ and $e$ and I found that all of proof I found starts from the sentence "Suppose $x$ is algebraic...", which means the proof relies on the proof by contradiction.
Since $\pi$ and $e$ are computable, I suspect that their transcendence can be proven in constructive sense, and I guess that we may eliminate non-constructive nature of a proof of transcendence of them. However I didn't get how to do this. Thanks for any idea.
 A: There is a faulty premise in the question, namely that a proof that begins with "suppose not" is necessarily a proof by contradiction. In constructive mathematics, the notion of "not" is different than in classical mathematics; this is one reason why the double negation of a statement is not equivalent to the original statement. 
In constructive mathematics, a statement of the form "not X" is viewed as an abbreviation for "X implies a contradiction". Thus, to prove a statement of the form "not X" constructively, a mathematician can assume X and then derive a contradiction. This is not a proof by contradiction, however: it is a direct proof of "not X". Like other direct proofs of implications, it merely assumes the hypothesis and derives the conclusion.  For a longer explanation, please see this blog post by Andrej Bauer.
I have not examined the proof that $\pi$ is transcendental to see whether it can be rephrased as a constructive proof. There are many other issues in classical logic that are nonconstructive, such as the way that "or" is handled, and the way that equality of real numbers is handled. But the mere fact that one proves $\pi$ is transcendental by assuming $\pi$ is algebraic is not a real concern in mathematical constructivism.
