Our server costs ~$56 per month to run. Please consider donating or becoming a Patron to help keep the site running. Help us gain new members by following us on Twitter and liking our page on Facebook!
Current time: March 19, 2024, 4:12 am

Thread Rating:
  • 0 Vote(s) - 0 Average
  • 1
  • 2
  • 3
  • 4
  • 5
Proof Assistants/Interactive Theorem Provers: Any recommendations?
#1
Proof Assistants/Interactive Theorem Provers: Any recommendations?
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.











Reply
#2
RE: Proof Assistants/Interactive Theorem Provers: Any recommendations?
You're in for a ride! Smile
I had never heard of those PAs, but I've used a neat site where people help out and I think it has a lot of pre-existing material that should help you: https://artofproblemsolving.com/
The community area is huge, it's tremendous, it's awesome. You'll love it. Wink

Then you have good old Wolfram Alpha... this will give you step by step resolutions of whatever you throw at it... not sure about proof of theorems, as I've never thought of using it for that.
https://www.wolframalpha.com/
Reply
#3
RE: Proof Assistants/Interactive Theorem Provers: Any recommendations?
I've never used one. I'd imagine they'd be pretty limiting because most proofs deal with complex constructions with so many logical "moving parts"... but I'd be interested to hear if you have any experience with them...
The fool hath said in his heart, There is a God. They are corrupt, they have done abominable works, there is none that doeth good.
Psalm 14, KJV revised edition

Reply
#4
RE: Proof Assistants/Interactive Theorem Provers: Any recommendations?
Try Coq

https://en.m.wikipedia.org/wiki/Coq

Used for proving four colors theorem.
Slave to the Patriarchy no more
Reply
#5
RE: Proof Assistants/Interactive Theorem Provers: Any recommendations?
This is a bit out of my purview.

When in doubt about something mathematical in CS, I default to googling Haskell <Mathematical concept>
https://wiki.haskell.org/Applications_an...em_provers

Edit: Haskell is a good option in general if you want to improve proof-writting (I am vaguely alluding to things friends of mine in the CS/Mathematics community have told me about haskell, so I can't give you a very definitive answer to "Improving your proof writting".)
http://softwareengineering.stackexchange...he-program
Reply
#6
RE: Proof Assistants/Interactive Theorem Provers: Any recommendations?
I think this is a new one.  No idea if you'll find this useful or not. My maths just isn't that good. Came across it and thought of your thread.

https://ncatlab.org/nlab/show/Globular


Quote:Globular is a web-based proof assistant for finitely-presented semistrict globular higher categories. It allows one to formalize higher-categorical proofs in finitely-presented n-categories, visualize them as string diagrams, and share them with collaborators, or with the world.
Reply
#7
RE: Proof Assistants/Interactive Theorem Provers: Any recommendations?
(March 11, 2017 at 6:09 am)Mathilda Wrote: I think this is a new one.  No idea if you'll find this useful or not. My maths just isn't that good. Came across it and thought of your thread.

https://ncatlab.org/nlab/show/Globular


Quote:Globular is a web-based proof assistant for finitely-presented semistrict globular higher categories. It allows one to formalize higher-categorical proofs in finitely-presented n-categories, visualize them as string diagrams, and share them with collaborators, or with the world.

Thank you for your thoughtful post, Mathilda.  In addition, I appreciate the time and effort that people have put into this thread.  I'm looking forward to giving the suggestions, which have been offered by all of you in this thread, a whirl.  Live long and prosper.











Reply



Possibly Related Threads...
Thread Author Replies Views Last Post
  Techtard recommendations. 5thHorseman 2 1022 July 27, 2012 at 4:57 pm
Last Post: 5thHorseman



Users browsing this thread: 1 Guest(s)