I realize this question is risky (as the title and the tags indicate), but hopefully I can make it acceptable. If not, and the question cannot be salvaged, I'm sorry and ready to delete it or accept closure.
Oftentimes, when one listens to chess grandmasters commentating on games, they will say things like, "The engines give a +1 advantage to White, but the postion is dead-drawn." And they proceed to provide high-level explanations of such statements. I'm a bad chess player so I cannot really attempt to verify those, but they often sound extremely convincing. Also, when they teach simple endgames, they seem to consider analyzing the crucial ideas to be enough for proof (at least in the sense of "a completely convincing explanation") and it's difficult not to agree with that. Even certain positions with a lot of pieces on the board can apparently be treated this way. "There is no way to make progress" is something that one can frequently hear.
Sometimes these just turn out to be wrong. These statements are generally based on intuitions ("axioms") such as "you cannot give away your queen for a pawn", which are believed to be true in almost all situations and on already analyzed positions (like the Lucena position). The grandmasters' intuitions are very fine, but it can happen that they will miss a counterintuitive material sacrifice, a counterintuitive retreat or a counterintuitive something else. However, they can be extremely convincing sometimes (and never proven wrong).
It's clear that chess can't be solved this way any time soon. A clear obstacle is the "wild" or "unclear" positions, where "anything can happen". But there are also those "tame" positions, "dead-drawn" positions and "winning advantages". (Surely, some -- or maybe a lot -- of these statements are not correct or correct with incorrect reasonings behind them.) Another indication is that the humans who make these statements get beaten by computers, which primarily use low-level tree searches.
My question is how much, if anything, of this high-level reasoning can be put to a form that would make it mathematics and mathematical proof. I think brute force is clearly not the only way of evaluating positions rigorously. In a K+Q v. K endgame, one doesn't have to analyze each possible move of the lone king to show that it's doomed. It's enough to show that a stalemate is impossible when the king is not on the side of the board, that the king can be forced to the side of the board and then that whenever the king is on the side, it can be checkmated. For a rigorous proof, one can use all kinds of symmetries and translations without having to go through every single node of the tree.
How much of that high-level thinking grandmasters employ can be made into mathematics?
is what I'm interested in, but this is vague -- it's not clear what "how much", "high-level thinking" or even "made into" mean. But I think people must have tried to pursue this and some clear mathematical statements must have been produced. If not, is it at least possible to say why it's difficult, infeasible or impossible?
Is there a chess position with a large (enough to be intractable to a human with just a pen and a piece of paper) tree that has been solved without brute-forcing the tree? Has a rigorous proof accessible to a human been produced?