Timeline for Non-trivial difference(s) between Computer Algebra System and Proof Assistant
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 4, 2023 at 14:25 | comment | added | Andrej Bauer | @MichaelBächtold: I misspoke. The semantics of CAS are not ill-defined, they're undefined. CAS does something, but what does it do, precisely? What is the formal mathematical meaning of CAS expressions, for instance? | |
| Apr 3, 2023 at 13:19 | comment | added | Michael Bächtold | I'm curious about these "ill-defined semantics of CAS" and the lack of mathematical meaning of the manipulations CAS carry out. Could you provide some concrete examples or tell me where to look for them? | |
| Feb 18, 2022 at 15:08 | history | edited | taylor.2317 | CC BY-SA 4.0 |
added 2 characters in body
|
| Feb 11, 2022 at 15:59 | vote | accept | prash | ||
| Feb 9, 2022 at 17:26 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
spell checking
|
| Feb 9, 2022 at 17:05 | comment | added | prash | Looks good now. I understand a bit more. | |
| Feb 9, 2022 at 16:15 | comment | added | Andrej Bauer | Is this better? | |
| Feb 9, 2022 at 16:13 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 49 characters in body
|
| Feb 9, 2022 at 16:13 | comment | added | Andrej Bauer | Your question implies that proof assistant only prove logical statements (which you phrased in a slightly unfortunate way mentioning "tautologies"). In reality they are used to define all sorts of elaborate concepts and construct complicated mathematical objects, which is the point of my first paragraph. I have modified it to better reflect the sentiment. | |
| Feb 9, 2022 at 15:11 | comment | added | prash | I like this answer, but could you modify it a little bit? I never meant to imply that proof assistants can only prove tautologies. They prove lots of different things by deriving tautologies. What's proven is whatever hypothesis we started with. Am I right in believing all this, or do the aspects of perfectoid spaces, etc. address this belief of mine too? If so, could you please elaborate on that? | |
| Feb 9, 2022 at 11:00 | comment | added | Gilles 'SO- stop being evil' | @GuyCoder I don't see why this technical concept would appear here. A lot of systems use normal forms for one reason or another, but this is an irrelevant detail from the perspective of this question. | |
| Feb 8, 2022 at 22:20 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 212 characters in body
|
| Feb 8, 2022 at 22:18 | comment | added | Andrej Bauer | Normal forms are overrated. | |
| Feb 8, 2022 at 21:56 | history | answered | Andrej Bauer | CC BY-SA 4.0 |