Background: An issue in my math study is that I haven't found a good way of storing the theorems ( mostly abstract algebra ) I studied and want to (re-)use in proofs. At the moment I use a personal Wiki and LaTeX but that doesn't -do- much for me. So I am thinking of investing time in learning an automated theorem prover package to which I am fairly newbie at the moment. A first Google search lead me to ACL2, Isabelle and Prover9 and that's where the confusion starts.
Question: - Given my requirements of documenting and re-using theorems which software tool is a good option to use? ( I have done a mathematical logic course already. )