To clarify the last sentence: I am not criticizing mathematicians for not doing formal proofs. Often mathematical publications are not final "products" but explorations into new methods. Requiring formal proofs on every publication, with the status quo of computer-assisted proving, will surely impeded the development of mathematics. What I am saying is that I hope one day with the development of computer-assisted proving, the chores involved in doing formal proofs will be reduced to such a degree that mathematicians are more inclined to do them than not.