The step that changes everything
There is a particular kind of mathematical frustration where every line is legal and none of them leads anywhere. The problem is not a missing calculation. It is a missing way to organize the calculation. A useful lemma arrives and suddenly several disconnected facts begin moving in the same direction.
I would welcome a machine that helps find that lemma. I do not think discovery becomes less real because a tool participated in it. The important question is what happens after the suggestion arrives. Do I inspect it, understand its assumptions, and learn why it fits? Or do I merely paste it into the gap and admire the fact that the proof now closes?
A concrete achievement
In July 2024, DeepMind reported that AlphaProof together with AlphaGeometry 2 solved four of the six problems from that year’s International Mathematical Olympiad, reaching a silver medal standard. That is a specific historical result, and I find it impressive. Difficult problems yielded to systems designed to search and reason in ways that differ from an unaided human approach.
What I resist is turning a competition result into a complete description of mathematics. A contest provides a problem and a criterion for success. Much mathematical work includes deciding which problem deserves to exist, choosing definitions, noticing a connection, or finding a statement whose importance only becomes clear after it is formulated.
Those activities can also benefit from machines. I simply do not want their value to disappear because they fit less conveniently into a score. A system that proposes a fertile definition might change a subject without producing the kind of result that is easy to summarize in a medal comparison.
Read the unexpected line
If a machine offers an unfamiliar lemma, I want the next step to be curiosity. What structure does the lemma exploit? Which hypothesis does the work? Can the statement be weakened? Is this a one time bridge or an instance of a larger pattern? Those questions turn assistance into an education.
Formal checking has an essential role here, but the human task should not shrink to watching a green indicator. A checked proof can provide confidence in a formal derivation while still leaving a great deal to understand. We should build interfaces that help people investigate that remainder.
A shortcut is most valuable when it improves the map. I want AI in mathematics to reduce wasted effort without teaching us that all effort is waste. The search may become faster. The reason for caring about the result can become richer. If we keep both ambitions visible, the machine’s useful suggestion does not end the conversation. It gives us a better place to begin it.