I feel like the analogy would be "writing mathematical proofs without writing down any of the propositions" (And indeed, the Curry-Howard correspondence lends credence to this). Writing down types for programs is not just useful because the computer can check them, but also because it commits what is in one's mind.

What's more, type-checkers offer a lot more help in checking types than Coq does at proving mathematical propositions (There is a reason, after all, that one is an assistant, whereas the other is a checker), so, relatively speaking, writing a proof without Coq is not as hard as typing a program without a type-checker.