Listen to this article
AI may have been used to generate this audio.
Press Space or K to play or pause, and J or L to go back or forward 15 seconds.Sources checked 4 October 2026.
The first four odd numbers add to sixteen. You can check the arithmetic quickly. You can also arrange sixteen dots into a square and see each odd number as the new edge needed to grow the previous square. The second view makes the next case easier to anticipate.
For a square with a side of n dots, adding a row and a column around the previous square contributes 2n minus 1 dots. That is why adding the first n odd numbers produces n squared. Nothing about this example needs AI. It helps explain the kind of work still worth doing after someone has checked an answer.
Lean is a proof assistant. It checks formal proof terms against formal statements. People still need to examine what statement was encoded and the assumptions on which it depends. The checker does not decide whether a result is interesting or explain why a mathematician would have thought to try its construction. [1]
A correct answer to a narrower question
Consider a second elementary example. Someone announces that x squared is at least x for every real number. That is false: at x = 0.5, the square is 0.25. If the formal statement instead assumes x is at least 1, the inequality is true. A checker accepting the restricted statement would be doing its job. The announcement would still be too broad.
The issue is visible because the example is small. In a research theorem, the restriction could sit inside a definition, a type or an imported lemma. Reading the statement may take substantial subject knowledge. A green check gives useful evidence about the formal object; understanding the object remains part of the work.
Lean’s documentation describes how #print axioms exposes the axioms a declaration depends on. [4] That makes assumptions inspectable. It does not make every reader qualified to judge whether they are appropriate for the intended result. A sensible explanation should show the important assumptions in ordinary mathematical language as well as pointing to the formal artifact.
This is also why the phrase “the computer checked it” needs a referent. Which theorem, in which environment, with which dependencies? Those are answerable questions. Keeping the answers with the result makes it easier for the next person to decide what they can reuse.
In a September guest essay on Terence Tao’s blog, Grant Sanderson proposed giving greater academic recognition to explanations that make the motivation for mathematical ideas clear. His argument concerns the work of helping another person see where a construction comes from, including explanations intended for specialists. [2]
That work is easy to underestimate if the only question being counted is whether a problem has a proof. A researcher may need to adapt a method to a neighbouring problem. To do that, they need to recognise which step depends on a particular assumption, what breaks when it changes, and which part of the argument can survive.
Take the dot diagram. It gives a useful way to recover the identity rather than memorise it. It also makes its domain apparent: we are counting squares with whole-number side lengths. We would need more care before treating the picture as an argument about other kinds of numbers.
The limitations belong to the explanation. A clear drawing can help someone understand a valid argument, and an attractive drawing can also conceal a gap. The reader still needs the logical steps. Good exposition gives them a way to inspect those steps without having to rediscover every reason for them.
Question | Useful evidence |
|---|---|
Does the formal argument check | The statement, proof artifact and checking environment |
Does it express the intended theorem | A careful comparison of definitions and assumptions |
Why try this approach | An explanation of the construction and failed alternatives |
Where else might it work | Examples showing which assumptions can change |
An explanation should survive a changed question
Go back to the dots and ask for the sum of the first n even numbers. The old picture cannot be reused unchanged: the new strips have lengths 2, 4, 6 and so on. One way forward is arithmetic. Each even term is one greater than the corresponding odd term, so the sum gains n extra dots and becomes n squared plus n. Another picture could arrange that total into an n by (n + 1) rectangle.
That small variation tests something that repeating the original proof does not. Can the reader identify what was special about the construction and adapt it? In a more advanced setting, the variation might replace a finite object with an infinite one or remove a regularity condition. The value of understanding appears when the question changes.
A generated explanation can fail this test while sounding excellent. It may paraphrase every line of a proof without explaining why the author introduced a particular object. Ask it what would break if that object were omitted, then check the answer against the argument. Fluency is useful for reading; the dependency between steps is what makes the explanation informative.
The mathematics advisory group explicitly distinguishes outputs understood by a responsible mathematician from outputs that nobody yet understands. Its guidance treats the work needed to develop understanding as part of a responsible release. [3] That distinction does not imply that every result in the OpenAI collection lacks a human reader.
An organisation could publish a checked argument and leave the community with a useful theorem but a difficult method. That would still be a contribution. It would also leave a substantial project for someone prepared to explain the method, simplify it or find a more revealing proof.
A sensible reading group could choose one such result and make the deliverable an explanation for the next group. Keep the formal statement beside the explanation. Show where the key construction becomes necessary, and identify the first assumption that the group could not remove. Credit the people who make that account usable.
In the dot example, the next border contains nine dots: five across the new row and four more down the new column. A reader can recover the next step from the construction. An explanation of a research result should make its corresponding choices available for someone else to examine.
Sources
One email when we publish. Research, product decisions, and what teams report back.
