AI Proof WatchKeep up with AI contributions

IMO 2024 Problem 6: aquaesulian functions

A function f:Q→Q is aquaesulian if, for every rational x,y, either f(x+f(y))=f(x)+y or f(f(x)+y)=x+f(y). Find the smallest integer c bounding the number of distinct values f(r)+f(−r), r∈Q, for every such function.

Why it matters and what counts as progress

Why it matters: The task asks how much global rigidity follows from a functional relation that permits a different branch for each input pair.

What counts as progress: A uniform bound on the number of possible f(r)+f(−r) values, together with a function attaining the smallest bound.

How the problem developed

  1. 17 Jul 2024 · Contest problem [1]

    IMO jury The problem appeared in the official IMO 2024 contest on this contest day.

  2. 25 Jul 2024 · Reported solution [2][3]

    Google DeepMind AlphaProof and AlphaGeometry solved four of six IMO 2024 problems; DeepMind published a proof page for this problem. Its problem page documents which formalization and proof system were used.

AI contribution

Olympiad-level formal mathematical reasoning with reinforcement learning

Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z. Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, Ottavia Bertolli, Tom Zahavy, Amol Mandhane, Jessica Yung, Iuliya Beloshapka, Borja Ibarz, Vivek Veeriah, Lei Yu, Oliver Nash, Paul Lezeau, Salvatore Mercuri, Calle Sönne, Bhavik Mehta, Alex Davies, Daniel Zheng, Fabian Pedregosa, Yin Li, Ingrid von Glehn, Mark Rowland, Samuel Albanie, Ameya Velingker, Simon Schmitt, Edward Lockhart, Edward Hughes, Henryk Michalewski, Nicolas Sonnerat, Demis Hassabis, Pushmeet Kohli, David Silver

DeepMind reports Lean proofs for IMO 2024 problems 1, 2, and 6, and publishes the specific proof artifacts.

AI involvementAI-centered
ImportanceModest
Technical verificationFormal (Lean)
Human understandingFull
Paper date:

Read the contribution and its assessment →

Sources

  1. IMO 2024 official problem archive
  2. Original report (25 July 2024)
  3. Google DeepMind, IMO 2024 problem solution
  4. AlphaProof research paper
  5. Authors’ specific IMO statements and proof files
Website timeline

Publication dates and editorial changes.