Sure, but I don't think theoretical guarantees are that important in practice. When I solve math problems, I don't personally use methods with such guarantees. Mathematica has certain guarantees for evaluating integrals, but that really doesn't help when it chokes for an hour on one. In practice what matters is computational complexity, and how well heuristics can help you narrow down your search space. And here IMO geometry problems have the enormous advantage that one knows there exists a short, purely synthetic solution.

I think there is actually a guaranteed synthetic-geometry technique, where the main idea is to compare areas of regions. See e.g. http://www.mat.uc.pt/~pedro/cientificos/Publicacoes/apresent... and http://argo.matf.bg.ac.rs/publications/2011/area.pdf. I vaguely remember hearing many years ago that the Chinese IMO team had been trained in applying something like this method, but I've no idea whether it was true then or whether anything like it is true now.

tho tbh i'd love to see an NLP project for turning high school geometry problems into grobner basis problems, and solving them there.