Warning: I am only an amateur in the foundations of mathematics.

My understanding of this Wikipedia page about Tarski's axiomatization of plane geometry (and especially the discussion about decidability) is that "plane geometry is decidable".

The 2019 International Maths Olympiad happened recently, and there were two plane geometry questions in it (problems 2 and 6). Their solutions look really intimidating! However even as a student I felt that one should be able to solve these questions, in theory, by just "writing down coordinates of everything and doing the algebra". Tarski's work, which I will freely confess that I do not understand fully, might even vindicate my view.

The question: Is there an algorithm for solving these kinds of questions, or have I misunderstood? If so, is this algorithm actually feasible to run in practice nowadays (on a computer say) for IMO-level problems? In other words -- are there computer programs which will take as input a planar geometry question of "olympiad level" (for example problems 2 and 6 in this year's IMO) and actually output a solution?

Currently I am not too bothered about whether the solution is human-readable -- it could just be a formal proof in some kind of type theory or something, but the output would be some object that some expert could coherently argue was a solution of some sort.

The reason I'm asking is that I was talking to some computer scientists about various goals in the long-term project of getting computers to do mathematics "better than humans", and having a computer program which could solve IMO problems by itself was a suggested milestone.

Tarski'salgorithm was not bounded by any stack of exponentials, the modern way of eliminating quantifiers for real-closed fields iscylindrical algebraic decomposition, which is only double exponential. Mathematica has an implementation of this. Apparently, there is also an algorithm for eliminating existential quantifiers (projecting a semialgebraic set) that only takes exponential time, but this is not available in Mathematica or any other major CAS, and the only implementation I could find of it hit a bug on every nontrivial example I tried. $\endgroup$15more comments