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.

http://www.sciencedirect.com/science/article/pii/030439759290344F

He later handled B+B but I think it remained unpublished.

http://www.math.ucla.edu/~tom/papers/unpublished/kriegbishop.pdf

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. 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.)

http://www.minet.uni-jena.de/preprints/bleicher_04/FREEZER_.PDF

http://www.freezerchess.com/

C. One of my favorite examples, which I saw posted by George Tsavdaris awhile back, and he never gave the source, is this study.

1k6/3p4/1B6/4Pp1p/1p5R/1p4p1/pP3n2/K6n w - - 0 1

[![enter image description here][1]][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 extent) the solution but computers were traditionally baffled, is the Behting study (first "solved" by the somewhat special-purpose program PATZER in 1999), though general computer programs appear capable by now indicate that the position is indeed drawn.

http://chessprogramming.wikispaces.com/Behting+Study


  [1]: https://i.sstatic.net/48QUp.png