Reverse IMO grand challenge

Stream: general

[Joachim Hauge]

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]

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

[Patrick Massot]

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]

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

[Mario Carneiro]

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]

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

[Joachim Hauge]

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]

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

[Mario Carneiro]

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