A story with nondegeneracy conditions

Stream: IMO-grand-challenge

[Joseph Myers]

The following story does not actually involve Lean.

At the recently concluded 14th European Girls' Mathematical Olympiad held in Kosovo, the wording that was originally planned to be used for geometry problem 3 did not have all the nondegeneracy / configuration conditions present in the final version of the first day's paper; it was missing the conditions that ADE is acute, that D, H, M, P are pairwise different, and that E, H, N, Q are pairwise different. Late in the evening of the day the translations were being prepared, one of the leaders noticed that statement didn't work when ADE has a right angle (and thus orthocentre) at D or E, resulting in all 37 language versions of the first day's paper needing updating with the additional conditions to avoid such a configuration, and the translations getting approved after 2am (and the printing of the papers for the following morning's exam being completed after 4am).

Unless you think this shows that human competition problems should be checked before use by formalizing a solution, there may be no immediate Lean lesson here (and I've no current plans to formalize this particular problem, although I think all the relevant definitions for the statement at least are in mathlib). However, it would not surprise me if there are some past IMO geometry problems, especially older (pre-GeoGebra) ones, that are in fact missing such nondegeneracy conditons required for the problems to be correct.

It may also illustrate that getting a fully correct informal statement without a formal solution can be hard. Indeed, that's not specific to competition problems; I expect that if you want to autoformalize large parts of the mathematics literature, there will be many cases where a lemma statement fails to exclude some trivial case for which the lemma is false (but that doesn't actually matter for important applications of the lemma), and formalization will need to deal with that. (The ability of Lean to tell you what needs updating when you fix the incorrect statement of a lemma you were using is of value here, whenever you start by sorrying a lemma you are using rather than proving things in strict priority order.)