Invitation to give (online) expository talk.

Stream: IMO-grand-challenge

[Nikolay Shilov]

Dear All,

Since I do not know to whom address in person I prefer to address the community of the IMO Grand Challenge: Would anyone be so kind to give an expository talk on what currently is going on the community, who are involved and what is job flow.

Why I am interested? - We have a Math Club at Innopolis University (https://innopolis.university/). - Please check our activities on Telegram - https://t.me/InnoMath. Annually we attempt to solve problems of the most recent IMO. It was true September 2019 too when I apparently came across the announcement about IMO Grand Challenge. Unfortunately I had no time during the year to join or (at least follow) the activities...

But last Wednesday, September 30, I gave an introductory talk to the club about IMO Grand Challenge as an initiative of a group of experts on automatic proof to create a system that can systematically win gold at the International Mathematical Olympiad. Presentation (in English) is available at https://drive.google.com/file/d/13xlcgfy0zqvkEpsEA40fs-464_bhLEyd/view?usp=sharing and meeting recording (just in Russian) - at https://drive.google.com/file/d/1tuBMqf5IBRGcfEhSngZJL4FKS5G7CMiU/view?usp=sharing.

So I just look for volunteers from the IMO Grand Challenge community to give an expository talk for IU Math Club (and, maybe, for the World - Urbi et Orbi) about what currently is going on the community, who are involved and what is job flow. - I believe it will recruit more people ready to contribute (me and my students at least).

You can just reply to this message or write my in person by email (provided below).

Regards,

Nikolay Shilov
(Just to introduce myself:
Dr. Nikolay V. Shilov
Assistant Professor of Innopolis University, Russia
email: shiloviis@mail.ru
official web-page: https://innopolis.university/en/faculty/
personal web-page:  http://persons.iis.nsk.su/en/person/shilov)

[Miroslav Olšák]

As far as I know, there is no serious automation attempt so far. The current status is rather trying to formalize IMO problems (problem statements and solutions), and we also have some very vague ideas on how some automated prover could work. Parallel to that, there are some machine learning experiments around theorem proving but really below the IMO level. @Daniel Selsam could be interested in giving a motivational talk but there is a question on how far beyond your motivational talk it could go.

[Miroslav Olšák]

Maybe, you could be interested in learning lean and formalizing some IMO problems / solutions in it. Such work would be always appreciated here. From my experience, formalizing IMO solution (in lean) is way harder than it looks from the human solution but with enough determination, I believe that your group can do it.

[Miroslav Olšák]

And from the mathematical human solving point of view, there is another idea that could turn to be useful in the long run for writing the solver: try to solve an IMO problem and record as much ideas during the process as possible. I am trying to do that for some shortlisted problems in combinatorics here (I have also tried three geometry problems, they are not there ): http://www.olsak.net/mirek/human-imo-solving.php So far, this is just my personal project but we could extend it if you would be interested. The idea is to have an unbiased look at what people actually do when solving such problems.

[Kevin Buzzard]

Yes, I would have very little to say other than observing that formalising IMO problems is an interesting challenge for a human

[Kevin Lacker]

@Nikolay Shilov if you formalize one IMO problem, in exchange I will give your math club a talk :D

[Daniel Selsam]

(FYI I am away on vacation this week, and will respond to these threads next Monday)