Do you ever use formal logic when working on proofs?

When I'm writing to a proof I use formal way. I do this because I find it easier to remember like this, using that way makes me think about how to write each step and thus makes me remember it better. Another advantage I think it has is that writing formally makes you read formally better which is great thing to know.

When I'm explaining something, giving hints, brainstorm etc. I prefer to use natural way, because I think that it gives you the advantages of understanding "why it is like it is" and not only the "how you get to that".

I mostly rely on what you call 'mathematical natural language', as it usually better 'fits' my conceptual ways to think about a problem, but there are definitely times when I work something out in formal logic to better grasp some of the details, e.g so I can see the difference between a $\forall x \exists y ...$ and a $\exists y \forall x ...$, for example.

Thus, as with most things like this, sometimes one representation is more helpful, and at other times a different representation is more helpful. Cognitively this makes sense: representations cue us to proceed in certain ways, and so different representations can cue us differently. So that's exactly why you sometimes get stuck using one representation, but 'see the light' when using the other one, and vice versa.

Basically never, it's both too slow and too hard to read. The point of learning formal logic isn't to use formal logic (unless you then go on to work in logic, where you will be writing proofs in natural language about logic), it's to train habits of thought and get you to clarify your thinking both to yourself and to others; a simple example is being able to instantly negate a universal quantifier to get an existential quantifier and vice versa (which everyone knows everyone else can do and hence which nobody will explicitly mention that they're doing). Once you've ingrained the relevant habits you don't need the formal logic anymore.

See also Terence Tao's description of the pre-rigorous, rigorous, and post-rigorous stages of learning math.

Recently, I wrote a paper, where almost all the proofs are in the level of formality which you refer as "2. Using formal logic...". However, the work is from foundations of mathematics, where formality is easier, but also necessary. I myself, prefer to read formal, precise statements than these in natural language; I just grasp the formal expressions faster. Also, many results come to me symbolically; I did not see them intuitively. Also, intuitive and habitual thinking may be sometimes very misleading. The difficulties connected to expressing complicated statements in a formal way can be overcome by sufficient number of formal definitions. Clearly, a text is easier to comprehend when such definitions have a "nice" intuitive interpretation.

I think all depends on the author: one people prefer to use intuitive, habitual thinking and natural language, other like to read formal statements and think symbolically. Hence, I think each mathematician should be allowed to work in his own style, and there is no "the only correct way".

If you are a type theorist, then doing so is part of the math itself, so in that case the answer is a resounding yes!

One theme of type theory is that it describes partly (but more deliberately than any other branch) how to mechanize a mathematician using a computer program.

So pretend this is 100 years into the future and someone has put Qiaochu Yuan's math personality into a computer. Well, if the computer works the way that type theory outlines that it should work, then internally, yes the computer is using directly these formal expressions, but what does the human see it doing? Well this is 100 years into the future, so surely someone has invented a human-readable interface to the logic engine's internals. A feature of this would be that it makes conceptual leaps syntactically at least, much like a human does.

So is the machine doing math in way 1 or way 2?

So now, imagine that the human being is abstractly the same thing as a computer when it comes to math. Then are they not doing internally the same thing? And if not, did they not once do each logical step internally, and memorize the result in such a way that it can be used in an intuitionistic way later? It would not be hard, 100 years from now, to make a machine do the same thing. As today, there are millions of biological machines already doing it.