IMO 2024 Solutions
Google DeepMind IMO 2024
IMO 2024 P1IMO 2024 P2IMO 2024 P4IMO 2024 P6
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