International Physics Olympiad (IPhO)

Stream: PhysLean

[Joseph Tooby-Smith]

Within Mathlib there is the directory ./Archive/Imo/ consisting of solutions to past international math olympiad questions. The reasons stated their for such a file are:

• The IMO Grand Challenge will need training data, and exemplars, and this is a reasonable place to collect Lean samples of IMO problems.
• As with the rest of Archive/, we want to have high quality examples covering elementary mathematics, available as learning materials.
• They are popular as a first contribution to mathlib, and an opportunity to teach new contributors how to write Lean code.

I am reluctant to consider the first of these an advantage - mainly because I don't want to do the AI's companies work for free. But I think the other two are valuable.

Thus, the question is, should have the same in PhysLean for the IPhO?

I think the particular aim, or challenge, should be to:

Formalize the necessary physics into PhysLean such that the IPhO theoretical questions can be stated and proved using formalizations which are connected to other parts of the project and more generally applied.

In particular, I think it is important that the is aim to formalize not only each question and answer, but also the background behind that question and answer (which, from the physics point of view is the most interesting bit).

This would obviously not become main objective of PhysLean, but I think would provide a valuable source of project ideas at a nice level, and a goal which could be aimed for. There are no doubt issues here I haven't thought of as well. Any thoughts would be appreciated.

The questions in the IPhO can be seen here.