Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
Aotomated Theorem Proving – pedja Feb 12 '12 at 10:07
Thanks @pedja but from my perspective this only adds to the confusion. I don't want to follow dead tracks. – nilo de roock Feb 12 '12 at 10:10
@ndroock1: Automated theorem proving is about proving theorems in the sense of mathematical logic. Given that the vast majority of mathematicians do not write their proofs in formal systems, I think it is highly unlikely that an automatic theorem prover will be able to help you learn mathematics. – Zhen Lin Feb 12 '12 at 11:32
@ZhenLin - My issue is not learning the theorems, but documenting them in a -productive- way. I read from the Isabelle project that it may become a requirement in the near future that when a paper is submitted to a journal the proofs should be readable by a formal system. – nilo de roock Feb 12 '12 at 12:53
@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! – Zhen Lin Feb 12 '12 at 13:03

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.