1. Geoff Hinton has said lots of stupid things about AI.
2. In some sense it feels like researchers at the more elite schools are *more* threatened by these developments. I'm just a humble math professor trying to make an honest living as a teacher-scholar. I'm not trying to solve Millenium Prize problems. I've always thought teaching was an essential pillar of my calling, since long before the AI explosion. In fact, I've always thought that giving a talk at a conference is part of that pillar.
3. Which brings me to my next point. The mathematicians *I* interact with (including some very, very good ones) certainly don't *seem* to cling to this "honor code" as you call it (though maybe they do, behind my back?). It's more about what you bring to your particular intellectual community. But then again, maybe this is because, as I said, I'm not trying to knock out age-old conjectures.
4. We did not sell a bill of goods to 8 billion people. 99% of the planet has no idea what we do and never did. They probably assume we get paid to teach (which, to be fair, is true). Even the funding that is given out by the government for us to do research is largely allocated by...us. This is an impressive situation. It seems the people who need most convincing that mathematics will still be useful in the future are mathematicians. OK maybe computer scientists too.
5. All of the hand wringing about how college degrees are going to be worthless misses an extremely important point. According to an intellectual's criteria for utility, college degrees *already are* useless and have been for many years, probably decades. AI has certainly made cheating much easier (seriously, people, stop grading homework!) but students always found ways to cheat. What's interesting is that when I talk to prospective students, they actually don't seem to be that down on the whole idea of college. The drop in demand for college these days has much more to do with the demographic cliff than with AI. What value exactly people get out of going to college is a huge complex issue, but I can assure you it is mostly not intellectual.
6. I try to remain mostly optimistic about what AI can do for us mathematicians, at least in the short run. If it can prove lemmas and theorems for us, great. Calculators brought an end to one kind of doing math, AI will bring an end to another kind. In the long run, though, I gotta say there is something deeply unsettling about the confident prediction that, sure, machines will eventually be better than humans at math in every way, including creativity. When that is the case, I think there is literally nothing that they need humans for--those same skills will also make them scientists and engineers and anything they want ("want"??) to be. If they can "understand" the world in even greater clarity than we can, then basically this planet belongs to them. So, yeah, for me it's hard to just casually read over such predictions and think "oh yeah of course why not." And when I read this whole thing from that perspective, I think, are we even talking about the right thing?
Thank you Jameson, interesting feedback as always.
Re: the honor code. What I found (but this may very from one community to the other) is that many mathematicians are happy to value teaching and expository work, but still bow to theorem-proving-flex in specific contexts, especially for hiring. Also, there is also notable absence of sizable prize opportunities / prestige career tracks for anything but theorem-proving. (Sure, there are exceptions, but they are fairly minor.)
Re: college degrees… I’m reporting a fear that is present. Like you, I see this as a more complex situation that predates the AI issue (I discussed this in my earlier piece on AI & academia, https://davidbessis.substack.com/p/letter-to-a-phd-student)
The "closed system" framing is worth pushing on because it collapses under foundational scrutiny. Logicism, formalism, intuitionism, and predicativism give genuinely different answers to what mathematics is, and Gödel ensured no single answer could be complete. Excluded middle, impredicative definitions, proof by contradiction - these remain contested. Brouwer, Weyl, and Bishop worked seriously within frameworks that reject large portions of what Mathlib assumes. ZFC plus classical logic is a philosophical commitment, not neutral ground..
The 200,000-line blob is more troubling than the accretiveness argument alone captures. Every formal verification inherits unresolved foundational commitments, and an unreadable proof makes it impossible to assess which assumptions are doing the real work. Kontorovich's canonization is precisely the process of making those commitments visible and negotiable, embedding results into the corpus in a way that exposes what is actually being assumed. A proof nobody can follow forecloses that negotiation rather than contributing to it.
Your point about intelligibility being structural rather than aesthetic is right, but the foundational picture strengthens it considerably. Mathematical truth was never independent of the framework in which a proof was constructed, always relative to axioms chosen and logic adopted, with canonization as the mechanism by which those choices got examined and refined. When a human proves something difficult, the proof demonstrates comprehension of that framework... vs the blob which demonstrates only that the kernel accepted it.
Spoken like a true intuitionist (I presume). Personally, I believe Platonism gives us the complete answer, and even the incompleteness theorems of Gödel.
When a human proves something difficult, they prove that they understand the very essence of the problem; which is usually not related to some logical framework in any interesting way. For example, to quote Grigori Perelman when he was asked about the axiom set that makes his proof true: "I don't know, and I don't care."
Platonism doesn’t remove the need to specify a framework—it just asserts that something exists beyond it. But proofs, verification, and disagreement all happen within frameworks. My point is about that level: if a proof is unintelligible, we lose the ability to see which assumptions are doing the work, regardless of whether you think the result is “true” in a Platonic sense.
It seems to me that one could apply many of your arguments to research in general (including research in non-mathematical disciplines) especially in those disciplines that try the hardest to maintain a distinction between 'pure theory' and 'application' and also between 'teaching' and 'original research'.
This is the most insightful and serious discussion of the implications of recent AI advances on mathematics I've seen so far. No regrets over reading the 35 pages!
I am more pessimistic about academia and more optimistic about mathematics.
The pessimism first: The college system, at least in America, seems too big of a ship to turn, even if the captains weren't asleep at the wheels. Faculty might be doing research but are paid for teaching, most of it at the undergrad level. AI destroys the signaling value (via assignment cheating) while simultaneously creating cheap competition for the learning value (GPT-5.4 is a patient explainer and certainly competent enough to replace a undergrad lecturer). Given that the other two legs of the student experience (socializing and matchmaking) have been broken under the weight of administrative pressure over the last two decades, and even the role of colleges as an immigration pipeline is under attack now, I don't see what could stabilize the colossus once it starts tumbling. But teaching aside, the most telltale sign of universities' decline is how little they have contributed to what is clearly the main industrial innovation of the last decade: The WWW was half an academic project; the free software ecosystem (which later gave us Android) was still to a large extent developed at colleges; but the role of universities in modern AI is... basically standing in the peanut gallery and occasionally writing "something with AI in the title" papers for all I see.
But I'm in maths because I want to know answers to my questions, and on that front I'm only seeing progress. Around a month ago I realized that GPT-5.4 can actually solve some problems I was struggling with (as long as I was ready to sift through a lot of plausible-sounding bullshit). It one-shotted three of my long-standing MathOverflow questions (I still had to fill in some details, but GPT's output would have passed as a proof in a mediocrely written paper), and helped enough with another that I could finish the solution myself. The proofs were all on the computational side, but this doesn't mean straightforward; the AI had to guess the right formulas to induct on, sometimes several times. The proofs were not obvious in hindsight, but also -- except for one case -- not overly full of unmotivated tricks; I learnt new things from each of them. You can judge for yourself:
In terms of accretion, I think these aren't any worse than the typical useful paper. We don't usually motivate our proofs either, and much of the time we can't, since our discovery process is 90% subconscious and resists verbalization. Sometimes we tell a good just-so story afterwards, but that's not necessarily better than whatever parallel-constructed rationalization a reader comes up with. Even Euler's results on formal power series aren't fully "explained" yet.
The divergence between formalization and readable exposition has been a problem for decades; it has been plaguing every proof assistant in history. In fact the inability of proof assistants to break through the usability barrier -- for reasons that are not even easy to articulate -- has been a major reason why I was so skeptical of AI timelines as late as a year ago. But AI actually offers a new approach to this problem: generate formal proofs (in Lean) and informal proofs (in TeX) simultaneously, with the objective function (besides correctness of the formal proof) being the speed at which a different (possibly weaker) AI can formalize the informal proof, divided by the length of the latter. This doesn't look much harder than what Fabian Glöckle has done in https://arxiv.org/abs/2604.03071 (he built a whole in-silico maths community out of agents), and I think it's only a matter of time until someone tries it. If it works, we'll have LLMs generate proofs that are both correct and readable. Whether they will be *conceptual* and *inspiring* are different, more subjective questions, but these qualities are already rare in existing human-authored mathematics.
Eliminating the overhang might not be a bad thing! I have given up on several projects when I learned the answers were *probably* in the literature. If there was an easy way I could extract them from that literature, I would feel a lot better about that! A very natural question about Coxeter groups (do they have spin extensions like in type A? details at https://mathoverflow.net/questions/285263/a-spin-extension-of-a-coxeter-group ) sits unresolved because I find the existing work impenetrable to an extent I'm not sure if it even claims (let alone proves) an answer. Yet I've seen people just assume the result as if it was well-known. Do I want to invest a couple weeks into what would then likely be unpublishable? No, but I would happily invest a hundred tokens and share the answer with the community. (Right now GPT is not good enough for this yet; generally, it struggles with injectivity proofs.)
Thurston is right. It's not about what you contribute to *mathematics*, it's about what you contribute to *humanity*.
We have to take a step back and ask, what does mathematics as a whole contribute to humanity? In academia it's easy to get distracted and only pay attention to what other academics think. But every academic field needs to be useful outside of its own bubble, or else it will dwindle over time as nobody else cares, nobody wants to fund it, and young people don't want to go into it.
The real danger to human mathematicians is not that some AI will prove more theorems than they can. It's that people might stop needing human mathematicians for anything other than satisfying the aesthetics of other human mathematicians. If the physicists stop needing mathematicians because the math AI works better for them. And the computer scientists, and the experts in every other field of science and engineering.
Thank you for this. There are so many thoughts here that I love, but this one is really standing out:
"Problem solving is just a means to an end. The core payout of pure mathematics is the neuroplastic elevation of our worldview, and we can’t get there by copy-pasting the result."
This is a feeling to which any human who enjoys learning can relate, mathematician or not. What if the core payout of living is "neuroplastic elevation of our worldview" instead of "copy-pasting" historical solutions to our problems?
I'll be thinking carefully about how we might define "neuroplastic elevation of our worldview" more precisely. :-D
Thank you for the excellent post! But why adapt a defeatist tone and uncritically accept the claims/rationale of AI companies when we can do the math?
For instance let's look at the results that seem to have initiated the post:
1- Math Inc. basically hijacked an existing formalization effort and brute force vibe coded the reminder of the project, by throwing an unknown amount of MathPhd+GPU hours at it to snatch a PR victory. To cite Math Inc press release, no one seems to bother with papers anymore, the project at that stage only required "six more months of work" and already had "a detailed blueprint and developed an extensive codebase consisting of new definitions and theorems". We have no information whatsoever about the nature of the system (Gauss) that was used, the level of human input or computational resources that went into producing the formalization. And the grand result is an intelligible/useless formalization of a result of which the correctness was never in doubt and whose only function seems to be discouraging people from working on the project...
2- On First Proof, the best performing team from DeepMind, claims to have solved 6 out of 10 lemmas using their Alethia agent. 2 (Problems 9 and 10) of those later turned out to have been solved in literature. And when we look at the paper from Deepmind we see that they ran two versions of their agent based on different base models of which each individually solved at best 4 of the problems. In each round each models submitted 2 candidate solutions which were then evaluated by human experts. Again we know almost nothing about the base model or the specifics of the scaffolding including whether they were modified/fine tuned for the type of problems in First Proof. The same goes for how many attempts/rounds of verification and the computational resources that went into producing the results (All we know that keeping track of it requires a logarithmic scale! (see the original Alethia paper)). And even if we interpret the results in the most charitable way possible, one would only have a ~20% chance of getting a correct solution on a randomly selected problem - assuming that one is willing/capable of checking them in the first place. And if we look at their results on Erdos Problems they managed to "solve" 13 out of 700 problems of which only one (Problem 1051) survived closer scrutiny and even that single “autonomous” result turns out to be hand selected, corrected and formalized by human mathematicians. Frankly I am hard pressed to think of a more absurd way of doing mathematics! - unless one has a well paid job at an AI company of course.
Re defeatism: I don't think my article is defeatist. Elsewhere, I have been blamed for not being defeatist enough. In truth I simply tried to be accurate. The First Proof assessment is that of Litt, who has directly looked at it (I haven't).
Of course there are many more levels to defeatism like Avigad, Hinton and C. Szegedy. But still I am having a hard time reconciling statements like the ones bellow with the actual state of "AI for mathematics" - which has yet to produce a single original proof/significant contribution to mathematics despite the huge resources and talent being poured into it:
"If theorem-proving remains their only official currency, all research mathematicians run the risk of becoming demonetized in the course of the next few years."
"This might be the largest product recall in memory—we sold a bogus idea of math to billions of people, and the bill is coming due."
"These will be difficult years for mathematicians. Students will desert. Money will dry up. Postdocs will ask pressing questions and senior faculty will have to come up with answers. At parties, people will start giving them weird looks, as if they had become living fossils."
I believe that mathematicians will be far better off applying the logical rigor and meticulous scrutiny that is characteristic of their discipline to the claims of AI labs who as you said are "barely engaging with mathematics itself, its core problems and significance" rather than silently retreating into the cloak of metaphysics in the face of fantastical claims of impending “super-human mathematician AI”.
I think you are underestimating the public relation aspect. Even if unjustified by the fundamentals, it creates conditions that are extremely difficult to navigate, individually and collectively, and has many real-life consequences.
I agree the PR situation is impossible especially for mathematicians in academia. And of course the funding situation, especially in the US, makes collaborations with the AI-industry/funding from venture/crypto capital hard to resist (as for instance in the case of Terence Tao and SAIR, Timothy Gower's G-research project or his recent paper/collaboration with OpenAI, Avigad's Center for F. Mathematics just to name a few.) So speaking out against the "Superhuman AI mathematicians" hype in a way that goes beyond mumbling something like "but Mathematics is more than just proving theorems" in the current climate is probably the worst thing one can do for their academic career at least in the short run.
Nevertheless I don't believe this is reason enough to lower our scientific standards to the level where we uncritically accept every claim that comes out of an AI-lab/startup let alone to throw Mathematics under the AGI-hype train. Especially when we have all the reasons to believe that the most likely outcome of this episode will be the AGI fantasies of the tech industry dying on the hills of Mathematics rather than Mathematics dying at the altar of some superhuman oracle. Unfortunately, the damage will already be done either way.
This reminds of one of David Hilbert's lectures where I last saw the Carl Jacobi quote “the object of mathematics is the honor of the human spirit.” you cite :
"Whoever feels the truth of the generous way of thinking and worldview that shines forth from these words of Jacobi's will not fall prey to regressive and fruitless skepticism; such a person will not believe those who today, with a philosophical air and superior tone, prophesy the downfall of culture and content themselves with the Ignorabimus. For the mathematician, there is no Ignorabimus, and, in my opinion, for natural sciences not at all either." [David Hilbert, Naturerkennen und Logik]
I see everything you write compatible with everything I wrote.
This might no be transparent from the "defeatist" passages about the PR debacle, but I hold the seemingly contradictory yet consistent view that our notion of creativity is misconstrued and AI is about to teach us painful lessons (hence my tentative elaboration on the Overhang) AND that AI is about to hit harder roadblocks than the AGI prophets anticipate (hence the "optimistic" conclusion).
Thank you David for a lovely, deep and insightful article. I have several questions/thoughts/reflections. I wanted to spend time weaving them into a coherent whole, but I don't think I can, so I just put them out there. Would love to hear your thoughts if you time.
I'm a computer scientist, who (like many computer scientists) mainly spends their time proving lemmas and theorems. I like to summarize this branch of computer science as the mathematics of Turing machines. I decided to pursue computer science rather than mathematics, which I also deeply love, because of a lifelong fascination with (efficient) mechanical computation. Inevitably, this frames my questions.
1. I notice this trend towards saying (extremely crudely summarized) that the proving is the comparatively easy bit once the definitions and structures are in place. I really don't understand this -- although perhaps it is something that holds true in pure mathematics? I am frequently confronted by statements that turn out to be true but take months or years of effort to prove, whereby the obstacle is not a lack of appropriate definitions or structures, but putting all the pieces together in the correct way, which can require a lot of creativity. It sometimes feels like the "proofs are the comparatively easy bit" thesis is somewhat circular: "proofs are the comparatively easy bit once you have the proof"?
2. Relatedly: I fully understand and endorse the concerns around truth, meaning, canonicalization... the idea that the journey and the lessons learned for yourself and others is at the very least as important as the destination. But sometimes, simply knowing that a statement X is true can be an essential building block for larger truths, even if you don't have a (deep) understanding of why X is true. So can black-box truths, obtained by whatever means, not in themselves be part of larger palaces of mathematical truth? (Of course, later on we might realize that we need to understand WHY X is true, and then we will re-open it, but until then...?)
3. You mention the 1976 proof of the Four Colour Theorem. I find it a deeply beautiful proof, the synthesis of human insight, to reduce an infinite number of cases to finite cases, and mechanical enumeration. But of course, it remains controversial because of the mechanical-enumerative part (despite formalizations in Coq etc). I understand the feeling of uneasiness that this proof generates, and why.
It is of course not an AI-driven proof, but I keep asking myself: what would happen if, rather than 1976, Appel and Haken's proof was published today? How would we respond, given current developments, and what role would we give it in our epistemic discussions? Most provocatively: would it, should it, end up in Mathslop?
Incidentally, on June 21st 2026 it will be exactly 50 years since its announcement. Such a quirk of history, given current developments...
Thank you Steven! Your questions would probably a full post, especially the first one. Here’s a quick take.
To put the pieces together, you usually need something other than brute force. Even without new definitions, you might rely on a latent pre-conceptualisation. If you’re not seeing this as visible concepts, it might be that your proofs aren’t yet fully canonized, in the sense of becoming a simple chain of trivialities once you’ve made explicit the right conceptual structure (like Grothendieck’s most profound things). Another options is that your domain is intrinsically more computational (see point 3 below), but in my experience this is rarely the case.
Yes, there is some value in knowing things are true even if you don’t understand them. This intermediate status isn’t devoid of value, but it isn’t terminal (unless… see 3 below).
Yes, the four colour theorem would qualify as Mathslop, but there’s a nuance—in all likelihood, it can’t be proved in a non-Mathslop way.
There are theorems whose proofs can’t be conceptualized, because there’s just too much “entropy” (can’t think of a better word) in the result itself. The classification of simple groups, or Hales’s theorem, might belong to the same category. But Viazovska’s results are different, in the sense that we know that the proof can be made much more conceptual (which is remarkable, since she solved in dim 8 and 24 the same problem Hales solved in dim 3 with a structurally Mathslop proof). So it’s much more frustrating to be happy with a Mathslop autoformalization of her results.
Hi Steven, I think framing the topics here around computation is indeed very interesting.
Basically David suggests that there are valuable bits in math which, even after the formal computation runs, are not yet fully "captured". I think this observation has impact even beyond the "human side" of math (community, careers, education, etc); it is a real "computer-science" truth since, when humans have a clear mental picture of something, they form some kind of "compression" of the huge chunk of "verify this, verify that" MathSlop, and we know that compression is intelligence.
So the question is, once machines "compute" a proof in, eg, Lean, can they compress it?
This reminds me of another point: AI models can interact with language servers at a speed faster than any human, but they currently lack the ability to, say, "fork" a language altogether and implement language traits suitable for specific challenges. AI can write rust better than me, but we cannot count on AI to come up with the next rust for now.
That brings me to a crude comparison: mathematicians each have their own fork of "mathlang", where the same math definition, while seemingly identical in the "official math" sense, can differ wildly in the secret math sense. This makes understanding math difficult since we see someone call an API we know but still cannot understand what they're doing, for there is a secret documentation of this API living in the brain of that mathematician... I"ll stop this slop now... haha...
You're right to say that these conceptual mistakes aren't particular to mathematics. When you follow the reasoning of people like Hinton, though no one dares put it this way, they also think that great tranches of the physical sciences are a closed system - sure, experiments are important for 'empirical confirmation', the story goes, but in ideal terms, no interaction with the world is necessary.
This is a belief in the Triumph of Theory: our ability to brute force an understanding of the world by devising the right combination of sentences and equations to describe it, all of which is already latent in folk descriptions. In the end, they'd have you believe that you can take a large enough model that hasn't read any physics, say to it "did you know that apples fall from trees?" and it'll come up with Newton's laws.
This is part of an ancient delusion which has overlooked the real sources of human creativity, first because it cannot understand them and second because it fears the realisation that they exist outside of language. We feel that language is what gives us control; to place our prowess outside of it is almost to take away our freedom.
The particular situation of mathematics is therefore symptomatic of a deeper failure of human self-understanding. In naively optimistic moods, I hope that - though the road will be rough - the eventual failure of AI to capture creative mathematics will be impetus for a widespread re-examination of what we think we are. But realistically, we're going to be told that we didn't buy enough GPUs and that we didn't use the tools in the way we were supposed to. The role of intuition will only be accepted when it can be built and sold.
I find it amazing how you manage to hit all the interesting aspects of AI for math in your exciting article, but come away with basically the opposite conclusions than me for many of them.
I think your belief that neuroplasticism provides a better foundation than platonism to explain mathematical activity has something to do with it :-)
In particular, I don't think that developing the right concepts for difficult theorems is something that is particular to us humans. I think anyone, even AI, will have to come up with the right concepts and definitions in order to prove difficult theorems. The Math inc scoop was not about scooping the fields medal winner. It was about scooping people who formalised concepts in Lean that had already been conceived before, in order to prove the theorem. If mathlib poses conceptual challenges beyond the concepts in the published proof, well, I think that is due to mathlib and type theory.
So proving difficult theorems will remain an important measure, and yield important insights, as before. If an AI proves the Riemann hypothesis first, it will *undoubtedly* also introduce the necessary concepts to do so. There are already many mathematicians much more powerful than me in proving theorems; if I can use an AI to prove the theorems I need in my application, splendid.
And I think that is what will make mathematics more important and embedded in our culture and work life than ever: It is the correct way to think about many problems, and that doesn't change with AI. What AI will give us is that once you manage to think in math, solving the problems you think about will suddenly become much easier.
I never said concept building was specific to human. I simply noted that current systems, while obviously built around a latent concept architecture, are extremely poor at canonization.
I am not sure that is entirely true. Maybe canonization with respect to mathlib, but people like Peter Scholze refused in the past to interact directly with Lean for a reason. Maybe the AI shares that sentiment. Math is already pretty canonical, why can we not just use this existing structure for the prover? I've seen good results telling the AI to first think informally and conceptually through a proof, then sketch the proof formally, then complete the full formal proof, building any needed proof tools in the process, when the formal language is closely aligned with the informal one. They don't seem to be able yet to invent new concepts, but are pretty good at discovering and reusing existing concepts (the Overhang). In case of the Math inc scoop, that 200K blob was probably just the easiest and messiest formal proof they could rush out *based on an existing informal proof*. If tasked with formalising something entirely new, I don't think that messiness would necessarily pay off (depending on how large the ocean is, of course).
Why cannot explicability (including explicability of theorems proved by AI) be something that math's master or phd students can get credit for in their studies? Seems like a great learning experience and an opportunity to contribute.
This is really, really good. And some thoughtful comments here that echo some of what I want to say.
I’m not a mathematician, but I did study the foundations of mathematics and logic in grad school. To this day, I think Wittgenstein remains the best guide here. He would reject both the platonism and the psychologism you describe. Neuroscience has nothing to offer us here, please don’t be misled by that. But math isn’t metaphysically mysterious either. Adding, following a rule, stating assumptions — these are things we do. They’re part of our form of life. Not “merely” so; Wittgenstein’s quietism consists in the rejection of both platonism and psychologism as genuinely intelligible philosophical views. The question they thought they were trying to answer is supposed to dissolve when you’ve done the work of philosophical therapy.
One of the reasons I’m skeptical that LLMs will contribute much to math in the devastating ways you describe is because the intelligibility scaffolding that supports proof-work is just so deeply enmeshed in our other social practices that it’s hard to imagine an LLM getting it without being, well, enmeshed in our social practices.
It’s common in cogsci and AI research to think of intelligence as a natural kind, g, that organisms have more or less of. But in biology this view has fallen out of fashion — most accept that intelligence isn’t one thing, but a way of describing different responsive practices to widely varied ecological niches. Which says nothing about the epistemic status of math or logic!
If mathematicians fetishized the proof over the “shadow math” of scaffolding and canonization, it was probably because they were uncomfortable with the epistemic status of that work. LLMs will hopefully force a reckoning where they actually realize these practices weren’t epistemically precarious at all — so they can re-value that work to shift the professional incentives you describe. Public defensibility is another story.
Excellent articulation of the threat AI poses to the current dynamic of mathematics….it will be interesting to see what all can be achieved if we embrace the technology, rather than oppose it out of fear of displacement
This was an incredibly insightful article. I really enjoyed reading it. However, I still think this is
somewhat of a retreat in that one is abandoning a central aspect of why one does mathematics. This aspect is the allure of and thirst for discovery. A characteristic embodied by Grothendieck and his school (mentioned in the embedded image).
Assuming that AI does outpace humans in sheer mathematical capability, is there a place left for human discovery in pure mathematics? Under this assumption, the human practice of doing mathematics will be restricted to the lecture hall or classroom. The extent of discovery for the mathematician will be limited to deciphering a proof given by AI. The days where mathematicians will explore the beautiful and mysterious realm of mathematics will be finished. The role of discovery will be overtaken by AI, which will discover and then "report" back to the human. Note, even this can be considered optimistic since why couldn't an AI explain a complex proof to a human being better than any other human could? Hence, the role of the mathematician, it seems, would be solely restricted to a student in a classroom.
The importance of the “right” definition, I believe, raises a fundamental obstruction for AI in ever achieving capabilities of mathematical discovery similar to that of humans. However, if we assume AI discovered a valid proof of the Riemann Hypothesis, I think AI would have already overcome this obstacle. Hence, it seems it would be a hindrance for mathematical discovery if humans were creating the definitions but not finding the theorems.
I agree that human understanding is a fundamental reason why one does mathematics. However, I think that the thirst for discovery is another just as crucial aspect. I would love to hear your thoughts. I hope I am making sense.
A few thoughts.
1. Geoff Hinton has said lots of stupid things about AI.
2. In some sense it feels like researchers at the more elite schools are *more* threatened by these developments. I'm just a humble math professor trying to make an honest living as a teacher-scholar. I'm not trying to solve Millenium Prize problems. I've always thought teaching was an essential pillar of my calling, since long before the AI explosion. In fact, I've always thought that giving a talk at a conference is part of that pillar.
3. Which brings me to my next point. The mathematicians *I* interact with (including some very, very good ones) certainly don't *seem* to cling to this "honor code" as you call it (though maybe they do, behind my back?). It's more about what you bring to your particular intellectual community. But then again, maybe this is because, as I said, I'm not trying to knock out age-old conjectures.
4. We did not sell a bill of goods to 8 billion people. 99% of the planet has no idea what we do and never did. They probably assume we get paid to teach (which, to be fair, is true). Even the funding that is given out by the government for us to do research is largely allocated by...us. This is an impressive situation. It seems the people who need most convincing that mathematics will still be useful in the future are mathematicians. OK maybe computer scientists too.
5. All of the hand wringing about how college degrees are going to be worthless misses an extremely important point. According to an intellectual's criteria for utility, college degrees *already are* useless and have been for many years, probably decades. AI has certainly made cheating much easier (seriously, people, stop grading homework!) but students always found ways to cheat. What's interesting is that when I talk to prospective students, they actually don't seem to be that down on the whole idea of college. The drop in demand for college these days has much more to do with the demographic cliff than with AI. What value exactly people get out of going to college is a huge complex issue, but I can assure you it is mostly not intellectual.
6. I try to remain mostly optimistic about what AI can do for us mathematicians, at least in the short run. If it can prove lemmas and theorems for us, great. Calculators brought an end to one kind of doing math, AI will bring an end to another kind. In the long run, though, I gotta say there is something deeply unsettling about the confident prediction that, sure, machines will eventually be better than humans at math in every way, including creativity. When that is the case, I think there is literally nothing that they need humans for--those same skills will also make them scientists and engineers and anything they want ("want"??) to be. If they can "understand" the world in even greater clarity than we can, then basically this planet belongs to them. So, yeah, for me it's hard to just casually read over such predictions and think "oh yeah of course why not." And when I read this whole thing from that perspective, I think, are we even talking about the right thing?
Thank you Jameson, interesting feedback as always.
Re: the honor code. What I found (but this may very from one community to the other) is that many mathematicians are happy to value teaching and expository work, but still bow to theorem-proving-flex in specific contexts, especially for hiring. Also, there is also notable absence of sizable prize opportunities / prestige career tracks for anything but theorem-proving. (Sure, there are exceptions, but they are fairly minor.)
Re: college degrees… I’m reporting a fear that is present. Like you, I see this as a more complex situation that predates the AI issue (I discussed this in my earlier piece on AI & academia, https://davidbessis.substack.com/p/letter-to-a-phd-student)
The "closed system" framing is worth pushing on because it collapses under foundational scrutiny. Logicism, formalism, intuitionism, and predicativism give genuinely different answers to what mathematics is, and Gödel ensured no single answer could be complete. Excluded middle, impredicative definitions, proof by contradiction - these remain contested. Brouwer, Weyl, and Bishop worked seriously within frameworks that reject large portions of what Mathlib assumes. ZFC plus classical logic is a philosophical commitment, not neutral ground..
The 200,000-line blob is more troubling than the accretiveness argument alone captures. Every formal verification inherits unresolved foundational commitments, and an unreadable proof makes it impossible to assess which assumptions are doing the real work. Kontorovich's canonization is precisely the process of making those commitments visible and negotiable, embedding results into the corpus in a way that exposes what is actually being assumed. A proof nobody can follow forecloses that negotiation rather than contributing to it.
Your point about intelligibility being structural rather than aesthetic is right, but the foundational picture strengthens it considerably. Mathematical truth was never independent of the framework in which a proof was constructed, always relative to axioms chosen and logic adopted, with canonization as the mechanism by which those choices got examined and refined. When a human proves something difficult, the proof demonstrates comprehension of that framework... vs the blob which demonstrates only that the kernel accepted it.
Spoken like a true intuitionist (I presume). Personally, I believe Platonism gives us the complete answer, and even the incompleteness theorems of Gödel.
When a human proves something difficult, they prove that they understand the very essence of the problem; which is usually not related to some logical framework in any interesting way. For example, to quote Grigori Perelman when he was asked about the axiom set that makes his proof true: "I don't know, and I don't care."
Platonism doesn’t remove the need to specify a framework—it just asserts that something exists beyond it. But proofs, verification, and disagreement all happen within frameworks. My point is about that level: if a proof is unintelligible, we lose the ability to see which assumptions are doing the work, regardless of whether you think the result is “true” in a Platonic sense.
If you have a machine proof, you can just filter for the used axioms. In that sense, no machine proof can ever be unintelligible.
It seems to me that one could apply many of your arguments to research in general (including research in non-mathematical disciplines) especially in those disciplines that try the hardest to maintain a distinction between 'pure theory' and 'application' and also between 'teaching' and 'original research'.
This is the most insightful and serious discussion of the implications of recent AI advances on mathematics I've seen so far. No regrets over reading the 35 pages!
I am more pessimistic about academia and more optimistic about mathematics.
The pessimism first: The college system, at least in America, seems too big of a ship to turn, even if the captains weren't asleep at the wheels. Faculty might be doing research but are paid for teaching, most of it at the undergrad level. AI destroys the signaling value (via assignment cheating) while simultaneously creating cheap competition for the learning value (GPT-5.4 is a patient explainer and certainly competent enough to replace a undergrad lecturer). Given that the other two legs of the student experience (socializing and matchmaking) have been broken under the weight of administrative pressure over the last two decades, and even the role of colleges as an immigration pipeline is under attack now, I don't see what could stabilize the colossus once it starts tumbling. But teaching aside, the most telltale sign of universities' decline is how little they have contributed to what is clearly the main industrial innovation of the last decade: The WWW was half an academic project; the free software ecosystem (which later gave us Android) was still to a large extent developed at colleges; but the role of universities in modern AI is... basically standing in the peanut gallery and occasionally writing "something with AI in the title" papers for all I see.
But I'm in maths because I want to know answers to my questions, and on that front I'm only seeing progress. Around a month ago I realized that GPT-5.4 can actually solve some problems I was struggling with (as long as I was ready to sift through a lot of plausible-sounding bullshit). It one-shotted three of my long-standing MathOverflow questions (I still had to fill in some details, but GPT's output would have passed as a proof in a mediocrely written paper), and helped enough with another that I could finish the solution myself. The proofs were all on the computational side, but this doesn't mean straightforward; the AI had to guess the right formulas to induct on, sometimes several times. The proofs were not obvious in hindsight, but also -- except for one case -- not overly full of unmotivated tricks; I learnt new things from each of them. You can judge for yourself:
https://arxiv.org/abs/2604.13619 (the key is Theorem 0.11, and while I still find it mysterious, I also find it beautiful)
https://mathoverflow.net/questions/164601/central-idempotents-from-characters-in-frobenius-algebras-generalizing-lusztig/509672#509672 (in hindsight, the only trick here was to take a very simple example and modify the trace form a bit)
https://mathoverflow.net/questions/26520/rational-congruence-of-binomial-coefficient-matrices/509509#509509 (maybe it would have been easy to anyone who knew Kravchuk polynomials; maybe it's even a known result about them; but nothing in the problem shouted "Kravchuk polynomials" at me)
https://mathoverflow.net/questions/420318/proving-the-spectrum-of-the-young-jucys-murphy-elements-by-formal-computation-in/509909#509909 (this one took lots of back-and-forth and work of my own, and the proof is rather long and weird).
In terms of accretion, I think these aren't any worse than the typical useful paper. We don't usually motivate our proofs either, and much of the time we can't, since our discovery process is 90% subconscious and resists verbalization. Sometimes we tell a good just-so story afterwards, but that's not necessarily better than whatever parallel-constructed rationalization a reader comes up with. Even Euler's results on formal power series aren't fully "explained" yet.
The divergence between formalization and readable exposition has been a problem for decades; it has been plaguing every proof assistant in history. In fact the inability of proof assistants to break through the usability barrier -- for reasons that are not even easy to articulate -- has been a major reason why I was so skeptical of AI timelines as late as a year ago. But AI actually offers a new approach to this problem: generate formal proofs (in Lean) and informal proofs (in TeX) simultaneously, with the objective function (besides correctness of the formal proof) being the speed at which a different (possibly weaker) AI can formalize the informal proof, divided by the length of the latter. This doesn't look much harder than what Fabian Glöckle has done in https://arxiv.org/abs/2604.03071 (he built a whole in-silico maths community out of agents), and I think it's only a matter of time until someone tries it. If it works, we'll have LLMs generate proofs that are both correct and readable. Whether they will be *conceptual* and *inspiring* are different, more subjective questions, but these qualities are already rare in existing human-authored mathematics.
Eliminating the overhang might not be a bad thing! I have given up on several projects when I learned the answers were *probably* in the literature. If there was an easy way I could extract them from that literature, I would feel a lot better about that! A very natural question about Coxeter groups (do they have spin extensions like in type A? details at https://mathoverflow.net/questions/285263/a-spin-extension-of-a-coxeter-group ) sits unresolved because I find the existing work impenetrable to an extent I'm not sure if it even claims (let alone proves) an answer. Yet I've seen people just assume the result as if it was well-known. Do I want to invest a couple weeks into what would then likely be unpublishable? No, but I would happily invest a hundred tokens and share the answer with the community. (Right now GPT is not good enough for this yet; generally, it struggles with injectivity proofs.)
Thurston is right. It's not about what you contribute to *mathematics*, it's about what you contribute to *humanity*.
We have to take a step back and ask, what does mathematics as a whole contribute to humanity? In academia it's easy to get distracted and only pay attention to what other academics think. But every academic field needs to be useful outside of its own bubble, or else it will dwindle over time as nobody else cares, nobody wants to fund it, and young people don't want to go into it.
The real danger to human mathematicians is not that some AI will prove more theorems than they can. It's that people might stop needing human mathematicians for anything other than satisfying the aesthetics of other human mathematicians. If the physicists stop needing mathematicians because the math AI works better for them. And the computer scientists, and the experts in every other field of science and engineering.
Thank you for this. There are so many thoughts here that I love, but this one is really standing out:
"Problem solving is just a means to an end. The core payout of pure mathematics is the neuroplastic elevation of our worldview, and we can’t get there by copy-pasting the result."
This is a feeling to which any human who enjoys learning can relate, mathematician or not. What if the core payout of living is "neuroplastic elevation of our worldview" instead of "copy-pasting" historical solutions to our problems?
I'll be thinking carefully about how we might define "neuroplastic elevation of our worldview" more precisely. :-D
Thank you for the excellent post! But why adapt a defeatist tone and uncritically accept the claims/rationale of AI companies when we can do the math?
For instance let's look at the results that seem to have initiated the post:
1- Math Inc. basically hijacked an existing formalization effort and brute force vibe coded the reminder of the project, by throwing an unknown amount of MathPhd+GPU hours at it to snatch a PR victory. To cite Math Inc press release, no one seems to bother with papers anymore, the project at that stage only required "six more months of work" and already had "a detailed blueprint and developed an extensive codebase consisting of new definitions and theorems". We have no information whatsoever about the nature of the system (Gauss) that was used, the level of human input or computational resources that went into producing the formalization. And the grand result is an intelligible/useless formalization of a result of which the correctness was never in doubt and whose only function seems to be discouraging people from working on the project...
2- On First Proof, the best performing team from DeepMind, claims to have solved 6 out of 10 lemmas using their Alethia agent. 2 (Problems 9 and 10) of those later turned out to have been solved in literature. And when we look at the paper from Deepmind we see that they ran two versions of their agent based on different base models of which each individually solved at best 4 of the problems. In each round each models submitted 2 candidate solutions which were then evaluated by human experts. Again we know almost nothing about the base model or the specifics of the scaffolding including whether they were modified/fine tuned for the type of problems in First Proof. The same goes for how many attempts/rounds of verification and the computational resources that went into producing the results (All we know that keeping track of it requires a logarithmic scale! (see the original Alethia paper)). And even if we interpret the results in the most charitable way possible, one would only have a ~20% chance of getting a correct solution on a randomly selected problem - assuming that one is willing/capable of checking them in the first place. And if we look at their results on Erdos Problems they managed to "solve" 13 out of 700 problems of which only one (Problem 1051) survived closer scrutiny and even that single “autonomous” result turns out to be hand selected, corrected and formalized by human mathematicians. Frankly I am hard pressed to think of a more absurd way of doing mathematics! - unless one has a well paid job at an AI company of course.
Thanks!
Re defeatism: I don't think my article is defeatist. Elsewhere, I have been blamed for not being defeatist enough. In truth I simply tried to be accurate. The First Proof assessment is that of Litt, who has directly looked at it (I haven't).
Of course there are many more levels to defeatism like Avigad, Hinton and C. Szegedy. But still I am having a hard time reconciling statements like the ones bellow with the actual state of "AI for mathematics" - which has yet to produce a single original proof/significant contribution to mathematics despite the huge resources and talent being poured into it:
"If theorem-proving remains their only official currency, all research mathematicians run the risk of becoming demonetized in the course of the next few years."
"This might be the largest product recall in memory—we sold a bogus idea of math to billions of people, and the bill is coming due."
"These will be difficult years for mathematicians. Students will desert. Money will dry up. Postdocs will ask pressing questions and senior faculty will have to come up with answers. At parties, people will start giving them weird looks, as if they had become living fossils."
I believe that mathematicians will be far better off applying the logical rigor and meticulous scrutiny that is characteristic of their discipline to the claims of AI labs who as you said are "barely engaging with mathematics itself, its core problems and significance" rather than silently retreating into the cloak of metaphysics in the face of fantastical claims of impending “super-human mathematician AI”.
I think you are underestimating the public relation aspect. Even if unjustified by the fundamentals, it creates conditions that are extremely difficult to navigate, individually and collectively, and has many real-life consequences.
I agree the PR situation is impossible especially for mathematicians in academia. And of course the funding situation, especially in the US, makes collaborations with the AI-industry/funding from venture/crypto capital hard to resist (as for instance in the case of Terence Tao and SAIR, Timothy Gower's G-research project or his recent paper/collaboration with OpenAI, Avigad's Center for F. Mathematics just to name a few.) So speaking out against the "Superhuman AI mathematicians" hype in a way that goes beyond mumbling something like "but Mathematics is more than just proving theorems" in the current climate is probably the worst thing one can do for their academic career at least in the short run.
Nevertheless I don't believe this is reason enough to lower our scientific standards to the level where we uncritically accept every claim that comes out of an AI-lab/startup let alone to throw Mathematics under the AGI-hype train. Especially when we have all the reasons to believe that the most likely outcome of this episode will be the AGI fantasies of the tech industry dying on the hills of Mathematics rather than Mathematics dying at the altar of some superhuman oracle. Unfortunately, the damage will already be done either way.
This reminds of one of David Hilbert's lectures where I last saw the Carl Jacobi quote “the object of mathematics is the honor of the human spirit.” you cite :
"Whoever feels the truth of the generous way of thinking and worldview that shines forth from these words of Jacobi's will not fall prey to regressive and fruitless skepticism; such a person will not believe those who today, with a philosophical air and superior tone, prophesy the downfall of culture and content themselves with the Ignorabimus. For the mathematician, there is no Ignorabimus, and, in my opinion, for natural sciences not at all either." [David Hilbert, Naturerkennen und Logik]
I see everything you write compatible with everything I wrote.
This might no be transparent from the "defeatist" passages about the PR debacle, but I hold the seemingly contradictory yet consistent view that our notion of creativity is misconstrued and AI is about to teach us painful lessons (hence my tentative elaboration on the Overhang) AND that AI is about to hit harder roadblocks than the AGI prophets anticipate (hence the "optimistic" conclusion).
Thank you David for a lovely, deep and insightful article. I have several questions/thoughts/reflections. I wanted to spend time weaving them into a coherent whole, but I don't think I can, so I just put them out there. Would love to hear your thoughts if you time.
I'm a computer scientist, who (like many computer scientists) mainly spends their time proving lemmas and theorems. I like to summarize this branch of computer science as the mathematics of Turing machines. I decided to pursue computer science rather than mathematics, which I also deeply love, because of a lifelong fascination with (efficient) mechanical computation. Inevitably, this frames my questions.
1. I notice this trend towards saying (extremely crudely summarized) that the proving is the comparatively easy bit once the definitions and structures are in place. I really don't understand this -- although perhaps it is something that holds true in pure mathematics? I am frequently confronted by statements that turn out to be true but take months or years of effort to prove, whereby the obstacle is not a lack of appropriate definitions or structures, but putting all the pieces together in the correct way, which can require a lot of creativity. It sometimes feels like the "proofs are the comparatively easy bit" thesis is somewhat circular: "proofs are the comparatively easy bit once you have the proof"?
2. Relatedly: I fully understand and endorse the concerns around truth, meaning, canonicalization... the idea that the journey and the lessons learned for yourself and others is at the very least as important as the destination. But sometimes, simply knowing that a statement X is true can be an essential building block for larger truths, even if you don't have a (deep) understanding of why X is true. So can black-box truths, obtained by whatever means, not in themselves be part of larger palaces of mathematical truth? (Of course, later on we might realize that we need to understand WHY X is true, and then we will re-open it, but until then...?)
3. You mention the 1976 proof of the Four Colour Theorem. I find it a deeply beautiful proof, the synthesis of human insight, to reduce an infinite number of cases to finite cases, and mechanical enumeration. But of course, it remains controversial because of the mechanical-enumerative part (despite formalizations in Coq etc). I understand the feeling of uneasiness that this proof generates, and why.
It is of course not an AI-driven proof, but I keep asking myself: what would happen if, rather than 1976, Appel and Haken's proof was published today? How would we respond, given current developments, and what role would we give it in our epistemic discussions? Most provocatively: would it, should it, end up in Mathslop?
Incidentally, on June 21st 2026 it will be exactly 50 years since its announcement. Such a quirk of history, given current developments...
Cheers, Steven Kelk
Thank you Steven! Your questions would probably a full post, especially the first one. Here’s a quick take.
To put the pieces together, you usually need something other than brute force. Even without new definitions, you might rely on a latent pre-conceptualisation. If you’re not seeing this as visible concepts, it might be that your proofs aren’t yet fully canonized, in the sense of becoming a simple chain of trivialities once you’ve made explicit the right conceptual structure (like Grothendieck’s most profound things). Another options is that your domain is intrinsically more computational (see point 3 below), but in my experience this is rarely the case.
Yes, there is some value in knowing things are true even if you don’t understand them. This intermediate status isn’t devoid of value, but it isn’t terminal (unless… see 3 below).
Yes, the four colour theorem would qualify as Mathslop, but there’s a nuance—in all likelihood, it can’t be proved in a non-Mathslop way.
There are theorems whose proofs can’t be conceptualized, because there’s just too much “entropy” (can’t think of a better word) in the result itself. The classification of simple groups, or Hales’s theorem, might belong to the same category. But Viazovska’s results are different, in the sense that we know that the proof can be made much more conceptual (which is remarkable, since she solved in dim 8 and 24 the same problem Hales solved in dim 3 with a structurally Mathslop proof). So it’s much more frustrating to be happy with a Mathslop autoformalization of her results.
Entropy is a good term, or https://en.wikipedia.org/wiki/Kolmogorov_complexity
Hi Steven, I think framing the topics here around computation is indeed very interesting.
Basically David suggests that there are valuable bits in math which, even after the formal computation runs, are not yet fully "captured". I think this observation has impact even beyond the "human side" of math (community, careers, education, etc); it is a real "computer-science" truth since, when humans have a clear mental picture of something, they form some kind of "compression" of the huge chunk of "verify this, verify that" MathSlop, and we know that compression is intelligence.
So the question is, once machines "compute" a proof in, eg, Lean, can they compress it?
This reminds me of another point: AI models can interact with language servers at a speed faster than any human, but they currently lack the ability to, say, "fork" a language altogether and implement language traits suitable for specific challenges. AI can write rust better than me, but we cannot count on AI to come up with the next rust for now.
That brings me to a crude comparison: mathematicians each have their own fork of "mathlang", where the same math definition, while seemingly identical in the "official math" sense, can differ wildly in the secret math sense. This makes understanding math difficult since we see someone call an API we know but still cannot understand what they're doing, for there is a secret documentation of this API living in the brain of that mathematician... I"ll stop this slop now... haha...
You're right to say that these conceptual mistakes aren't particular to mathematics. When you follow the reasoning of people like Hinton, though no one dares put it this way, they also think that great tranches of the physical sciences are a closed system - sure, experiments are important for 'empirical confirmation', the story goes, but in ideal terms, no interaction with the world is necessary.
This is a belief in the Triumph of Theory: our ability to brute force an understanding of the world by devising the right combination of sentences and equations to describe it, all of which is already latent in folk descriptions. In the end, they'd have you believe that you can take a large enough model that hasn't read any physics, say to it "did you know that apples fall from trees?" and it'll come up with Newton's laws.
This is part of an ancient delusion which has overlooked the real sources of human creativity, first because it cannot understand them and second because it fears the realisation that they exist outside of language. We feel that language is what gives us control; to place our prowess outside of it is almost to take away our freedom.
The particular situation of mathematics is therefore symptomatic of a deeper failure of human self-understanding. In naively optimistic moods, I hope that - though the road will be rough - the eventual failure of AI to capture creative mathematics will be impetus for a widespread re-examination of what we think we are. But realistically, we're going to be told that we didn't buy enough GPUs and that we didn't use the tools in the way we were supposed to. The role of intuition will only be accepted when it can be built and sold.
I find it amazing how you manage to hit all the interesting aspects of AI for math in your exciting article, but come away with basically the opposite conclusions than me for many of them.
I think your belief that neuroplasticism provides a better foundation than platonism to explain mathematical activity has something to do with it :-)
In particular, I don't think that developing the right concepts for difficult theorems is something that is particular to us humans. I think anyone, even AI, will have to come up with the right concepts and definitions in order to prove difficult theorems. The Math inc scoop was not about scooping the fields medal winner. It was about scooping people who formalised concepts in Lean that had already been conceived before, in order to prove the theorem. If mathlib poses conceptual challenges beyond the concepts in the published proof, well, I think that is due to mathlib and type theory.
So proving difficult theorems will remain an important measure, and yield important insights, as before. If an AI proves the Riemann hypothesis first, it will *undoubtedly* also introduce the necessary concepts to do so. There are already many mathematicians much more powerful than me in proving theorems; if I can use an AI to prove the theorems I need in my application, splendid.
And I think that is what will make mathematics more important and embedded in our culture and work life than ever: It is the correct way to think about many problems, and that doesn't change with AI. What AI will give us is that once you manage to think in math, solving the problems you think about will suddenly become much easier.
I never said concept building was specific to human. I simply noted that current systems, while obviously built around a latent concept architecture, are extremely poor at canonization.
I am not sure that is entirely true. Maybe canonization with respect to mathlib, but people like Peter Scholze refused in the past to interact directly with Lean for a reason. Maybe the AI shares that sentiment. Math is already pretty canonical, why can we not just use this existing structure for the prover? I've seen good results telling the AI to first think informally and conceptually through a proof, then sketch the proof formally, then complete the full formal proof, building any needed proof tools in the process, when the formal language is closely aligned with the informal one. They don't seem to be able yet to invent new concepts, but are pretty good at discovering and reusing existing concepts (the Overhang). In case of the Math inc scoop, that 200K blob was probably just the easiest and messiest formal proof they could rush out *based on an existing informal proof*. If tasked with formalising something entirely new, I don't think that messiness would necessarily pay off (depending on how large the ocean is, of course).
The future belongs to Brouwer.
Why cannot explicability (including explicability of theorems proved by AI) be something that math's master or phd students can get credit for in their studies? Seems like a great learning experience and an opportunity to contribute.
It will come, out of necessity. The price to pay is a substantial decrease in perceived objectivity.
Why is that the price?
This is really, really good. And some thoughtful comments here that echo some of what I want to say.
I’m not a mathematician, but I did study the foundations of mathematics and logic in grad school. To this day, I think Wittgenstein remains the best guide here. He would reject both the platonism and the psychologism you describe. Neuroscience has nothing to offer us here, please don’t be misled by that. But math isn’t metaphysically mysterious either. Adding, following a rule, stating assumptions — these are things we do. They’re part of our form of life. Not “merely” so; Wittgenstein’s quietism consists in the rejection of both platonism and psychologism as genuinely intelligible philosophical views. The question they thought they were trying to answer is supposed to dissolve when you’ve done the work of philosophical therapy.
One of the reasons I’m skeptical that LLMs will contribute much to math in the devastating ways you describe is because the intelligibility scaffolding that supports proof-work is just so deeply enmeshed in our other social practices that it’s hard to imagine an LLM getting it without being, well, enmeshed in our social practices.
It’s common in cogsci and AI research to think of intelligence as a natural kind, g, that organisms have more or less of. But in biology this view has fallen out of fashion — most accept that intelligence isn’t one thing, but a way of describing different responsive practices to widely varied ecological niches. Which says nothing about the epistemic status of math or logic!
If mathematicians fetishized the proof over the “shadow math” of scaffolding and canonization, it was probably because they were uncomfortable with the epistemic status of that work. LLMs will hopefully force a reckoning where they actually realize these practices weren’t epistemically precarious at all — so they can re-value that work to shift the professional incentives you describe. Public defensibility is another story.
Excellent articulation of the threat AI poses to the current dynamic of mathematics….it will be interesting to see what all can be achieved if we embrace the technology, rather than oppose it out of fear of displacement
Here's something more like autocannonization https://arxiv.org/pdf/2603.20396
This was an incredibly insightful article. I really enjoyed reading it. However, I still think this is
somewhat of a retreat in that one is abandoning a central aspect of why one does mathematics. This aspect is the allure of and thirst for discovery. A characteristic embodied by Grothendieck and his school (mentioned in the embedded image).
Assuming that AI does outpace humans in sheer mathematical capability, is there a place left for human discovery in pure mathematics? Under this assumption, the human practice of doing mathematics will be restricted to the lecture hall or classroom. The extent of discovery for the mathematician will be limited to deciphering a proof given by AI. The days where mathematicians will explore the beautiful and mysterious realm of mathematics will be finished. The role of discovery will be overtaken by AI, which will discover and then "report" back to the human. Note, even this can be considered optimistic since why couldn't an AI explain a complex proof to a human being better than any other human could? Hence, the role of the mathematician, it seems, would be solely restricted to a student in a classroom.
The importance of the “right” definition, I believe, raises a fundamental obstruction for AI in ever achieving capabilities of mathematical discovery similar to that of humans. However, if we assume AI discovered a valid proof of the Riemann Hypothesis, I think AI would have already overcome this obstacle. Hence, it seems it would be a hindrance for mathematical discovery if humans were creating the definitions but not finding the theorems.
I agree that human understanding is a fundamental reason why one does mathematics. However, I think that the thirst for discovery is another just as crucial aspect. I would love to hear your thoughts. I hope I am making sense.