Thinking about Mathematics

OpenAI has released several hundred machine-generated mathematical manuscripts. A note on the difference between proving and explaining, and on what it implies for the question whether mathematical concepts are discovered.

On 6 October 2026 OpenAI published 722 mathematical papers written by one of its models, which is not yet public.1 The model was given about four thousand open problems, and the company kept the results it judged significant. Some of the proofs have been checked by a computer, in a language called Lean; the others have not yet been checked by anyone. OpenAI also announced that it will fund workshops on how to understand these results.

This last point is the one I want to discuss. If a result still has to be understood after it has been proved, then proving it and understanding it are two different things. The difference is old, but the release turns it into a practical matter.

Proving that and proving why

Aristotle already distinguished a proof that something is the case from a proof that shows why it is the case.2 Edward Witten describes the same difference, between knowing “what” is true and knowing “why” it is true, with an example from his own work.3

The example comes from the theory of knots. The same knot can be drawn on paper in many ways, and a basic problem is to tell whether two drawings show the same knot. In 1984 Vaughan Jones found a way to attach a polynomial to every drawing, computed with a few rules applied at the crossings. He proved that the polynomial does not change when the drawing changes but the knot stays the same, by checking that each elementary move of the drawing leaves it unchanged. The proof shows that the polynomial belongs to the knot. It does not show why a quantity computed on flat drawings should capture something about a knot in space.

Witten gave the reason a few years later. He treated the knot as the path of a particle moving in three-dimensional spacetime, in a quantum field theory that ignores distances and shapes and registers only how paths are tangled. In such a theory every knotted path receives a number, and the number cannot change when the path is deformed, because the theory sees nothing except the tangling. Witten showed that this number is the Jones polynomial. Its invariance, which Jones had to check move by move, now follows from what the polynomial is. Jones’s proof was correct before and after Witten’s work; what Witten added was the reason.

Jones and Witten on the same knotLeft: two different flat drawings of the same knot, a trefoil, the second with an extra twist; an arrow marked with the elementary move connects them, and both give the same Jones polynomial. Right: the same knot drawn as the path of a particle inside a box representing three-dimensional spacetime.JONESWITTENMOVETWO DRAWINGS, SAME POLYNOMIAL:CHECKED MOVE BY MOVEA PATH IN SPACETIME: ONLY THETANGLING COUNTSTIME
Left: two drawings of the same knot, the second with an extra twist. Jones's polynomial gives the same result for both, and his proof checks this for each elementary move of the drawing. Right: Witten's picture, in which the knot is the path of a particle in three-dimensional spacetime and the theory registers only how the path is tangled.

A simpler example shows the same thing. The Taylor series of 1/(1+x²) around zero converges only when |x| < 1, although the function is smooth on the whole real line. This can be proved with real numbers alone, and that proof gives no reason for it: nothing happens to the function at x = 1. The reason appears in the complex plane. There the function has two singular points, i and −i, and both lie at distance 1 from zero. That distance is the radius of convergence.

Philosophers of mathematics have tried to say what makes a proof explanatory. For Mark Steiner, a proof explains when it uses a property that characterises the object it is about.4 For Marc Lange, it explains when it uses a feature that stands out in the result, such as a symmetry.5 Jeremy Avigad looks at the question from the side of the reader: understanding a proof means acquiring abilities, for instance being able to adapt it to a new case.6

Where the explanation is

These views raise a simple question: where is the explanation? There are two possible answers.

The first answer is that the explanation is in the proof. A proof explains because of what it does with the mathematics, whether or not anyone reads it. A correct proof that nobody has checked is still correct, and in the same way an explanatory proof that nobody has read is still explanatory.

The second answer is that the explanation is in the relation between the proof and its reader. A proof explains when it lets a reader see why the result holds, and this depends on the reader: how many steps they can follow at once, and which concepts they already have. This does not make explanation a matter of feeling. Whether a given kind of mind can follow a proof is an objective fact; it is simply not a fact about the proof alone.

Both answers have support. The first matches the way mathematicians speak, since they say that a proof explains without adding “for us”. The second matches two facts. What counts as an explanation changes over time, as Witten himself notes.3 And proofs that rest on long computer checks, such as the proof of the four colour theorem, are accepted as correct but are rarely regarded as explanations, because no one can follow them step by step.7

Until now it was hard to choose between the two answers, because every reader of proofs was human. Machines change this. If the explanation is in the proof, a machine can produce explanatory proofs, and our failure to understand them is a fact about us. If the explanation is in the relation, the question becomes for whom a proof is explanatory, and a proof that is opaque to us might be clear to a mind that can follow more steps at once.

Discovered or invented

The two answers also bear on an old question, i.e. whether mathematics is discovered or invented.

The knot example shows what makes mathematicians speak of discovery. Jones found his polynomial while working on operator algebras, a field far from knot theory, and Witten later found the same object in quantum field theory. A notion introduced in one place turned out to belong to others that nobody had in mind. The complex numbers are an older case: they were introduced to solve equations, and they turned out to explain the behaviour of real functions, as in the example of 1/(1+x²). Concepts of this kind are usually called natural, and it has been proposed that naturalness in mathematics consists in this, i.e. in appearing in the proofs that explain and in connecting results that would otherwise stay separate.8

If this is right, the question whether mathematics is discovered becomes the question of the previous section. If the explanation is in the proof, which concepts explain is fixed by mathematics itself. Natural concepts are then there before anyone finds them, and the reappearance of Jones’s polynomial in physics reveals a connection that already existed. If the explanation is in the relation with the reader, which concepts explain depends on the minds that use them. Natural concepts are then partly built: the theorems do not depend on us, but the notions that make them intelligible do.

Machines could provide evidence on this point. A system that proves many theorems will use intermediate notions of some kind. If these turn out to be our concepts, this supports the view that natural concepts are discovered. If the system reaches the same results through notions that are foreign to us and work equally well, this suggests that our concepts are one choice among several. The present release cannot settle the matter, because the model learned from human mathematics and tends to reuse our concepts. What it does show is that proving a theorem and understanding it can now happen at different times, and be done by different agents.

Cover photograph: equations on a blackboard, by Roman Mager on Unsplash.

Footnotes

  1. OpenAI, “Sharing AI progress in mathematics”, 6 October 2026, and the repository openai/math on GitHub. ↩

  2. Aristotle, Posterior Analytics, I.13. ↩

  3. E. Witten, “Adventures in Physics and Math”, commemorative lecture for the 2014 Kyoto Prize in Basic Sciences; the explanation of the Jones polynomial is in E. Witten, “Quantum field theory and the Jones polynomial”, Communications in Mathematical Physics 121 (1989), 351–399. ↩ ↩2

  4. M. Steiner, “Mathematical explanation”, Philosophical Studies 34 (1978), 135–151. ↩

  5. M. Lange, “Aspects of mathematical explanation: symmetry, unity, and salience”, Philosophical Review 123 (2014), 485–531. ↩

  6. J. Avigad, “Understanding proofs”, in P. Mancosu (ed.), The Philosophy of Mathematical Practice, Oxford University Press, 2008, 317–353. ↩

  7. T. Tymoczko, “The four-color problem and its philosophical significance”, Journal of Philosophy 76 (1979), 57–83. ↩

  8. J. Tappenden, “Mathematical concepts: fruitfulness and naturalness”, in P. Mancosu (ed.), The Philosophy of Mathematical Practice, Oxford University Press, 2008, 276–301. ↩