problems: the source

Stream: IMO-grand-challenge

[Johan Commelin]

PDF files with the IMO problems are available here: https://www.imo-official.org/problems.aspx

Does anyone know whether there is a LaTeX version of these files available? Could we ask IMO for such files?

[Jason Rute]

I’ve never done IMO stuff, so I’m not an expert, but I see there are a lot of problems here in a wiki format (which I assume uses some pseudo LaTeX). https://artofproblemsolving.com/community/c3222_imo

[Johan Commelin]

Aha... that's already a start. I don't see a mass download button though...

[Jason Rute]

@Johan Commelin I think if this is a serious research project, which it seems to be, it is worth talking to a number of people about the best sources of official problem sets and training problem sets and what formats they come in. Some ideas include talking to the IMO folks, the admins for the Art of Problem Solving, the team leads for various countries (Po Shen Lo is at CMU for instance), previous Olympians like Reid, and maybe the MathOverflow/MathSciNet community. It would be good to talk to them about the official IMO problems, but also about other canonical sets of practice problems at various levels of difficulty. It is always good to have lots of training and test data, especially if machine learning is involved. AOPS or the IMO committee might like the press of partnering with Microsoft Research to train computers to solve challenging math problems. (Or a different spin: "computers can't come even close to the most talented high school students".) I could also imagine a large dump of a website like AOPS involving copyright and data sharing issues that need to be worked out. Also, once the data is procured, there are questions about how to start to organize and process it. (To be clear, I am sure Daniel Selsam and team are carefully thinking through all this, and I don't mean to suggest otherwise.)

[Jason Rute]

Also, I am reminded of DeepMind's data set here: https://github.com/deepmind/mathematics_dataset It is a similar goal of "teach computers to do math", but it is also different in many ways. They are much easier and more computational math problems, but the overall problem is also in other ways harder since they involve natural language processing from text. I think DeepMind's goal is to have a general NLP/AI algorithm which can solve these problems just from seeing text examples (similar to the goal to solve Atari games from pixels alone), whereas the goal in this IMO challenge is to throw everything at the IMO problems (ATP, ML/AI, decision procedures, hard coded heuristics, etc.).

[Yury G. Kudryashov]

I was in top-10 in Team Russia try outs for IMO 2002, so if you need a help from someone familiar with this type of problems, you may ping me. And my wife has an IMO gold medal. Disclaimer: it seems that I forgot a lot of tricks since then. Sorry, maybe this was a wrong thread in this channel.

[Scott Morrison]

Probably it makes sense to pick a "representative" small set of problems, and then discussion in detail what a formalisation of the statements would look like.

[Scott Morrison]

I just wrote a statement of imo_2018_q3. I'm tempted to suggest that a few others do the same thing, then we all reveal at once, just to see how much variation there is. :-)

[Scott Morrison]

(from https://artofproblemsolving.com/community/c681585_2018_imo)

[Mario Carneiro]

I guess Q3 is decidable :)

[Daniel Selsam]

... whereas the goal in this IMO challenge is to throw everything at the IMO problems (ATP, ML/AI, decision procedures, hard coded heuristics, etc.).

I would say the goal is to spur fundamental progress in AI. I would be very surprised if a team could win gold by piecing together existing methods.

[Oliver Nash]

Maybe I'm too late but if it helps, thirty years (1990 -- 2019) of IMO problem statements are available in LaTeX here: https://github.com/ocfnash/visualising-imo-results/blob/master/src/problems.json (the only thing required is to replace \\ with \).