Proof Assistants/Interactive Theorem Provers: Any recommendations?
March 10, 2017 at 2:20 am
(This post was last modified: March 10, 2017 at 2:28 am by Kernel Sohcahtoa.)
Background
Hello everyone. I'm a math autodidact, and over the past year, I've been learning areas of math that are more theoretical/proof-based. Now, I've observed that a lot of the books that I'm using do not have much in the way of solutions/solutions manuals: there's usually a very limited selection of worked out proofs (many of them just offer hints), and many times, my proof is not a mirror image of the book's proof. Hence, while I'd love to tackle most of the exercises in the books that I'm using (I usually try do a decent chunk), I'm hesitant to do so, because without a reliable way to ensure that my thinking is precise, I don't want to risk reinforcing faulty logic and incorrect mathematical reasoning on my part. Consequently, as a remedy to this problem, I have perused sites like math stack exchange in order to see how particular proofs are done (this is helpful, but it is limited to what has been posted on the net by others), and I have posted proofs online (mostly on yahoo answers) for others to check and see if my proofs are correct.
Proof Assistants (PAs)?
With that said, I'd like to expand my resource base. Thus, I've recently heard about proof assistants/interactive theorem provers and was curious if anyone here knows much about them. Do you think they are helpful in improving/strengthening one's mathematical reasoning as it relates to writing logical and correct math proofs? Can they help one improve his or her proof-writing ability? In order to effectively use proof assistants, must one possess a lot of computer skills and be familiar with various codes? Would special software be required in order to use PAs?
Thanks for your time and attention, and I'd be grateful for any insights that anyone has on this? Live long and prosper.
Hello everyone. I'm a math autodidact, and over the past year, I've been learning areas of math that are more theoretical/proof-based. Now, I've observed that a lot of the books that I'm using do not have much in the way of solutions/solutions manuals: there's usually a very limited selection of worked out proofs (many of them just offer hints), and many times, my proof is not a mirror image of the book's proof. Hence, while I'd love to tackle most of the exercises in the books that I'm using (I usually try do a decent chunk), I'm hesitant to do so, because without a reliable way to ensure that my thinking is precise, I don't want to risk reinforcing faulty logic and incorrect mathematical reasoning on my part. Consequently, as a remedy to this problem, I have perused sites like math stack exchange in order to see how particular proofs are done (this is helpful, but it is limited to what has been posted on the net by others), and I have posted proofs online (mostly on yahoo answers) for others to check and see if my proofs are correct.
Proof Assistants (PAs)?
With that said, I'd like to expand my resource base. Thus, I've recently heard about proof assistants/interactive theorem provers and was curious if anyone here knows much about them. Do you think they are helpful in improving/strengthening one's mathematical reasoning as it relates to writing logical and correct math proofs? Can they help one improve his or her proof-writing ability? In order to effectively use proof assistants, must one possess a lot of computer skills and be familiar with various codes? Would special software be required in order to use PAs?
Thanks for your time and attention, and I'd be grateful for any insights that anyone has on this? Live long and prosper.
