Is there some method to do mathematical deduction on computer instead of with pen?

Question

Sorry if this question is not too fit into the website. I want to know if there're some methods that we can actually do mathematical deduction with formulae just on the computer instead of with pen and paper? I think latex is not a what you see is what you get type of way, so it might not be a good choice to do the mathematical deduction, so is there some other ways?

Answer 1

I can come up with several ways to do so:

• Using an electronic pen, so that ones writings are directly processed digitally.
• Using a markup language of ones choice to type math with a keyboard or other input device (including speech or maybe thought recognition)
• Use what you see is what you get editors, for instance some peoples beloved Word processor

But all what I listed is just obvious I guess. If you mean also to have computer aided mathematical arguments, sure there are many tools: Mathematica, Maple, Matlab,... or languages like Prolog, Haskell or all others like C++, Python, Fortran, Java,... with the desired libraries.

But if you mean to have some software which is doing the proofs for us, or which finds new mathematical results, then the big question would be: is it still mathematics and how does it help us? Since mathematics seems to me, at least in our world, mostly about humans understanding some mathematical idea/principle/law and not about a machine telling us some results which we cannot comprehend, no matter if true or not.

Edit: I would like to add IPE, extensible drawing editor, which can render Latex and is very nice for doing presentations, which is an essential part of teaching or communicating mathematics and also a way of deduction