5 ms·
What’s the purpose of automated theorem provers? Seems to take the fun out of proofs
by imranq 7y ago
What’s the purpose of automated theorem provers? Seems to take the fun out of proofs
- brohee 7y agoEnsuring the proof is actually one https://www.quantamagazine.org/in-computers-we-trust-20130222/ https://www.quantamagazine.org/in-computers-we-trust-2013022...
- imranq 7y agoThanks, I'd imagine an extremely small number of proofs could be verified this way
- brohee 7y agoThere are archives of formal proofs that are quite big, e.g. https://www.isa-afp.org/ https://www.isa-afp.org/ for Isabelle, https://github.com/UniMath https://github.com/UniMath for Coq
- imranq 7y agoThanks! This is really fascinating for me, i had never heard of this way of doing proofs and I studied math in college
- cvoss 7y agoThere's an important distinction (spectrum?) between automated theorem provers and proof assistants. Coq is a proof assistant, which means that any automation is there to try to help the programmer by clearing away the tedious parts and leaving only the creative, fun parts. At the end of the day, it's still a human writing a proof. Afterward, Coq ultimately verifies the proof's integrity, which is an easy mechanical operation.
- pliftkl 7y agoWhile coq is an automated theorem prover, I've had a tremendous amount of fun working my way through Software Foundations[1]. The vast majority of the proofs are assembled "by hand", but with coq verifying steps. For someone like me who has a "late in life" fascination with mathematics, doing proofs using coq has been fantastic. [1] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/