A Proof Is More Than a Correct Answer

The sum and the reason

The sum of the first n odd positive integers is n squared. I can check a few cases, and the pattern is pleasant. One, then four, then nine. But the pleasure changes when I imagine building a square by adding an L shaped border. The next border has exactly the next odd number of dots. The answer begins to feel less like a coincidence and more like something I can inhabit.

There are other proofs. Induction can establish the same statement with a small algebraic step. Neither proof becomes invalid because I prefer the picture. What differs is the route by which the result becomes intelligible to me. That difference is a mathematical concern, even if it is not the same concern as validity.

Correct under which statement

Proof assistants such as Lean make another useful distinction visible. A proof term can be checked by a kernel against a formal statement and its assumptions. This is a powerful way to make parts of mathematical trust explicit. It also places enormous importance on having formalized the statement you actually intended.

A verified result answers the question posed in the formal system. It does not automatically explain why the result is interesting, whether the model captures the informal problem, or which of its ideas will help with the next problem. Those are not complaints about verification. They are reasons to be precise about what verification accomplishes.

I think discussions of AI in mathematics sometimes collapse these different goals into a single scoreboard. Did the system get the answer? Could the proof be checked? Did anyone learn a reusable idea? Each question matters. They do not measure the same achievement, and treating them as interchangeable makes it harder to appreciate real progress.

An explanation has a reader

My preference is for mathematical work that leaves behind a way of seeing. A proof can do this by revealing an invariant, finding the right representation, or showing why a hypothesis could not simply be removed. It gives me more than confidence that this particular conclusion is licensed.

That preference does not make long computational proofs inferior. Some truths may resist the kind of explanation I find satisfying. I should not confuse the limits of my intuition with limits on legitimate mathematics. Still, I want to preserve explanation as an ambition, especially when producing correct arguments becomes easier.

The square made from odd borders remains useful because I can carry it into another question. I can modify it, test where the picture stops working, ask what a higher dimensional version might look like. The proof has become a source of thought. That is the kind of abundance I hope better tools will create.