Aren't some IMO problems pretty easy if you can throw a computer algorithm at it? (for example geometry problems can be coordinate bashed?)

Also I can't find an accompanying dataset from the link: https://imo-grand-challenge.github.io/

EDIT: Nvm found it: https://github.com/IMO-grand-challenge/formal-encoding/blob/.... But there are only a handful of formal encodings of problems and last commit was from a year ago!