4 ms·
I think this illustrates one of the preconceptions this challenge is meant to work against. Namely, people think of coordinate bashing as "computational" and pu
by knzhou 7y ago
I think this illustrates one of the preconceptions this challenge is meant to work against. Namely, people think of coordinate bashing as "computational" and purely synthetic/geometric solutions as "insightful". But there's no reason that a computer would find the second way more difficult. After all, synthetic geometry is just another system of rules, like ordinary algebra.
Us humans might fall back on coordinate bashing, but that's just because we have a lot of practice with the rules of algebra. To a computer, one rule set is as good as any other. What we call geometric insight boils down to pattern matching configurations to previously seen ones, combined with search in the space of possible moves, both of which computers can do.
- OscarCunningham 7y agoThe current situation doesn't reflect that though. We have a algorithm (Gröbner bases) for doing coordinate bashes which is guaranteed to succeed, whereas as far as I know we don't have an analogous algorithm in terms of synthetic geometry (other than the direct translation of coordinate bashing).
- knzhou 7y agoSure, 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.
- sdenton4 7y agotho tbh i'd love to see an NLP project for turning high school geometry problems into grobner basis problems, and solving them there.
- gjm11 7y agoI 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/apresentacaoDaysInLogic06.pdf http://www.mat.uc.pt/~pedro/cientificos/Publicacoes/apresent... and http://argo.matf.bg.ac.rs/publications/2011/area.pdf 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.