leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

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: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll