IMO 2024 Solutions

These pages show the proofs found via the AlphaProof and AlphaGeometry agents. More information about the agents can be found in the blog post.

The English problem statements are taken from the official IMO website.

In the Lean code produced by AlphaProof, the comments are inserted by hand to illustrate the approach the agent took. While the problem statements were formalized into Lean by hand, the answers within the problem statements were generated and formalized by the agent.

The Lean proofs are rendered using Verso, which allows the goal state (the proof progress) to be inspected before and after each "tactic". This is a pared-down version of the usual experience when writing Lean code in a supported editor, such as Visual Studio Code with the Lean 4 extension.

download Download the Lean files