Оргкомитет Международной математической олимпиады предложил создать конкурс IMO Grand Challenge, посвященный созданию алгоритма, который автоматически решает классические олимпиадные математические задачи. Алгоритм необходимо будет разработать с помощью языка программирования Lean.