[iop]

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!

[dselsam]

That repository has rotted. Preliminary roadmap described in recent invited talk at AITP-2020 http://grid01.ciirc.cvut.cz/~mptp/zoomaitp/aitp_sep_15_1930....