IMO 2024 shortlist statments

Stream: IMO-grand-challenge

[Joseph Myers]

https://github.com/jsm28/IMOShortlist2024Lean now has the Lean statements for IMO 2024 shortlist problems that I wrote shortly before that IMO (plus a couple of solutions and one incomplete solution). Note the various caveats given there; these statements don't follow my more recent conventions, don't include the problems that ended up on the IMO, don't include geometry problems because too many definitions were missing from mathlib at the time, and have not been carefully checked for correctness.

[Eric Wieser]

don't include geometry problems because too many definitions were missing from mathlib at the time,

Did you have more success with this year's shortlist problems, or is mathlib not quite there yet?

[Eric Wieser]

(I'm aware that the problems on the 2025 shortlist are secret for another year)

[Joseph Myers]

I haven't attempted to write Lean statements for any IMO 2025 shortlist problems beyond those selected for the paper. All definitions needed for IMO 2025 P2 were present (since I'd added definitions relating to tangency during the past year) without any workarounds for missing definitions being needed. In general terms, the main missing definitions needed for significant proportions of past IMO and IMO shortlist geometry problems relate to angle bisectors, polygons and arcs of circles. (Looking at the IMO 2024 shortlist geometry problems, for example, G2 (= P4), G7 and G8 can now be expressed cleanly, while definitions should still be added for stating G1, G2, G4, G5 and G6.) I hope to add more such definitions in future, but my current series of PRs (#26530 etc) are oriented more to adding enough incenter API to start on the solution to 2024 P4, rather than on definitions now the main incenter-related definitions have been added. (I think the most convenient form of lemmas relating incenter to angle bisectors for solving problems in two dimensions is probably not the same as one involving explicit bisector definitions for $(n-1)$-dimensional oriented subspaces for the faces of a simplex in $n$ dimensions that describes the relation in $n$-dimensional generality.)