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.)
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:
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).
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.
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.)
Can you give an example of the type of theorem or proof you're talking about?
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:
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.
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:
(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).
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.