# Zulip Chat Archive

## Stream: general

### Topic: Reverse IMO grand challenge

#### Joachim Hauge (May 08 2021 at 13:26):

I wonder if the following could help popularize formal math. A competition for college students where they are given 3 hours to exhibit terms of some given types. The types would be accompanied by explanations in human language. Their terms have to typecheck within say two minutes. This would be an olympiad like ICPC but with a math focus.

Has anybody tried this?

#### Mario Carneiro (May 08 2021 at 13:30):

Isn't that just the regular IMO? At least if you believe the curry howard correspondence

#### Patrick Massot (May 08 2021 at 13:30):

I would rather see a version involving the word proof instead of "terms of a given type". What you describe doesn't have a "math focus" but rather a "computer science focus".

#### Mario Carneiro (May 08 2021 at 13:31):

The types most computer scientists deal with are too simple to have a nontrivial inhabitance problem

#### Mario Carneiro (May 08 2021 at 13:31):

It only starts to get interesting when you throw in dependent types, and at that point it's just a mathematical theorem in disguise

#### Patrick Massot (May 08 2021 at 13:32):

Part of what I mean is that Joachim's wording suggests not using tactics.

#### Joachim Hauge (May 08 2021 at 13:35):

Mario Carneiro said:

Isn't that just the regular IMO? At least if you believe the curry howard correspondence

Yeah but in regular IMO you write on a sheet of paper, here you write in Lean

#### Mario Carneiro (May 08 2021 at 13:36):

Oh so it's a formalization competition. There are a few of those. One that has been advertised here is Proof Ground

#### Mario Carneiro (May 08 2021 at 13:38):

Although those don't require a text explanation usually. I would be pretty surprised if you could write a formal proof in two or three hours where the proof approach isn't obvious and needs explanation beyond the formal text itself

Last updated: Dec 20 2023 at 11:08 UTC