A proof is a social construct – it is what we need it to be in order to be convinced something is true. If you write something down and you want it to count as a proof, the only real issue is whether you’re completely convincing.
Some philosophers of mathematics (often those who call themselves “naturalists”) argue that what we ought to be paying attention to in mathematics is what mathematicians actually do. If you look at it like this, you notice that very few mathematicians actually produce fully valid proofs in first-order logic, even when they’re proving a new theorem (although there are salutory attempts to change this, such as proving lots of existing theorems using Coq).
The best encapsulation that I’ve heard of what mathematicians actually do when they offer proofs is something like:
You don’t have to provide a fully rigorous proof, you just have to convince me that you could do if you had to.
It seems pretty clear to me that this still indicates that mathematicians are really interested in the existence of the formal proof, but they use a bunch of heuristics to figure out whether it exists and what it is. Rather than mathematical practice showing us that the notion of proof is really this more social notion, and that therefore the formal version is somehow off base.
I think people often dismiss systems like STV/IRV by essentially saying “Arrow’s theorem implies you can still vote tactically, so it’s just as bad”. But there’s a big difference: in STV it’s much harder to figure out how to vote tactically.
In First Past The Post systems, tactical voting is blindingly obvious: if there are two candidates you like, but you don’t think that your favourite has enough popularity to win outright, then you should vote for the other one, to avoid splitting the vote. This is easy to understand, and it’s also easy to detect circumstances where it would be beneficial for you to vote other than your preferences.
OTOH, even though there are times where you can vote tactically in STV, they’re harder to understand, and crucially, it’s much harder to recognise such opportunities: you need a lot more information.
This means that, in general, STV would cut down on tactical voting a great deal, simply because it makes it harder.