IMO 1996 P3 video

Stream: general

[David Renshaw]

I uploaded a video in which I formalize a solution to IMO 1996 P3. https://youtu.be/5NbYtDfXfR4

[Jovan Gerbscheid]

There's multiple places to put IMO problem formalizations:

• Archive in mathlib
• https://github.com/jsm28/IMOLean which has only the statements formalized.
• Your compfile repository.

What do you think about this? I'm asking because I have a mathlib PR with a formalization of IMO2020Q6 (which btw I haven't touched in a while, because I wanted to develop some more API for it but that never went through).

[David Renshaw]

I like working in the Compfiles repo because progress there does not need to be held up by mathlib review and also I can experiment with additional features like the problem syntax and website generation.

[David Renshaw]

mathlib4/Archive has higher standards of review, and if you land something there you probably get greater assurance that it will be kept up-to-date with the latest mathlib.