Оргкомитет Международной математической олимпиады предложил создать конкурс IMO Grand Challenge, посвященный созданию алгоритма, который автоматически решает классические олимпиадные математические задачи. Алгоритм необходимо будет разработать с помощью языка программирования Lean. Пока что правила конкурса уточняются, сообщается на странице IMO Grand Challenge на github.
Международная математическая олимпиада ежегодно проводится среди школьников старших классов с 1959 года: участникам предлагается решить шесть задач из разных областей математики, которые условно можно разделить по уровням сложности.
Все задачи участники должны решать самостоятельно без использования какого-либо программного обеспечения. В дополнение к классической олимпиаде оргкомитет, однако, решил добавить дополнительный конкурс, цель которого — разработка компьютерных методов решения задач.
Участникам такого конкурса предложат к решению классические олимпиадные задачи (в формальном виде), которые разработанный ими алгоритм будет решать с помощью языка Lean. Алгоритму дается столько же времени, сколько и участникам самой олимпиады (по 4,5 часа на каждый набор из трех задач), при этом в конкурсе не ограничены используемые вычислительные средства.
Что касается самого алгоритма, то он должен быть в открытом доступе, поступить к оргкомитету олимпиады за день до проведения состязаний, а также должен работать без подключения к сети.
Пока что неясно, будет ли конкурс отдельным мероприятием или же станет частью самой Международной математической олимпиады. Среди участников оргкомитета, который будет заниматься созданием конкурса, — исследователи из Microsoft Research, Питтсбургского и Стэнфордского университетов и Лондонского имперского колледжа. Они уточнили, что предложенные правила пока что предварительные и пригласили всех желающих принять участие в их обсуждении.
В этом году на Международной математической олимпиаде первое место с 226 баллами (из 252 возможных) разделили команды из США и Китая. Российская команда набрала 179 баллов.
Елизавета Ивтушок