logoalt Hacker News

umanwizard04/03/20251 replyview on HN

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


Replies

codebje04/04/2025

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

show 2 replies