It's less useful, because humans make fewer mistakes and take longer to turn their thoughts into Lean. I think most mathematicians have a higher success rate thinking about the problem informally, poking at it themselves, then formalizing it iteratively to make it more watertight as they gain confidence in the idea.