A lovely image here for the interplay between formal and informal reasoning that characterises even the purest of mathematics:
A fully formal proof of the Lee–Yang circle theorem would be very long and quite unreadable and uncheckable by a human mathematician. One could say that human mathematics is a sort of dance around such a formal text: one gives a convincing argument that it could be written, but one does not write it.
The problem of how formally one ought to argue — how close to the formal text one ought to dance — is one that most of us first encounter when facing exam questions. It may or may not be reassuring to know that it never really goes away…