Why is there no formal Geometry data?

Stream: IMO-grand-challenge

[andy]

Compared to other domains?

[Scott Morrison]

@Joseph Myers is the expert here, and you should search back through his posts about IMO geometry to get the proper answer to your question.

A short version is: deciding how to formalise the statements of geometry problems is conspicuously harder than many other domains. Often, this is a matter of implicit side conditions in problem statements, that require a subtle reading to decide how to formalise correctly and fairly. Moreover, there is simply a lot of theory to formalise before you can even state geometry problems, relative to combinatorial or algebraic problems at IMO level. Joseph has been doing this!