This may depend sensitively on the subject area. My impression (or perhaps my prejudice) is that proofs in certain areas, like geometric topology, are much farther from being formalized than proofs in most other areas of mathematics.