It's like solving a maze or exploring a dungeon. Exploring from the start might find something interesting, but having an interesting goal in mind can suggest a possible path and is a guarantee that the proof is rewarding. Whereas untargeted exploration can end up somewhere more surprising and fun, but also less likely to generate anything interesting.

> I don't usually start with a statement I want and then look to prove it, it's more like I explore various derivations to see where they lead (probably with some kind of hunches), and then some of them end up in an interesting place.

You can work this way in Lean. You need to have a goal to make the engine happy, but there's no need for the goal to be true -- you can just do something like

    have h : ∀x, ∀y, x = y := by
      -- h is not true, but in the attempt to prove it,
      -- we can do whatever we want.
      -- If we find something interesting, we can redefine h

Maybe what you are saying is that you want to use the proof assistant like a computer algebra system. You apply correct transformations, and so you are at the same time proving and exploring.

I would agree that this aspect is underdeveloped in proof assistants. At the root of it is that people believe that logic is different from algebra, while it really isn't.

This is an interesting perspective. I've recently been playing with sequent calculus, and I'm writing everything upside-down because I'm starting with the statement to prove and applying the derivations mechanically to produce the proof tree.

But hearing how you approach proofs makes the standard directionality make much more sense.