Member-only story
AI Found the Answer. Now Who Can Understand It.
The counterexample fits on a napkin: {1, 2, 4, 8, 13}.
In October 2025, Boris Alexeev and Dustin Mixon showed that this little set does away with a conjecture Paul Erdős posed for two decades and put a $1,000 prize on. It is a Sidon set, a collection of integers whose pairwise differences never repeat, and it cannot be extended to a finite perfect difference set. The human insight is actually fairly short.
To be sure of the result, they formalized the argument in Lean using ChatGPT to actually write it. A formally checked proof spanning thousands of lines was used to confirm a fact you can explain in a paragraph.
This illustrates a growing gap in AI-driven discovery: the distance between verifying a result and understanding it.
Yes, mathematicians must still check the assumptions and the like, but even a verified argument can leave readers struggling to see the main ideas that make it work.
I tell my students to verify AI outputs, but verification is not the difficult part. A machine can hand you a result, which you can check and still not understand. Perhaps you get a result that answers a somewhat different question from the one you asked.
The interesting question is no longer whether AI can find the answer, it’s what we’re supposed…
