2 ms·

Related to this, I wish someone had a simple course on this for people who don’t know that much about (automated) proofs. I looked it up on HN [1], but couldn’

Related to this, I wish someone had a simple course on this for people who don’t know that much about (automated) proofs. I looked it up on HN [1], but couldn’t find any. [1] https://hn.algolia.com/?q=proof+assistant https://hn.algolia.com/?q=proof+assistant

Someone 7y ago
If you don’t know much about proofs, you first have to learn how incredibly good mathematicians are at nitpicking (if they want to), and you have to accept that that is a good thing. Thing is, if you want to be rigorous, you cannot accept anything as true, except for the axioms you’re working from, and you want as few and as simple as possible of those because that decreases the risk that your starting set is internally inconsistent. You also want every single step in your proof to be absolutely bloody obvious. For example, if you want to build math from the ground up, you don’t accept that integer multiplication or even integer addition exist, but you construct them. In fact, you don’t even accept that integers exist; you construct them, for example from natural numbers (https://en.wikipedia.org/wiki/Integer#Construction https://en.wikipedia.org/wiki/Integer#Construction) Starting with the absolute basics also allows you to pick and choose which axioms to start with, for example by not including the law of the excluded middle (https://en.wikipedia.org/wiki/Law_of_excluded_middle#Logicists_versus_the_intuitionists https://en.wikipedia.org/wiki/Law_of_excluded_middle#Logicis...) or the parallel postulate (https://en.wikipedia.org/wiki/Parallel_postulate#History https://en.wikipedia.org/wiki/Parallel_postulate#History) For learning how deep that nitpicking can go, http://us.metamath.org/index.html http://us.metamath.org/index.html (A proof assistent that is, IMO, simpler to understand than many other ones, but has really, really long proofs) may be illustrative. See for example their proof that 2+2=4. Once you accept that every detail needs your full attention, I think https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/ has a decent introduction. If you just want an introduction to _a_ theorem prover, http://www.cs.ru.nl/~freek/comparison/comparison.pdf http://www.cs.ru.nl/~freek/comparison/comparison.pdf (discusses 17 different ones) also may be useful.

Someone 7y ago

If you don’t know much about proofs, you first have to learn how incredibly good mathematicians are at nitpicking (if they want to), and you have to accept that that is a good thing. Thing is, if you want to be rigorous, you cannot accept anything as true, except for the axioms you’re working from, and you want as few and as simple as possible of those because that decreases the risk that your starting set is internally inconsistent. You also want every single step in your proof to be absolutely bloody obvious. For example, if you want to build math from the ground up, you don’t accept that integer multiplication or even integer addition exist, but you construct them. In fact, you don’t even accept that integers exist; you construct them, for example from natural numbers (https://en.wikipedia.org/wiki/Integer#Construction https://en.wikipedia.org/wiki/Integer#Construction) Starting with the absolute basics also allows you to pick and choose which axioms to start with, for example by not including the law of the excluded middle (https://en.wikipedia.org/wiki/Law_of_excluded_middle#Logicists_versus_the_intuitionists https://en.wikipedia.org/wiki/Law_of_excluded_middle#Logicis...) or the parallel postulate (https://en.wikipedia.org/wiki/Parallel_postulate#History https://en.wikipedia.org/wiki/Parallel_postulate#History) For learning how deep that nitpicking can go, http://us.metamath.org/index.html http://us.metamath.org/index.html (A proof assistent that is, IMO, simpler to understand than many other ones, but has really, really long proofs) may be illustrative. See for example their proof that 2+2=4. Once you accept that every detail needs your full attention, I think https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/ has a decent introduction. If you just want an introduction to _a_ theorem prover, http://www.cs.ru.nl/~freek/comparison/comparison.pdf http://www.cs.ru.nl/~freek/comparison/comparison.pdf (discusses 17 different ones) also may be useful.