3 ms·

s/proof/demonstration/ and be done with the arguments. Intuitive but formally wrong is still good for intuition.

xpe 2y ago
Such a visual argument isn't "formally wrong" because it isn't trying or claiming to be a formal proof at all. "Formally wrong" would mean that formal mathematics is used incorrectly.
- layer8 2y ago
  No, “formally wrong” means that it fails formal verification.
  - xpe 2y ago
    >> "Formally wrong" would mean that formal mathematics is used incorrectly. > No, “formally wrong” means that it fails formal verification. The word "formal" has meaning in mathematics independent of formal verification. The latter builds upon the former. Agree? > In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. - Wikipedia https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification Here is how I'm using the terms: - "Formal" in mathematics refers to rigorous logical reasoning with precise definitions and deductive steps. This is the older, more general meaning. - "Formal verification" emerged later as a specific term in computer science referring to automated/mechanical verification of system properties. This is now the standard meaning in software/hardware contexts. So, putting these terms into use... If a human verifies a formal proof "by hand", I think it is fair to say that does not comprise "formal verification". On the other hand, if an automated system verifies the proof, then I would say "formal verification" has happened. Perhaps you will agree this is how many, if not most, experts use the terms. Are we mostly playing language games -- or is there a key insight you think I don't understand?
    - layer8 2y ago
      You can perform a formal verification of an informal proof, like for example the ones in https://youtu.be/VYQVlVoWoPY https://youtu.be/VYQVlVoWoPY linked elsethread. Of course, you have to come up with some formalization of what the informal proof is trying to claim, but it doesn’t mean that what you’re proving wrong must be a formal proof to start with.
      - xpe 2y ago
        Yes, I understand what you mean. We don't disagree on the substance.
        layer8 2y ago
        It therefore makes sense to me (and represents actual usage of those terms) to say that some informal proof is formally wrong, meaning that translating its reasoning into a formal representation will reveal its incorrectness.
- xpe 2y ago
  Analogously, one wouldn't call a mathematical proof "visually wrong" simply because it lacked visual diagrams.
lupire 2y ago
Quod erat demonstrandum.

xpe 2y ago

Such a visual argument isn't "formally wrong" because it isn't trying or claiming to be a formal proof at all. "Formally wrong" would mean that formal mathematics is used incorrectly.

layer8 2y ago
No, “formally wrong” means that it fails formal verification.
- xpe 2y ago
  >> "Formally wrong" would mean that formal mathematics is used incorrectly. > No, “formally wrong” means that it fails formal verification. The word "formal" has meaning in mathematics independent of formal verification. The latter builds upon the former. Agree? > In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. - Wikipedia https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification Here is how I'm using the terms: - "Formal" in mathematics refers to rigorous logical reasoning with precise definitions and deductive steps. This is the older, more general meaning. - "Formal verification" emerged later as a specific term in computer science referring to automated/mechanical verification of system properties. This is now the standard meaning in software/hardware contexts. So, putting these terms into use... If a human verifies a formal proof "by hand", I think it is fair to say that does not comprise "formal verification". On the other hand, if an automated system verifies the proof, then I would say "formal verification" has happened. Perhaps you will agree this is how many, if not most, experts use the terms. Are we mostly playing language games -- or is there a key insight you think I don't understand?
  - layer8 2y ago
    You can perform a formal verification of an informal proof, like for example the ones in https://youtu.be/VYQVlVoWoPY https://youtu.be/VYQVlVoWoPY linked elsethread. Of course, you have to come up with some formalization of what the informal proof is trying to claim, but it doesn’t mean that what you’re proving wrong must be a formal proof to start with.
    - xpe 2y ago
      Yes, I understand what you mean. We don't disagree on the substance.
      - layer8 2y ago
        It therefore makes sense to me (and represents actual usage of those terms) to say that some informal proof is formally wrong, meaning that translating its reasoning into a formal representation will reveal its incorrectness.
xpe 2y ago
Analogously, one wouldn't call a mathematical proof "visually wrong" simply because it lacked visual diagrams.

lupire 2y ago

Quod erat demonstrandum.