Timeline for Non-trivial difference(s) between Computer Algebra System and Proof Assistant
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 9, 2022 at 18:51 | comment | added | Will Sawin | @MikeShulman Sure - my point is just that saying "machinery to produce proofs" admits multiple interpretation depending on your view of what a proof is. I thought what I said in the body of my answer, talking about formal proofs, the formal system they're written in, the kernel that verifies them, and the rest of the proof assistant that helps you produce them, was more precise. | |
| Feb 9, 2022 at 18:33 | comment | added | Mike Shulman | Hmm, I think I'd use a different word than "produced" there. | |
| Feb 9, 2022 at 18:19 | comment | added | Will Sawin | @MikeShulman I mean when someone writes in a paper Lemma 3.7 and in the proof it says "This was checked in Magma", that's a (informal) proof produced by a CAS. | |
| Feb 9, 2022 at 18:11 | comment | added | Mike Shulman | @WillSawin I wouldn't count a CAS doing a computation using an algorithm that is justified by a separate proof external to the CAS as the CAS "producing a proof". Is there some other sense in which you would say that they do? | |
| Feb 8, 2022 at 20:31 | comment | added | Will Sawin | @AgnishomChattopadhyay Well, what is a proof? If the answer is "anything mathematicians accept as a proof" then CASs do form proofs. If the answer is "anything accepted by the trusted kernel" than they don't. | |
| Feb 8, 2022 at 20:27 | comment | added | Agnishom Chattopadhyay | The key point is that Computer Algebra Systems are not typically equipped with machinery to produce proofs. For example, mathematica can tell me that the sum of the first n integers is n*(n+1)/2, but it will not produce a proof of why this is the case. | |
| S Feb 8, 2022 at 20:24 | review | First answers | |||
| Feb 9, 2022 at 0:06 | |||||
| S Feb 8, 2022 at 20:24 | history | answered | Will Sawin | CC BY-SA 4.0 |