What makes a proof explanatory

Two proofs of the same theorem can differ enormously in how much they tell you. Mathematicians have argued about why for a century, and the answer turns out to matter for how we teach machines.

There is a proof that the sum of the first n odd numbers is n squared which proceeds by induction, and there is a proof which consists of drawing a square and noticing that it decomposes into L-shaped shells of sizes one, three, five, and so on. Both are complete. Both are rigorous. Only one of them tells you why the theorem is true, and almost everyone agrees on which.

This is awkward, because rigour is supposed to be the whole game. If two arguments both establish the same fact with the same certainty, on what grounds can one be better? And yet the intuition is nearly universal, survives translation between fields, and shows up in how working mathematicians choose what to publish.

The standard accounts#

The literature offers roughly three answers, none of them fully satisfying, and the disagreements between them are more interesting than any of them individually.

• Unification — an explanatory proof is one that derives the result from a principle which also derives many other results. Explanation is economy of assumption.
• Generality — an explanatory proof is one that shows the theorem is an instance of something larger, so that the specific hypotheses can be seen as inessential.
• Visualisability — an explanatory proof is one you can hold in your head as a single object rather than a sequence of steps. This is the shell decomposition.

The third is the least respectable and the most predictive. Ask a room of mathematicians which proof of the Pythagorean theorem is explanatory and the rearrangement argument wins over the coordinate computation nearly unanimously, despite the coordinate computation being shorter, more general, and more mechanically checkable.

Induction verifies that a statement is true for every n. It does not tell you what n squared has to do with odd numbers.

Why this suddenly matters#

For most of the twentieth century this was a question for philosophers of mathematics and nobody else. It became an engineering question the moment automated systems started producing proofs at scale, because an automated prover optimises for whatever you tell it to optimise for, and "shortest" is much easier to specify than "most explanatory".

The result is a growing corpus of machine-found proofs that are certainly correct and almost entirely opaque — case splits over thousands of configurations, each individually trivial, collectively meaningless. They settle the question and teach nothing. For a formal verification pipeline that is perfectly acceptable. For mathematics it is a strange kind of loss: the theorem is now known, and no one understands it.

Which suggests the useful reframing. Explanation is not a property of the proof; it is a relation between the proof and a reader who wants to do something next. The shell decomposition is explanatory because it hands you a method — decompose the object, count the shells — that transfers. Induction hands you nothing but the theorem, which is exactly what you asked for and less than you wanted.