Human mathematics in the age of reasoning machines

Paper · Source
Knowledge After the Web

Source: Akshay Venkatesh — Annals of Mathematics and Philosophy · 2025

Abstract. This essay intertwines reflection on current mathematical practice with discussion of how it may be reshaped by automation. I speculate that the conceptual language of mathematics might undergo drastic rewritings, and look to historical examples for guidance.

Introduction. Mechanical reasoning will change not only how we do mathematics, but what it is; this must be renegotiated amongst its practitioners and with society. To examine this, I prefer to focus on humans rather than technology, and to try to understand mathematics in terms of the way we think about it, rather than its symbolic trappings. In this broad spirit I shall discuss a few topics related to automation in mathematics: in §2, some discontents of mechanization and formalization; in §3 how the conceptual language of mathematics might be changed by reasoning machines; in §4 some examples of prior shifts in this conceptual language; and finally in §5 a few thoughts about the relationship of mathematics and society. This essay is an expansion of my first Ahlfors lecture at Harvard University, entitled “(Re)imagining mathematics in an age of reasoning machines,” and some of the terminology reflects that audience: “mathematics” means solely pure mathematics, and the pronoun “we” refers to researchers and students in this field.

Related work. To think about our future, we must understand why we do what we do; and for this we must engage more deeply with our own history. The late nineteenth and early twentieth century were a period of broad disquiet in mathematics (see Gray’s article [27] for a discussion of this climate). The discovery of non–Euclidean geometry, the failure of our intuition to anticipate various classes of pathological functions, the paradoxes arising from infinite sets – all these suggested that something was, perhaps, very wrong in the subject. The response to these concerns – the “foundational crisis” – shaped modern mathematics. In a manner of speaking, mathematics suffered an anxiety attack, and responded by trying to mechanize itself. established. The result can be slightly different each time; there are, after all, different ways to axiomatize the same structure. Hilbert’s book triggered a systematic study, in the United States, of precisely this issue – “the systematic investigation of axiomatic systems for geometry, algebra, arithmetic and even mechanics,” as Van Vleck was to describe it, or “postulational analysis” as it was frequently called. Thus, for example, in 1902 Edward Huntington(4) offers a three-axiom presentation of group, which he shortly followed with a four-axiom presentation; a little later Eliakim Moore gives a five-axiom version “very desirable from the group theoretic standpoint,” and in 1905 Leonard Dickson offers a different four-axiom version. In each case, the authors painstakingly verify that each axiom is independent of the remaining ones. Such investigations were carried out for a variety of other mathematical structures too, and involved many mathematicians, including well-known names such as Theodor Hildebrandt, Oswald Veblen, R. L. Moore and (later) George Birkhoff and Norbert Wiener. See [5, 46]. Postulational analysis displays, on its surface, features that are often absorbed into the mathematical subconscious. For example, Huntington uses symbols + , < , · in his axiomatization of a Boolean algebra, in place of the more usual +, <, ·. Why so?

On account of the circles around them they are sufficiently unfamiliar to remind us of their true character as undefined symbols which have no properties not expressly stated in the postulates; while the +, · and < within the circles enable us to adopt, with the least mental effort, the interpretation which is likely to be the most useful. [32, p. 292] formulates clearly where the postulates end and the human component begins:

The postulates adopted as the basis of any system constitute the definition of that system, within its universe of discourse; and the selection of one definition rather than another as the subject for discussion is again a matter of human volition.

Method. Formal descriptions of mathematics are – partly by design, as we saw – very hard to parse. We narrate mathematics, instead, in a dialect intermediate between natural language and formal language, whose vocabulary consists of specialized terms that I will informally call concepts:

Concepts have both a communicative and a cognitive function. They are an abridged way of recording and expressing our thought process, but they are also part of our thought process itself. Like Huntington’s “combinations of symbols,” what is and is not a concept is very much a matter of human choice. How might these choices change in the future?

The answer is that it is only possible for a = b = 1. Let me contrast (without giving details) my approach to this problem with AlphaProof’s. When I see such a problem, my training predisposes me to deploy a general-purpose strategy in number theory: replace arithmetic of integers by the arithmetic of integers modulo a prime. In the case above, I consider a, b with the stated property, fix a prime p, and look at the equations enough n. Now, the advantage of arithmetic modulo p is that many tools of ordinary high school algebra apply; in this case, I analyzed (2) by taking logarithms, followed by some algebraic manipulation. This suggested to me that there would be a problem in the case that ab is equal to −1 modulo p(9) , that is, when p divides ab + 1. Analyzing that case quickly leads to a contradiction, at least for p odd. Thus ab + 1 must be a power of 2, and I ruled this out by an argument modulo 4. What about AlphaProof? AlphaProof directly guesses that it is useful to consider arithmetic modulo ab + 1. Who knows why? Perhaps it, in effect, tried reduction modulo many different moduli, to see which simplified the problem – I do not know, and perhaps it is unproductive to apply the metaphors of human thought to it. Now, doing arithmetic modulo a product pqr . . . of primes is in essence equivalent to doing separately arithmetic modulo p, modulo q, modulo r, etc.; and so, by working modulo ab + 1, AlphaProof is in effect doing arithmetic modulo all prime divisors of ab + 1 at the same time. Thus, in a sense, AlphaProof has collected arguments that I do in parallel (an analysis for each p separately) and collated them into one. For a trained number theorist it is not hard to go between the two points of view; but there is, again, enough psychological distance between them that the difference is worth exploring.

