The following comment was recently posted on one of my YouTube videos (a session I ran a few years back on “How do we do proofs?” , available at https://www.youtube.com/watch?v=T3ti6-l7cNk)
“Why do people who write proofs use confusing language like ‘let’, ‘consider’ (instead of ‘if’, ‘look’) etc.? Why do they write their proofs backwards, like they found it from thin air?”
My reply (with a couple of typos corrected!) was:
I think we might disagree about the meanings of “backwards” and “forwards”. Mathematical reasoning often has a specific direction, and not all steps in the proof are reversible. Proofs are often discovered working backwards from the destination (almost like some mazes are easier to solve that way), but the logic of the final argument must point in the correct direction. If you try to prove something by making deductions from the desired conclusion, you won’t have proved that conclusion unless all of your reasoning is reversible. (You can see some sample warnings about “backwards reasoning” in my Foundations of Pure Mathematics classes.) However, it is allowed to say “Y would follow if we could only prove X.” and then prove X, as long as you don’t use Y to prove X. So you can rewrite most proofs to fit more closely with the way they are discovered.
On the other hand, sometimes, perhaps like in a game of chess, there are only a limited number of sensible options for what information or tool you might use next. Here experience and fluency play a role: a strong chess player will usually focus quickly on a relatively small number of likely moves from what could appear to be a bewildering number of options.
Correct use of “let” or “suppose” is a very important (and traditional) tool when you want to prove that something is true for ALL examples of a particular kind. You can think of it as an abbreviation for the following ideas. “We want to show that [an interesting fact] is true for ALL things of type A. So what we need to show is that, if we have something of type A then [an interesting fact] is true for that thing. As long as we only assume the thing is of type A, and nothing else, then our proof will be valid for all things of type A. So, let x be an arbitrary thing of type A. We’ll show that just using the assumption that x is of type A, and no extra assumptions, we can still show that [an interesting fact] is true for x. Because we made no other assumptions about x, our argument will show that [an interesting fact] is true for all things of type A.”
That is the traditional approach. But you could do a lot with “If”, as in “If x is a thing of type A, then …”. But, at least to me, the important thing is to make sure that you really understand the structure of the proof you need. Using traditional language can help when you are using a traditional proof structure, but is not essential as long as the reasoning is correct.