Have seen long proofs in articles some with $15$+ lemmas for a single theorem. How does a writer keep track of and manage so many lemmas?

Question

When someone sets out to prove a theorem, they may be able to see for example a couple results that if proven could give them the theorem. But I don't see how anyone could mentally grasp dozens of lemmas/identities and simultaneously fit them together in their head to show they can be used to prove the original theorem. So then how is it that researchers come up with all these lemmas for their theorem? Do they just jot down any identity/interesting property they come across and compile loads of stuff, and then later go back and see if any of it fits together? Also while putting the pieces together so to speak, how are they handling the lemmas/identities? I imagine they are going to want to be able to look at all of them or multiple ones quickly, so it wouldn't be efficient to have each one saved as a separate file with $15+$ open at once. Do people have relevant lemmas/theorems etc. all saved in a single file for viewing when they are writing papers, or what? How does one manage all that information.

Answer 1

Here's a variation on the cycle described by @TheSimpliFire. This is not so much a "cycle" as it is a "tree" or a "recursion". I also think of this as the "top down" method of proof writing.

For the first step of the recursion, write down the theorem you want to prove. Then write down a very short proof, 2 or 3 or 4 steps. Each of those steps may include its own clearly stated but as-yet-unproven lemma (although sometimes the proof of a step can be completed without any unproven lemma). So now your original theorem has been reduced to 2 or 3 or 4 unproven lemmas.

For the next step of the recursion, repeat the previous step for each of the 2 or 3 or 4 unproven lemmas: write a very short proof of each lemma, breaking it into a small number of steps, each step of which may include its own clearly stated but as-yet-unproven lemma.

Continue the process. If you do this well, the number of unproven lemmas will not increase exponentially, although it may indeed grow into 15+ lemmas before the proof approaches the end.

Also, there is one thing to keep in mind. As you write your proof, you have the entire history of written mathematics to draw on, a deep and rich tradition of proved theorems which you may apply.

Answer 2

It is very difficult. But a good way to do it is to work backwards.

Here's a kind of cycle:

• Start from the result you're trying to prove.

• Find a relevant formula. (this is the hard part)

• Use it to manipulate the result into a simpler expression. (this is usually indicated by 'thus it suffices to prove that...')

• Repeat.

Sometimes it is possible to skip step two entirely.

An example is Chapter 7 of Apostol's Introduction to Analytic Number Theory, with no fewer than eight lemmas.

Answer 3

I think that more experienced math-research people have already assimilated most of those "lemmas", in some form or other, so that their mental processes do not have to treat them as "new" things, nor as "things to remember". Rather, those "lemmas" are not thought of as "lemmas" at all, but as true, observable (!) facts about the environment. So they are mostly subliminal, rather than occupying space in one's conscious mind.

Some of the weirdness of the writing style in mathematics is that the conventional organization is, indeed, to organize things in a way that is logically ordered, while perhaps counter-intuitive (and very different from the order of events in discovery). So part of the answer is "how do people deal with this weird organization" is that they don't, really, but just formulate things that way after everything is settled.

Similarly, as to a question "how would anyone know what to do next?", the answer often is that the actual order of events was entirely different, and that specific issue never arose... although the re-ordered version of things might strongly suggest that it does/did.