>> "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
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?
You can perform a formal verification of an informal proof, like for example the ones in 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.
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.
