logoalt Hacker News

codebje04/04/20252 repliesview on HN

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


Replies

umanwizard04/04/2025

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

show 1 reply
xpmatteo04/04/2025

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.