Let me prove, for example, that the following 7-piece position is a draw. 7-piece positions are about the borderline of what's doable by brute force: they were tabulated around 2010.
Black draws as follows:
if white queen captures the rook or the pawn, recapture.
else, in the event of check, move the king to h7, h8, or g8 (cannot all be controlled by the queen simultaneously)
else, if white queen or pawn moves to 6-th rank, capture it with the rook,
else, move the rook to f6 or h6.
Clearly, unless white sacrifices the queen, she cannot cross the 6-th rank with the king and thus cannot break the above routine. The possible sacrifices are:
A) by capturing the g7 pawn. Recapture with the king and continue moving the rook, securing a draw.
B) by taking the rook. Any resulting pawn endgame is drawn by moving the king between h7, h8, and g8;
C) by Qa6, Qb6, Qc6, Qd6 or Qe6, followed by rook takes queen and king takes rook. The very same idea, only be sure to take g7:h6 when you can.
D) By Qg6 R:g6 h5:g6. This is also a theoretical draw. Move Kh8-h7-h8-... and be sure not to take g7:h6 at a wrong moment.
Some details are left off here, but I think the level of rigour is fairly close to how math is written.
P. S. In a game between Mamedyarov and Caruana (world N17 and N3, respectively), played last Friday, a draw was agreed in the following position:
Computers wrongly give a decisive advantage to white: the idea of cutting the king with the rook is too "high-level" for them to understand it. And I believe, if needed, one can devise a rigorous proof here similar to the one above.