The title is click baiting.

Prompt engineering is still important.

From a philosophical point, it always makes a difference how you phrase a problem. If you formalize a problem in Lean code, it's easy to understand for a proof assistant but not for most humans (even mathematicians or programmers).

So rephrasing the problem in human language makes it easier to grasp and comprehend. And given the dataset the AI is trained on, there might be certain style it prefers. If you train it on Lean code, better input lean code. Also, more context makes it usually easier to solve the problem.