A. In general, proving draws (from fortresses) is easier than proving wins for humans. I guess you could write K+Q and K+R as induction proofs, and in general (see B+N below) you want to progress from one goal to the next, but clarifying this is in an explicitly mathematical way is not typical.
As for actual publications, chess is not so apparent, but the B+N ending in Kriegspiel was proven to be a win by Ferguson, notably published in a TCS (theoretical computer science) journal. He later handled B+B but I think it remained unpublished.
Maybe Timman's famous R vs B and a-pawns analysis could be considered similarly weighty as a publication (the old-school analyses of Cheron and Averbakh largely before computers are of course error-prone, but did make some attempt to mathematize the process).
B. There is a lot of misunderstanding regarding computers and fortresses, as usually the humans do not use the right tools (they will use a general computer program and "root search" for instance). Moreover, phrases like "decisive advantage" are not really meaningful to a computer until a win is actually proven (for instance, today's game of Giri versus Hou Yifan had some interpretations of computer scores erroneously giving a "decisive advantage" (-2.5 after White's 71st move Kb5) in a 7-piece rook ending at a point when it was theoretically drawn by enumeration from consulting either the Lomonosov tablebases or RobboBlockedBases).
It is diverging into peculiarities of chess analysis (rather than proof), but one simple yet often superior alternative (indicating the aforementioned Mamedyarov-Caruana draw rather easily, though proof is of course a different question) involves seeing whether the computer's score increases or not as the search goes on (e.g., is some progress being made, such as pushing a pawn?). Naturally this will not likely help in extreme (typically contrived) examples, but in most practical cases this suffices.
C. Some software solutions have been attempted. The programmer of the chess program "Houdini" had a special mode (reduction of 50-move rule) to try to suss out fortresses, demanding progress be made quickly. There is also Bleicher's "Freezer" that is a human/computer interactive proof agent: you make the "rules", and it iterates over positions. (Unfortunately, the article from 2004 is rather old, and the given examples are solvable by brute means by now.)
There is also a paper of Guid and Bratko ("Detecting Fortresses in Chess"), which discusses some other methods in specific cases, though I don't think they would lead to "proofs" per se.
D. One of my favorite examples, which I saw posted by George Tsavdaris awhile back though he never gave the source, is this study.
1k6/3p4/1B6/4Pp1p/1p5R/1p4p1/pP3n2/K6n w - - 0 1
Peter Martan (a noted computer chess expert) was baffled, and then kicked himself when given the solution, realizing that he should have checked whether the scores were diverging or stabilising. I won't give the solution, but knowing that "fortress" plays a role is already a significant hint IMO.
Another famous example of a position where humans can "see" (and prove, to some degree) the solution but computers were traditionally baffled, is the Behting study (first solved by the program PATZER in 1999), though general computer programs by now appear capable of indicating that the position is indeed drawn (though as warranted, "0.00" must be interpreted rightly by humans, particularly with Graph History Interaction making this a bit sticky). As with other famous fortress examples, you really don't need a huge search space once you have the "rules" down (see here), so something like FREEZER should apply (I don't know if anyone ever did this one).
E. The most significant blunder in modern computer chess (f4 on move 71), was committed by Rybka against Zappa in Game 9 of their 2007 showdown match, simply because it didn't realize that being 3 pawns up in an opposite-bishop ending was worthless. Zappa "knew" the resulting position was drawn, but I don't know if I'd call it a "high-level proof" or not.