Commit 2024-11-16 08:23 f136306a
View on Github →feat(Archive/Imo): IMO 2024 Q5 (#18685)
Formalize IMO 2024 problem 5.
Note that this solution is longer than any of the existing IMO formalizations in either the mathlib archive or compfiles; feel free to golf, where doing so isn't adverse to the role of such formalizations as readable examples. Various definitions using proofs (that certain paths used in an optimal strategy are valid paths) by essentially split_ifs <;> simp <;> omega are (subjectively, not counted heartbeats) slow for Lean to process; in those cases, I think the tactics used are a better approach as an example than a faster but lower-level and probably longer proof would be, so rather than making those proofs longer to speed them up it might be better to treat them as examples that might show opportunities for speeding up those tactics.