The answer turns out to be pretty boring: As long as humans are still better than machine, humans can provide algorithmic insights and be a source of cheap labels.
So I am pretty pessimistic about this particular task. There are only a small handful of humans in the world who are qualified to help! (according to IMO scores: https://www.imo-official.org/hall.aspx)