The TLS 1.3 "Selfie attack" is an example of a gap between what we did prove and what we intuitively understood.
The formal proof for TLS 1.3 says Alice talking to Bob gets all the defined benefits of this protocol, and one option is they have a Pre-shared Key (PSK) for that conversation. They both know the same key, in that sense it's symmetric.
But the human intuition is that we're talking about an Alice+Bob key, whereas the proof says this is an Alice->Bob conversation key. If we re-use the same PSK for Bob->Alice conversations too we get the Selfie Attack, the formal proof never said we can expect that to work, it was just our intuition which confused us.
Also PSK involves sending a PSK identity, which is supposed to be used to find the PSK, in particular it can be a user name, so the server can check the user name is correct.
Up until now it's always been a hard sell, people say "Well, I can prove it myself, and that's less work than getting the computer to prove it", and they weren't completely wrong.
However, now we have LLMs which can do lots of interesting work, but really can't be trusted for anything important (like an LLVM optimisation pass, for example). If those LLMs can convince a theorem prover the LLVM optimisation pass is correct, then suddenly their output is much more useful.