2
$\begingroup$

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. )

  • 2
    @ndroock1: I think "near future" is very optimistic. Look at any paper submitted to a mathematical journal, or any mathematics textbook. In my view, your wish to "document" theorems is just a means to the goal of learning them – you have not really understood a theorem until you know how to use it!2012-02-12

0 Answers 0