Remix clone Hacker News

Theorems and proofs are almost never written in formal symbolic language.

▲ codebje 15 days ago | parent [-]

My experience in reading computer science papers is almost exactly the opposite of yours: theorems are almost always written in formal symbolic language. Proofs vary more, from brief prose sketching a simple proof to critical components of proofs given symbolically with prose tying it together.

(Uncommonly, some papers - mostly those related to type theory - go so far as to reference hundreds of lines of machine verified symbolic proofs.)

▲ umanwizard 15 days ago | parent | next [-]

Can you give an example of the type of theorem or proof you're talking about?

	▲	codebje 15 days ago \| parent [-]
		Here's one paper covering the derivation of a typed functional LALR(1) parser in which derivations are given explicitly in symbolic language, while proofs are just prose claims that an inductive proof is similar to the derivation: `https://scholar.google.com/scholar?&q=Hinze%2C%20R.%2C%20Paterson%2C%20R.%3A%20Derivation%20of%20a%20typed%20functional%20LR%20parser%20%282003%29` Here's one for the semantics of the Cedille functional language core in which proofs are given as key components in symbolic language with prose to to tie them together; all theorems, lemmas, etc are given symbolically. `https://arxiv.org/abs/1806.04709` And here's one introducing dependent intersection types (as used in Cedille) which references formal machine-checked proofs and only provides a sketch of the proof result in prose: `https://doi.org/10.1109/LICS.2003.1210048` (For the latter, actually finding the machine checked proof might be tricky: I didn't see it overtly cited and I didn't go looking).

▲ xpmatteo 14 days ago | parent | prev [-]

Common expressions such as f = O(n) are not formal at all -- the "=" symbol does not represent equality, and the "n" symbol does not represent a number.