Zulip Chat Archive

Stream: Is there code for X?

Topic: IMO 2012-4

Alain Verberkmoes (Mar 16 2021 at 14:37):

Hi. Has anyone done IMO problem 2012-4? I'm new at Lean and might have a go at that problem. Many thanks.

Johan Commelin (Mar 16 2021 at 15:14):

@Alain Verberkmoes Welcome! Good to see you here.

Johan Commelin (Mar 16 2021 at 15:14):

The IMO problems that have a formalization in mathlib are stored in archive/imo/. Currently it contains:

imo1959_q1.lean  imo1962_q4.lean  imo1972_b2.lean  imo1988_q6.lean  imo2013_q1.lean  imo2019_q4.lean
imo1960_q1.lean  imo1964_q1.lean  imo1981_q3.lean  imo1998_q2.lean  imo2013_q5.lean  imo2020_q2.lean
imo1962_q1.lean  imo1969_q1.lean  imo1987_q1.lean  imo2011_q3.lean  imo2019_q1.lean

Last updated: Dec 20 2023 at 11:08 UTC