George Boolos has a nice example in "A Curious Inference", where $\mathbb{T}\vDash\sigma$ is obvious from second-order or semantic considerations, but $\mathbb{T}\vdash\sigma$ is of Ackermann difficulty in first-order logic, so that anyone would come across the first proof first.
More tangentially from my other answers: Jeremy Avigad surveys this for $\mathbb{T}\vDash\{\sigma\in S\}$ and $\mathbb{T}\vdash\{\sigma\in S\}$; Harvey Friedman has an example for $\mathbb{T}\nvDash\sigma$ and an elemetary proof of $\mathbb{T}\nvdash\sigma$.