George Boolos has a nice example in "[A Curious Inference][1]", 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][2] surveys this for $\mathbb{T}\vDash\{\sigma\in S\}$ and $\mathbb{T}\vdash\{\sigma\in S\}$; Harvey [Friedman][3] has an example for $\mathbb{T}\nvDash\sigma$ and an elemetary proof of $\mathbb{T}\nvdash\sigma$.

  [1]: https://www.jstor.org/stable/30226368?seq=1#page_scan_tab_contents
  [2]: https://mathoverflow.net/a/164735/44143
  [3]: https://mathoverflow.net/a/261416/44143