“Finding these mathematical ideas is hard enough, and having to prove them in Lean makes things even harder.”
AlphaProof solved problems 1, 2 and 6 at IMO 2024, and only 5 of 509 human contestants cracked problem 6. Its answer hinged on a counterexample, f(x) = -x + 2⌈x⌉, that most humans would never think to build. Every step is in Lean, so a machine checks the proof and nobody has to take the lab’s word for it. That is the bar every AI math claim should clear.