A point that is maybe not obvious to people who have not done mathematics at a high level or done βnewβ mathematics, is that often you end of changing your theorem or at least lemmas and definitions while figuring out the proof. That is, you have something you want to prove, but maybe it is easier to proving something more general or maybe your definitions need to change slightly. Anecdotally, during a project I spend perhaps a year figuring out exactly the right definition for a problem to be able to prove it. Of course, this was a very new thing. For well-know areas it is often straight forward, but at the frontier, both definitions and theorems often change as your proceed and understand the problem better.