3 ms·
Can anyone here comment on what kinds of proofs coq is a good tool for, and what kinds of proofs are impractically hard for it to handle? I'm aware that most pr
by abeppu 7y ago
Can anyone here comment on what kinds of proofs coq is a good tool for, and what kinds of proofs are impractically hard for it to handle? I'm aware that most proofs aren't formalized, and now and again we hear that mathematicians spend a long time trying to assess whether a proof has errors. From that, I infer that there are proof approaches that are challenging to capture in tools like this (or else any proof not obviously correct could be formalised to resolve the issue). What are those hard-to-capture techniques?
- philzook 7y agoYou may be interested in a recent survey "QED at Large: A Survey of Engineering of Formally Verified Software" https://www.nowpublishers.com/article/Details/PGL-045 https://www.nowpublishers.com/article/Details/PGL-045 (have to sign up for a free account to access :\ )
- wuschel 7y agoHi, signed up for a free account, but access was not granted. Email is in my profile, if you would be so kind to help.
- alimw 7y agoThe big limitation of Coq is a limitation common to all proof assistants. It takes a lot of time and effort to formalise even simple mathematical ideas, so complex ones can seem quite beyond reach. However if a proof requires the analysis of more cases than a human could comfortably handle, as in the four colour theorem or the Kepler conjecture, then it is a good candidate. https://en.wikipedia.org/wiki/Proof_by_exhaustion https://en.wikipedia.org/wiki/Proof_by_exhaustion