Hacker News Reader

Comment by jonnybgood | Hacker News Reader

> 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?

View on HN

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.

> 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.

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.

Got it. This is what I was missing. Thank you.

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.

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.

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

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

Reply on news.ycombinator.com