AlphaProof's Greatest Hits

submited by

Style Pass

2024-11-17 17:30:03

Here I’ll try to explain the coolest ideas in each of AlphaProof’s IMO 2024 solutions. AlphaProof produces proofs in Lean, and each Lean proof is composed of a series of tactics. So I’ll pick out the tactics that correspond to these ideas in the proofs for problems 1, 2 and 6 (the three problems that AlphaProof solved). AlphaProof has developed its own proving style, so figuring out what it’s doing can involve some detective work.

If you’re not familiar with the problems already, I recommend trying them yourself, and then maybe reading Evan Chen’s solution notes, or watching these videos that give an intuition for some of the human solutions. The full AlphaProof solutions, annotated by Lean experts, are available here - I will only include snippets of the proofs in this post.

is a multiple of $n$. (Note that $\lfloor z \rfloor$ denotes the greatest integer less than or equal to $z$. For example, $\lfloor -\pi \rfloor = -4$ and $\lfloor 2 \rfloor = \lfloor 2.9 \rfloor = 2$.)