In a proof assistant such as Lean, tactics incrementally evolve an incomplete proof until it becomes complete. This builds a search tree. In this talk, I will discuss the tree search formulation of proofs and how this paradigm fails. I will also explain formalizing motivated proofs and the difference between the presentation, search, and kernel views. There will be a demo of using PyPantograph to emulate this search process.