> When I’m trying to write a proof, I think of the definitions and theorems as my standard library. I look at the conclusion of the theorem to prove as the result I need to obtain and then think about how to build it using my library.

fwiw, this is exactly the thing that you when you're trying to formally prove some theorem in a language like Lean.