3 ms·

> Technically, a proof communicated in spoken language is an informal proof, and this is how nearly all proofs in mathematics are conveyed. That doesn't sound

> Technically, a proof communicated in spoken language is an informal proof, and this is how nearly all proofs in mathematics are conveyed. That doesn't sound right. Nearly all proofs are communicated in a written formal language. That's completely different than spoken language. Am I missing something?

zeroxfe 10y ago
This is not that uncommon -- e.g., most proofs of the undecidability of the halting problem.
ambulancechaser 10y ago
its a pedantic point but most proofs are handwavy in the sense that they don't show which rule of inference allows them to claim a particular intermediary result. Proving anything but the most trivial thing where every single deduction is made is quite tedious, but the sentiment is correct.
adrianratnapala 10y ago
I think you should almost replace "spoken language" in that quote with "natural language". As opposed to a formal syntax like used by Russel and Walllace -- or indeed any programming language. I say "almost replace" because even natural languages can be restricted into formal versions good enough for proofs. People have been playing that game since Aristotle and his sylogisms.
cscurmudgeon 10y ago
Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Formal here is not "Mathy and jargony and with a lot of greek symbols" as is understood normally.
- jonnybgood 10y ago
  > Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Right. That's the formal I'm also referring to.
  - catnaroek 10y ago
    Mathematical papers are seldom written fully formally. This is in no small part because the most commonly accepted foundation of mathematics (ZFC atop first-order logic) was only designed to make formalization possible “in principle”. It's precisely because of this that researchers in formal verification are looking for systems that make formalization actually possible in practice, such as various flavors of type theory.
    - jonnybgood 10y ago
      Got it. This is what I was missing. Thank you.
jk4930 10y ago
Compare a proof in a text book or most papers with this: http://us.metamath.org/mpegif/mmset.html http://us.metamath.org/mpegif/mmset.html

zeroxfe 10y ago

This is not that uncommon -- e.g., most proofs of the undecidability of the halting problem.

ambulancechaser 10y ago

its a pedantic point but most proofs are handwavy in the sense that they don't show which rule of inference allows them to claim a particular intermediary result. Proving anything but the most trivial thing where every single deduction is made is quite tedious, but the sentiment is correct.

adrianratnapala 10y ago

I think you should almost replace "spoken language" in that quote with "natural language". As opposed to a formal syntax like used by Russel and Walllace -- or indeed any programming language. I say "almost replace" because even natural languages can be restricted into formal versions good enough for proofs. People have been playing that game since Aristotle and his sylogisms.

cscurmudgeon 10y ago

Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Formal here is not "Mathy and jargony and with a lot of greek symbols" as is understood normally.

jonnybgood 10y ago
> Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Right. That's the formal I'm also referring to.
- catnaroek 10y ago
  Mathematical papers are seldom written fully formally. This is in no small part because the most commonly accepted foundation of mathematics (ZFC atop first-order logic) was only designed to make formalization possible “in principle”. It's precisely because of this that researchers in formal verification are looking for systems that make formalization actually possible in practice, such as various flavors of type theory.
  - jonnybgood 10y ago
    Got it. This is what I was missing. Thank you.

jk4930 10y ago

Compare a proof in a text book or most papers with this: http://us.metamath.org/mpegif/mmset.html http://us.metamath.org/mpegif/mmset.html