AI Proof WatchKeep up with AI contributions

IMO 2024 Problem 2: eventual GCD constancy

Determine all positive integer pairs (a,b) for which positive integers g and N exist with gcd(aⁿ+b,bⁿ+a)=g for every n≥N.

Why it matters and what counts as progress

Why it matters: It asks when a sequence of greatest common divisors becomes permanently constant, rather than merely repeating for many tested exponents.

What counts as progress: A proof of the full classification of positive integer pairs, controlling every sufficiently large exponent rather than a finite list of tests.

How the problem developed

  1. 16 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.