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.
Best Answer
Arguably, the so-called "area method" of Chou, Gao and Zhang represents the state of the art in the field of machine proofs of Olympiad-style geometry problems. Their book Machine Proofs in Geometry features over 400 theorems proved by their computer program. Many of the proofs are human-readable, or nearly so.
The area method is less powerful than Tarski–Seidenberg quantifier elimination in the sense that not every statement provable by the latter is provable by the area method, but the area method has the advantage of staying closer to the "synthetic" nature of (the vast majority of) Olympiad problems.
EDIT (February 2022): OpenAI has announced some success with solving (some) formal math olympiad problems. They did not restrict themselves to geometry problems.