[generationP]

What deductive system are they using to verify the proofs? I'm asking because the conventions of olympiad geometry are slightly different from those of the rest of mathematics (you can make informal "general position" arguments; you can pooh-pooh issues of sign and betweenness; you can apply theorems to unstated limiting cases; etc.), and it is far from obvious to me how this logic can be formalized without causing contradictions.

[lacker]

They built their own symbolic geometry engine, called DDAR. The IMO judges will typically let you get away with much less rigor than a symbolic engine like this produces, so I don't think they are taking advantage of any of these conventions.

[generationP]

Ah, thanks! It seems to be this one http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf plus some algebra for adding angles and lengths. As I hoped, they are using oriented angles mod 180° ("full-angles") to get rid of betweenness conditions. They are also using evaluations at rational (I think) coordinates to check that nondegenerateness conditions are satisfied when the data is in general position. This is not as nice as I had hoped for, but certainly no worse than what contestants do at the IMO. And because a bunch of methods are off-limits (congruence criteria, probably anything involving undirected unsquared lengths), I'm not surprised that their proofs are longer/slower than human ones -- they're better proofs.