Does there exist a formal language capable of expressing any mathematical proof without resorting to drawings or natural language sentences?

Practically everytime I read a theorem proof in a book, paper, slides, website, pdf, anywhere, the proof is written using natural language (e.g. sentences in English) and sometimes drawings (e.g. 2D drawings if it's a proof about Geometry, Graph Theory, etc.). Even if the author does her/his best at writing a very technical and formal proof, full of formal symbols, at one point or another they can't help but resort to natural language and/or drawings to get some point across. My question is: does there exist a formal language capable of expressing any mathematical proof without resorting to drawings or natural language sentences?

UPDATE: As @Noah Schweber suggested in the comments to his answer, I should make clear that a very important underlying reason for my interest in formal proofs has to do with the issue of confidence in natural language proofs. That is, if we are not using any formal language to prove most theorems, then how can we be so sure that we have proved anything at all? Because, what if we made some mistake at some point during our natural language reasoning? Since we don't have a full symbolic formal proof, how can we truthfully check that our proof is indeed correct? I think this is a very valid concern considering that natural languages are incredibly prone to ambiguities, which I guess most would agree is an undesirable property when we want to prove mathematical statements with crystal clear certainty.

• "they can't help it but..." seems to indicate that there is something undesirable about using natural language and/or drawings. – Lee Mosher May 9 '18 at 1:17
• Just try to express everything with symbols only. I take it your background in math is strong enough to understand mathematical books, so you will be familiar with all the atomic symbols required to define new symbols and finally write every proof that way. There is not really a need for any "special" language other than the well known symbols from logic / set theory. I am not an expert on this but I have found you can get pretty "atomic" in formalizing proofs even without a background in formal languages. Bottomline: Authors could write that style, but nobody would want to buy such books... – mol3574710n0fN074710n May 9 '18 at 1:19
• @mol3574710n0fN074710n, do you know any examples of proofs written 100% without using natural language / drawings? – xwb May 9 '18 at 1:20
• @xwb Have you heard of Principia Mathematica? – Noah Schweber May 9 '18 at 1:21
• Without any language? Not really, I avoid such things, don't like. I used to troll some of my tutors by writing the homework that way during the second or third year as a student... - Did not always go down well! XD – mol3574710n0fN074710n May 9 '18 at 1:29

at one point or another they can't help it but resort to natural language and/or drawings to get some point across. My question is: does there exist a formal language capable of expressing any mathematical proof without resorting to drawings or natural language sentences?

I think you're misunderstanding the goal of the text: it's to explain the result to the reader. Proofs are presented using natural language and occasionally pictures in order to be better understood by the reader.

For what it's worth, I don't mean to imply that the desire for a fully formal proof is bad. You may be interested in$^*$ mathematical logic in general (and in particular the syntax of first-order logic and set theory); more specifically, I think both formal (= machine-verifiable) proof and automated theorem proving will be of interest to you. But it's important to keep in mind the fact that mathematical texts (tend to) seek to explain mathematics to the reader, and so - even if one has a purely formal proof in hand - need to make concessions to how humans actually learn.

As a historical note, you may be interested in the book Principia Mathematica by Russell and Whitehead. More modern sources you might be interested in reading, on the issue of certainty in mathematics (as you've clarified in your comments below), include the following:

And there are many others, found quickly by googling the relevant terms. It's a big and important problem!

$^*$I don't mean to imply that texts on mathematical logic will be written in the way you want - indeed, like other mathematical texts they're trying to explain something to the reader, so use natural language - but the subject itself has a lot to say about formal proofs as mathematical objects, and the formal languages developed and studied in mathematical logic are capable of faithfully expressing mathematical theorems and proofs.

• So, for example, would it be possible to write a full proof of the correctness of Dijkstra algorithm for finding the shortest path using only first-order logic and set theory? What would that look like? Do you know any examples of proofs written like that, by any chance? – xwb May 9 '18 at 1:28
• @xwb Yes, although I don't know why anyone ever would. As to what it would look like: long. I think you'll find the most interesting information if you read about formal proof verification and automated theorem proving. – Noah Schweber May 9 '18 at 1:31
• So if we are not using any formal language to prove most theorems, then how can we be so sure that we have proved anything at all? I mean, what if we made some mistake at some point during our natural language reasoning? Since we don't have a full symbolic proof, how can we truthfully check that our proof is correct? – xwb May 9 '18 at 1:37
• @xwb This is a reasonable - and in my opinion, very serious - concern, and indeed mistakes are found sometimes in claimed proofs. Which is one reason that machine-checkable (= computer-verifiable) proofs are so important. Which is why I recommended the topic to you. However, the idea that more formal = more accurate is far less true than it appears: looking online you'll quickly find lots of cranky math papers claiming to prove (say) the consistency of PA inside PA, which consist of pages upon pages of pure symbol-juggling. (cont'd) – Noah Schweber May 9 '18 at 1:44
• This sort of mess is practically unreadable to a person, and indeed it's very easy for the author to make a small typo somewhere and never notice. As far as human-generated mathematics goes, using natural language is necessary for the reader to actually understand what's happening. This situation changes immediately once we introduce computers into the mix, of course, but that's a recent (well, relatively) phenomenon. The idea of purely formal proof predates computers (and in particular is absolutely necessary to even state, say, the completeness theorem of logic) ... – Noah Schweber May 9 '18 at 1:46