Today I came across an interesting IEEE Spectrum article, “Should Researchers Write Papers for AI Instead of People?”, discussing a proposal by Jiachen Liu and collaborators for replacing, or at least supplementing, the traditional scientific paper with an “agent-native” research artifact. One observation in the article struck me as especially relevant to mathematics. A conventional paper is a highly compressed, and therefore necessarily lossy, record of how research was actually done.
This is certainly true in mathematics. A published mathematics paper normally presents a clean progression from definitions to lemmas to theorems and proofs. But almost nobody actually discovers mathematics this way. A more realistic history might begin with a conjecture, followed by a proof that almost works, the discovery of a gap, a counterexample to the original conjecture, a modified conjecture, several auxiliary lemmas, another dead end, a computational experiment, and finally a reformulation in which the right theorem becomes visible. Almost all of this history disappears from the finished paper.
From the standpoint of an AI, and also of a human mathematician trying to understand how a result was discovered, the discarded material might be extremely valuable. A failed proof tells us that a particular chain of implications does not work, and often tells us precisely where it fails. A counterexample identifies a boundary beyond which a theorem cannot be extended. A false conjecture, together with the example that falsifies it, substantially constrains the space of plausible conjectures. Even an unsuccessful proof attempt may contain useful mathematical information if the obstruction can be stated precisely.
This reminds me of lectures that I attended many years ago at Rutgers by my colleague Héctor Sussmann, an excellent teacher (as well as one of the most accomplished control theorists). He was teaching an advanced graduate course, and one of the things that made his lectures so valuable was that he would often explain a proof by first showing the natural approaches that do not work. One learned not only how to prove the theorem, but why one had to prove it that way. I have occasionally tried to do the same thing when teaching undergraduates, with less successful results. I remember receiving teaching evaluations in which students complained that “the professor makes lots of mistakes.” They had understandably missed the point: the mistakes were intentional, and I was trying to show them why the obvious approaches to a problem failed. Perhaps this method works better in an advanced graduate course! But there is a serious point behind the story. Knowing why several plausible arguments fail can be an important part of understanding why the successful argument works. Our published mathematical literature preserves remarkably little of this kind of knowledge.
There is an important difference between mathematics and many other sciences. In principle, much of this information can be recorded formally. Imagine that an AI mathematical researcher works in an environment based on a language such as Lean. It proposes a conjecture, attempts a proof, discovers that a lemma cannot be established, searches for a counterexample, modifies an assumption, and tries again. Instead of retaining only the successful final branch, the system could preserve the entire research tree. Its nodes would not merely contain comments such as “this approach didn't seem to work.” They could contain precisely stated conjectures, verified implications, machine-checked proofs, explicit counterexamples, and exact records of which assumptions were used at which points.
This connects closely with what I called “theorem mining” in an earlier essay. I suggested there that AI may eventually generate enormous numbers of candidate theorems, proofs, counterexamples, and connections, stored not primarily as conventional papers but in evolving and queryable mathematical repositories. The idea discussed in the IEEE Spectrum article suggests taking this one step further. We should perhaps mine not only the results of mathematical research, but also its search history.
There is a substantial inefficiency in the way mathematics works today that such a system could address. Negative information about mathematical research is almost never recorded. Mathematicians repeatedly try arguments that other mathematicians have already tried and abandoned, simply because there is normally no place in the literature to record a failed proof strategy. A mathematician may spend several weeks discovering that a natural strengthening of a theorem is false, construct a beautiful counterexample showing why, and then omit the entire episode from the paper because it is not part of the final result. Years later, somebody else may go through essentially the same process. A sufficiently rich formal record could make statements of the form “this route has already been explored, and here is precisely why it fails” part of our accumulated mathematical knowledge.
Suppose, for example, that I want to know whether a theorem remains true after dropping compactness. Today I search the literature for a theorem answering that question and, if I find nothing, start working on it. In a theorem-mining environment, an AI might instead discover that many previous proof searches had considered precisely this generalization. Some might have failed for identifiable technical reasons, while others might have produced counterexamples. The system could retrieve those counterexamples, determine which additional hypotheses eliminate them, compare the successful and unsuccessful proof attempts, and perhaps suggest a new conjecture. “No theorem was found” would be replaced by a much richer description of what is already known about the unexplored territory surrounding the theorem.
None of this makes the traditional mathematical paper obsolete, and I would be very unhappy if it did. Mathematics is not simply a collection of formally correct statements. A good mathematical paper explains why a problem is interesting, why a definition is the right one, which ideas in a proof are important and which are technical necessities, how a theorem relates to other parts of mathematics, and what one should think about next. A formal archive containing millions of correct statements and failed proof attempts would be almost useless to a human being without some way of seeing the ideas that organize it.
Indeed, this may make the role of the human mathematician more interesting rather than less so. Machines may become extraordinarily good at exploring large spaces of conjectures and proofs, keeping track of unsuccessful branches, checking arguments, and discovering connections that would otherwise be missed. But deciding which questions are worth asking, recognizing that several complicated results are manifestations of one simple idea, finding the right abstraction, and explaining why a piece of mathematics changes the way we should think about a subject are different activities. These are precisely the things that the best mathematical exposition already does.
One can therefore imagine two complementary layers of mathematical communication. Underneath would be a large, evolving, machine-readable mathematical structure containing proofs, conjectures, counterexamples, dependencies, unsuccessful proof attempts, computational evidence, and perhaps a detailed history of how all of these evolved. On top of it would be mathematics written for people: papers, lectures, books, conversations, and expository essays whose purpose is not to reproduce the entire underlying structure but to make sense of it.
Perhaps this is a more attractive way to think about theorem mining. The goal is not to remove humans from mathematics or to replace mathematical papers by gigantic Lean files. It is to stop throwing away so much of the mathematical knowledge that is generated while we search for proofs. We could preserve that knowledge in a form that machines can use, while leaving to humans one of the things we have always done best: deciding which mathematics is interesting, understanding why it is interesting, and finding good ways to explain it to one another.
There is another human role that I find particularly appealing: that of curator. If an AI system can explore a huge space of conjectures and generate tens of thousands of formally correct consequences, the interesting intellectual problem is no longer simply to produce another theorem. It is to recognize which of those theorems matters, which one reveals an unexpected connection, which complicated collection of results is really an instance of a simpler principle, and which direction is worth exploring next. This connects with an analogy I have used before (and which I believe Terry Tao mentioned), of the mathematician increasingly becoming something like the conductor of an orchestra. The conductor does not personally play every instrument, but this hardly makes the conductor superfluous. The conductor chooses and interprets, brings different parts together, and shapes the whole into something that has coherence and meaning. Perhaps the mathematician of the future will similarly be part explorer, part curator, and part conductor, working with AI systems that can range over mathematical territory on a scale that no individual human could, while exercising the taste, judgment, and sense of direction that turn an enormous collection of mathematical facts into mathematics.
There is a small recursive aspect to this essay that seems worth mentioning. It began this morning, while I was preparing breakfast, when I read the IEEE Spectrum article discussed above, or, more precisely, when I had an AI read the article aloud to me. It made me think about how these ideas might apply specifically to mathematics and how they connect with my earlier thoughts about theorem mining. I then turned to a different AI to discuss these ideas and asked it to help me prepare this essay. What you have just read emerged from that back-and-forth process between us.