This posting is mainly intended to provide some links to material about AI in math and physics that I’ve found interesting. I confess that to a large degree I’m trying to avoid seriously learning about exactly what is going on, so my own opinions and thoughts about this topic aren’t grounded in any expertise. If you have interesting things about this topic to point to in the comments, please do so, but for general discussion, try some other venue managed by someone better informed.
- A Future of Mathematics event just started a few minutes ago at Stanford. You’ll find a link to the livestream there and talks should be on Youtube.
- You can easily find people announcing that AI is about to make mathematicians obsolete. We’ll see. In the meantime what I’ve found interesting is that AI is motivating deeper thinking about what what it is that mathematicians really do, and how to protect the valuable parts of this. For good examples of this, see the substacks of Michael Harris and David Bessis. I especially like this recent posting. Also, it was from Michael Harris I learned that Peter Scholze has publicly expressed the opinion that
I already consider the influence of AI to be strongly negative, for humanity, for democracy, and for the planet.
- One of the main problems with AI agents in general is that they are better at saying things that are convincing than they are at saying things that are true. Their potential application in mathematics has the big advantage over other fields that one can use these agents together with formalization and proof-verification to deal with this problem. Scholze has been involved in a major effort using proof verification and I don’t think his remarks about AI apply to this. For a very interesting recent interview with him, see here, which includes some comments about why he hasn’t found formalization that useful.
Something useful that may come out of this is a conclusive demonstration that there’s a gap in the Mochizuki abc proof. There’s a project working on formalizing this proof announced here. From what I can tell, the situation so far is that the very few who think Mochizuki has a proof have been unable to explain to anyone else how the proof is supposed to work at the point where Scholze/Stix pointed to a gap, and this includes the people charged with trying to formalize this part of the proof.
- In fundamental theoretical physics, formalization is generally not relevant (except perhaps in some areas that could be described as mathematical physics). Given the fact that the subject has been stuck for a long time, with a lot of research devoted to ever-more irrelevant calculations, it seems clear that AI agents likely will soon be able to do this better than humans. For an example of what I mean, see here.
There is a huge amount of money being thrown in this direction. As an example, the DOE is promoting a Genesis Mission. I’ve no idea how fruitful this will be for most of its goals, but the one relevant to fundamental theoretical physics is “Unifying Physics from Quarks to the Cosmos”. The idea is that
An AI that internalizes the Standard Model could accelerate analysis by orders of magnitude, identify anomalies pointing to new physics, and propose theoretical extensions consistent with all data—a leap from pattern matching to physics reasoning.
which doesn’t look at all promising.
Jared Kaplan tells us here that in 2-3 years AI agents will be replacing the best of IAS theorists. Seems unlikely to me, but we’ll see soon…
Update: Some interesting discussion of this on X (kind of weird to see this in the middle of the intellectual sewer X now is…). See this by Jacob Tsimerman, this by Daniel Litt
Update: Timothy Gowers reports on his latest experience with an AI agent and implications for mathematics research. A team at Google DeepMind has produced an “AI Co-Mathematician“.
Small note, the Kaplan in question is Jared (the co-founder of Anthropic), rather than either of the David Kaplan(s) who are still in the field.
*Jared Kaplan, not one of the many Davids in particle physics.
Thanks! Fixed.
I recommend this interview with Terence Tao on the Dwarkesh podcast: https://www.dwarkesh.com/p/terence-tao
He says that AI is already having a dramatic impact on mathematics, for example some immediate success with many of the unsolved Erdos problems, but to go further we will need to change the way we think about science:
“It’s great that we can generate all kinds of things now with AI, but it means that the rest of the aspects of science have to catch up: verification, validation, and assessing what ideas actually move the subject forward and which ones are dead ends or red herrings. That’s not something we know how to do at scale. For each individual paper, we can have a debate among scientists and get to a consensus in a few years. But when we’re generating a thousand of these every day, this doesn’t work.”
And
“They excel at breadth, and humans excel at depth, human experts at least. I think they’re very complementary. But our current way of doing math and science is focused on depth because that’s where human expertise is, because humans can’t do breadth. We have to redesign the way we do science to take full advantage of this breadth capability that we now have.”
You may have seen this, or not?
https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems
I very much agree with this: “One of the main problems with AI agents in general is that they are better at saying things that are convincing than they are at saying things that are true.” However, I have been using these tools extensively for relatively straightforward It\^o calculus topics for several years, and they have improved considerably. They are getting pretty good at representing the status quo on topics that are relatively well established.
One potential upside, peer-review / validation of technical papers, appears to be a huge bottleneck right now–which AI is currently making worse, however, I think the better tools e.g, GPT 5.x and Claude are approaching the capability of providing a curation function at a first pass level. They could provide a score, perhaps similar to Sabine’s bullshit meter, that would enable people to focus on the most promising papers. This approach would naturally support some back and forth with the “reviewer” on a preprint server like SSRN or arXiv that would enable authors to comment on the automated review.
Bryan,
Tao has become somewhat the public face of the math research community on this issue. I haven’t read most of what he has been saying. One thing I did find interesting is his recent posts on mathstodon, see for instance:
https://mathstodon.xyz/@tao/116450581967483825
There he describes the problem-solving aspect of math research as generating a proof, verifying it, then trying to “digest” it, understand what new ideas are there that can be used elsewhere. AI is getting very good at the first two aspects, but what about the third (which is arguably the most important?).
There’s an interesting contrast with what someone like Scholze is doing, which is not problem solving, but coming up with a new and more insightful framework. Proofs and verifications of theorems are of secondary importance, more as checks that you’ve found the right thing. Ideally, a la Grothendieck, if you have the right point of view, the proof of the theorem is obvious, you don’t need AI to verify it for you (see his metaphor about opening nuts).
Harald,
Yes, AI and the Erdos problems have gotten a lot of attention and I’ve seen some of it. This is though exactly the kind of thing that is going on where I’m the wrong person to discuss it, because:
1. I know little about and am not interested in that kind of mathematics or in that kind of problem solving.
2. When I look at the claims being made and the press coverage, I recognize something I’m very familiar with: a large component of hype. From experience I know very well that engaging with a heavily hyped area is a huge sink of time, since you need to become expert enough to figure out what is really going on. But, in this case, see point 1.
At the “Future of Mathematics” event, a quite interesting talk by Terry Tao, just finished, you should be able to find it here
https://www.youtube.com/watch?v=tN4hsT5t0nw
He describes the problem now facing the math community as “proof indigestion”.
Regarding Mochizuki, see also here
https://youtu.be/H4n1XIa2flI?si=cw4-tvmqGoQ5mt4R
Here’s an AI formatted text version of Terence Tao’s part
https://rentry.co/kauuk4dw
His thoughts on problems with AI generated maths seem intuitively similar to what I think software engineering is going through. Understanding the issues becomes the bottleneck. The peer review bottleneck is essentially the same as with code review. His answer to a question on using AI to aid understanding is more negative than I would have thought though.
There was a fascinating exchange on X between Daniel Litt and Jacob Tsimerman regarding motivations for doing math, possible implications of growing AI impact on math etc. I would link it, but its easily found, and took place over multiple threads.
Mikey,
I already added some links to that as an update of the main posting, see there.
I like this tough by Daniel Litt on X (your link) : ”I think you start getting back answers, and then to continue, you have to UNDERSTAND them. And the dirty little secret of mathematics is that it’s impossible to understand what anyone else is saying. Conveying one’s mathematical intuition is incredibly hard: at least for me, the experience of acquiring understanding from someone else’s work is nearly identical to that of discovering it on my own.”
Savoureux !
Have you read Terry Tao’s paper on this topic?
https://arxiv.org/abs/2603.26524
The Genesis mission is a change in the way basic nuclear research is funded (switching to an SBIR phased model), in the recipients of that funding (private companies are expected to be direct recipients, along with smaller institutions), and the goals of that research (to use AI). Experimental groups are preparing to be hard hit due to nature of this program as a reallocation. I can add to Jared’s prediction that AI agents will replace theory a prediction that AI may also replace experiment, but not in the sense of the word replace that implies substitution.
Re Mochizuki there must be some backstory that hasn’t been made public. Attention to IUT has died down considerably in comparison with past years; the few sources I’ve seen discussing this latest formalization effort discuss either the LANA Project announcement (Peter’s link) or Mochizuki’s latest document (‘On the formalization of IUT…’) and the associated YouTube talk (Thomas’s link in the comments), or they conflate the two. The only source pointing out that these are actually two separate formalization efforts seems to be ‘A Glimpse of Resolution: Computer Formalization Targets Decades-Old Mathematical Dispute’. I don’t recognize either the author, Julian Thorne, or the site, Bode living, but the article seems like real journalism.
At any rate, this interpretation appears to check out. The LANA Project authors (Kato, Commelin, Topaz, Kedlaya, Hoshi) are different from the coauthors Mochizuki lists (Hoshi, Yamashita, Yang). Only Yuichiro Hoshi is common to the two lists. The timelines are also different: the LANA project is said to have been conceived in late 2023 and to have got started in earnest in late 2024, while Mochizuki says his group’s effort started in late 2025.
It is interesting to compare Hoshi’s comments in the LANA project announcement with what Mochizuki is saying. Hoshi’s comments:
“At the same time, however, I also believe, regrettably, that I have not yet fully fulfilled my role. In particular, with regard to the logic by which Corollary 3.12 is derived from Theorem 3.11 as I mentioned earlier, I must take seriously the fact that many members of the LANA Project still feel that there is some insurmountable wall there. Then I also keenly feel my own shortcomings in the face of such a situation.
“Nevertheless, I do not think at all that the efforts we have made over the past year and more have been meaningless. On the contrary, I think that precisely because we have thought so seriously, discussed so extensively, and tried so hard to understand matters up to this point, it has become far clearer than before where the true difficulty really lies. In that sense as well, I believe that the efforts we have made on this project have definite value and significance. ”
Thorne’s article states that Mochizuki sees the role of Lean formalization to be communication, that is, to convey the “simple logic” of the proof to outsiders who have so far failed to grasp it for sociological reasons, and not, as one might think, to prove correctness (which Mochizuki takes for granted). In the talk Mochizuki advertises a new Theorem 3.11.5, intermediate between Theorem 3.11 and Corollary 3.12 and “70 lines” of “skeletal Lean code”, which, while not yet publicly released, have, according to the abstract of the talk, “constituted a remarkably successful case of the use of Lean as a communication tool.” Communication to whom, one wonders…
It seems possible that the Mochizuki group’s work is a reaction to the obstacle the LANA Project ran into in trying to formalize the proof of Corollary 3.12, but Mochizuki doesn’t say this. In fact he makes no reference to the LANA Project in his writeup or talk, as far as I can tell. The LANA Project says there will be a press conference on July 17 in which they will give a progress report, so perhaps we will soon find out.
I am sure you have seen Timothy Gowers’ recent blog post. I am not a pure mathematician, but every academic in the mathematical sciences needs to understand the very serious existential threat we face. Undergraduate students have mostly already given up on learning. Graduate students (sometimes) still see the value in learning how to do things that ChatGPT can easily do. What will happen when it becomes clear that any research contribution that they can hope to make as a junior researcher can also easily be done by AI? There has been a lot of great discussion about where the real value of mathematics lies, how humans can best contribute in the future, and how the role of professionally trained mathematicians will have to evolve. However, unless the academic community can very quickly figure out how to offer young scientists a viable career path amid such rapid and far-reaching disruption, the human mathematical community will be on the path towards extinction. I am sure there are many people who think there is nothing wrong with that, but every other community that is based on human creativity will face similar existential threats. I am not excited about living in such a world.
Failed mathematician working as a statistician,
I very much share your concerns. For those who haven’t seen it the Gowers blog post is here, and it raises several important issues.
https://gowers.wordpress.com/2026/05/08/a-recent-experience-with-chatgpt-5-5-pro/
“A team at Google DeepMind has produced an “AI Co-Mathematician“.”
I thought a co-mathematician was a machine for turning theorems into coffee.
A mathematician is a machine for turning coffee into theorems. A co-mathematician is a device for turning cotheorems into ffee.
Isn’t it a bit iffy what happened here? The initial work was done by an undergraduate during an REU project. While I don’t know what went on during that project, it’s not unreasonable to assume that there was a lot of input from the project advisor. A great advisor would have selected a good problem and left a lot of meat on that bone for the student to start a career based on it. Reading the links, this seems to be the case – cited specialists in the filed considered the final results good enough to be part of a PhD thesis. That piece of meat is now cleaned to the bone. I guess it used to be that professors would steer clear from the work of junior colleagues, specially work of REU students, to give them a chance.