Zulip Chat Archive
Stream: IMO-grand-challenge
Topic: IMO 2021
Joseph Myers (Jul 20 2021 at 21:16):
The IMO 2021 problems are now available from imo-official.
Someone on AoPS appears to have got the idea that AI is already ready to attempt full IMO problems.
Daniel Selsam (Jul 20 2021 at 21:58):
Not this year :) We have still been mostly focused on core Lean4 and on porting Mathlib, but IMO-GC remains one of our main long-term initiatives.
Last updated: Dec 20 2023 at 11:08 UTC