3.3. Concepts and economy of thought. It is by now a reflex for me, faced with a new question, to replace arithmetic of integers by the arithmetic of integers modulo a prime p, or to “reduce modulo p” in the jargon of number theorists. This process is mentally efficient, saving me time and memory space. It is usable across a large range of problems in number theory, so I don’t need to remember a variety of domain-specific techniques; and doing arithmetic modulo prime numbers is greatly facilitated by the fact that I can recycle intellectual constructs familiar from early schooling such as addition, multiplication, subtraction, division and logarithms, as well as associated intuitions.

You could, of course, give this argument simply by writing out all the definitions and wading through the inequalities. It would not be so hard. But the Hilbert space packages the notion of closeness in such a way that we do not have to write out the definitions every time, and it does so in a way that almost perfectly aligns with our geometric intuition about points in space, so that the last conclusion (“... then g = f +h 2 ”) becomes obvious rather than a struggle with integrals. Thus we find our psychology, our spatial intuition, reflected in the concepts by which we encode rather sophisticated mathematics – even types of mathematics, such as the inequalities above, that do not seem on their face to be geometric in nature.

Although Birkhoff offers a formal definition, I wish to interpret cryptomorphism more flexibly to mean a translation between two valid classes of mathematical statements whose mental representations are distinct.

Discussion. There are many possible visions for the conceptual landscape of mathematics in the world of automated reasoning. Which one we choose depends very much on what we want mathematics to be. It is often implicitly supposed that we all agree on the answer to this. I do not think this is the case, and even if it were, the question must be considered afresh by each generation. But mathematicians cannot consider it in isolation; we must engage, and indeed re-engage, with the world around us. I will conclude with some reflections related to this.

The study of mental objects with reproducible properties is called mathematics. [18, p. 399] 5.2. Valuing communication. Thus mathematics in the broad sense plays fundamental human roles. But the more advanced the mathematics, the more tenuous its link to these human functions. The concepts mentioned in §3, such as Hilbert spaces and rings, indeed possess the character of mental replicability – but their replication takes great effort. It takes place only within the massive infrastructure of training and education bridging the gap between natural language and the modern language of pure mathematics, and the continued existence of that infrastructure cannot be taken for granted. The separation of mathematical from natural language is part of a broader theme, the separation of mathematics as an intellectual tradition from the broader academic and cultural discourse. This is part of what the historian Jeremy Gray has called the “modernist transformation” of mathematics:

The development of mathematics as an autonomous research field enabled us to probe structures of profound complexity, to a depth that could never have been matched were we constantly called to account by the society around us. But this came at a very high cost. As we forgot more and more about the rest of human thought – and here I include humanities and the arts as much as the sciences – we also developed a creeping amnesia about ourselves; we lost the narratives that help us understand the “value and meaning” of what it is that we are doing. Of course, most mathematicians would agree there is something very special about doing mathematics, or we would not do it; we experience it as an activity with intrinsic meaning, one that requires little external validation. But our ability to share this experience outside the narrowest circle of peers has become diminished, and the loss is ours, too.

112 A. Venkatesh M×Φ vol. 3, no. 1 Despite this gulf, our mathematics remains, in the final analysis, a servant of the broader culture around us. It is a tool for individual and collective thought and will only survive to the extent that it remains useful as such. And while our relationship to knowledge and scholarship will surely be transformed by artificial reasoning, just as it was transformed long ago by writing, the need for thought, alone and together, remains undiminished. Mathematics surely has its role to play in this, but we cannot take for granted that this role looks the same as it did in the past. Thus, as mathematicians consider our future, our thinking about how the field should evolve cannot stop at our doors. Rather, we need to engage in a much more serious dialogue with the intellectual world outside our borders; and for this we need to recenter communication in our conception of mathematics. As is so eloquently expressed by Davis and Hersh, communicability is not an afterthought to mathematics, but part of its very definition.

Lines of inquiry this paper opens 7

Research framings built by reading the notes related to this paper — the questions it feeds into.

Can formal verification substitute for human understanding of AI proofs? How does model scale affect fine-tuning and downstream task performance? Can scaling alone produce compositional generalization in neural networks?