Mathematics is like this. You read the first symbol in the paper, it is a wiggly triangle, what does that mean? Well you will find out that symbol means the Constant or Operator or Set or Function belonging to So-and-So with the unfortunate name. Well now you know it is called Grossediche’s Member, what does that mean? You will find out it is defined in these dozen lines in Grossediche’s seminal paper, you will need to read the entire paper to make sense of these dozen lines, you will need to read everything he published in this particular decade to make sense of the paper. Each of the dozen lines is jam packed with other symbols, for each of those you will have to repeat this entire process, with another stack of papers, from another unfortunately named mathematician. Now you have a firm grasp on Grossediche’s Member, you return to the original paper. You read the second symbol in the paper, it is a half-melted letter t, what does that mean? Well, …
Behind each symbol is a whole paper, behind each paper is a whole life’s work, and so on. With this in mind, it is perhaps not so surprising that language models operating on embeddings are extraordinarily well-suited to this particular task.
LLMs don't understand things as human mathematicians do, even though they are very good at finding analogies and similarities. Their advantage is a larger search space (experience) and search speed, not better understanding.
I gestured at it with “embeddings” but to spell it out, I’m more or less claiming that the only sense in which LLMs “understand” a given thing is as big list of all the things it is related to (implemented in the form of a vector embedding). And all those things it is related to, each one of those things is just a big list of yet more things it is related to, and so on. I do not mean that it is eventually hitting a “base case” that contains semantic meaning and then transforming it according to the relationship path it took to get there; rather, I mean that it follows enough n-th order relationship links that the shape of the relationship to the future thing (i.e. what it is generating) is constrained enough to pick output tokens on the basis of their relationship to the current token alone.
As an analogy: if I give you a stream of numbers and you notice that the delta between number n and number n+1 is always 2, you now know enough about the relationships between the numbers in the stream to pick the next number without ever knowing what the numbers were.
While so many are complaining about AI on HN, an absolute master of his field is using it without any self-doubt or negativity. Just getting stuff done better and faster while remaining at the top.
> While tribe fear hot whispering rock, Wise number shaman wield it. Make cave painting faster, better. No fear. Shaman top mammoth hunter, king hill.
Other tribe not hate whispering rock. Tribe hate rock salesman saying it solve every problem.
Thinking rock make many wrong marks! Shaman must check every mark himself! Whispering rock speak with big confidence even when wrong. Dangerous rock! Who clean mess? Shaman!
Soon shaman forget how to hunt! Today rock help shaman. Tomorrow chief say no need shaman. Me worry.
In a recent talk (https://news.ycombinator.com/item?id=49056620), Terence Tao plainly says that AI generating and verifying proofs is only part of the picture. The process of making the proof usable/readable and then canonicalizing them so they can form a foundation for math built on that proof is the other half of the picture and those things are something that can only be done by human minds.
The second part can only be done by human minds... For now. Just like the first part could only be done by human minds until a few years (or decades) ago.
I'm not in the habit of counting my chickens before they've hatched and neither should anyone else. There are plenty of technologies, like fusion power, where supposedly another breakthrough or two is just around the corner that will make them viable but never comes.
He is knee deep in the AI money. This submission is him desperately trying to simplify a spaghetti AI proof (i.e., menial work) to show that AI works. He didn't discover anything new.
I find his submission very valuable. It is not only digestible for humans but also summarizes the proof, explains what humans were missing, and highlights the methods that could help with stronger and similar conjectures (see his comments to the post).
I don’t see enough people here expressing awareness of the deep societal revolution that is about to unfold. I’m grateful to Terence Tao for doing his best in this strange time to discover how human mathematics can adapt, but I’m not sure why you think this means he’s some uncritical user of AI. And he’s definitely not so shallow as being primarily motivated by staying at “the top”. That’s just silly.
Tao:
“There will be some places where we should use AI, but we should take initiative and decide what those are,” he said. “We set the rules on what’s acceptable or not, and we should not let external actors define those for us.”
The impact on the psyche on some Mathematicians of this AI progress must be pretty brutal. To me, it breaks the mystique of Mathematics a lot.
You still need a lot of skill to digest and understand the proofs, but "this is the worse it will ever be." I'd imagine part of the motivation of a large set of mathematicians is to be the "first" or to crack the nut that others couldn't. If Mathematics becomes working with an AI to get a Lean certificate, and then essentially reverse engineering that into something digestible, then it's fundamentally a different pursuit.
Software Engineering feels a little less impacted? Though if you identify with loving coding, then perhaps similarly? I've always liked the outcome of what writing code can do, and enjoyed the craft hand coding for the past ~30 years. But I haven't once ever missed writing code by hand since Opus 4.6, I couldn't go back.
My motivation to do mathematics is some combination of wanting to understand the system of mathematics deeply and enjoying the craft and puzzle of working on research problems. If I never had to publish again and the computer was 1000x better than me, so that I can live on my 20k a year UBI, then I’m fine with that. The anxiety is that this isn’t realistic at all so I’ll likely have to spend my life doing something different than pondering math now.
Software Engineering feels a little less impacted?
I don't think so - software engineering has already been completely up-ended; we are showing mathematicians what is next for them.
Sure though wrt your point about mystique there is a difference in psychological importance and cultural meaning - maths at the highest level is far more intellectually challenging and even "glamorous" and represents one of the peaks of human achievement. Ironically though if we allow the invention of AI belongs to our (software engineering) field, this is the first time we've matched those peaks.
I agree with you on not missing manual coding, which in some way surprises me - but it's been a long time since I had the passion of my youth for it.
I am a mathematician and I never believed in this kind of mystique (maybe in other, more resilient mystiques).
I have always expected machines will be able to do math. Since late 2018, I expected them to be able to do math long before physical stuff (basically Moravec paradox).
it does not in any way break the mystique of mathematics for me, though that mystique continues to attach to proofs that are in some way beautiful or elegant, whether produced by humans or machines.
as for software engineering, I've definitely used claude to help with both complex problems that I could have worked through myself but with greater expenditure of time and effort, and with problems that I would not have been able to do without spending a lot of time learning my way around a whole new domain, but in both cases what I am most keenly aware of is that I am benefitting from some human (or many humans) having solved this problem before.
I am ABD in mathematics. That was a long time ago. I taught math for many years at a community college. My amateurish but knowledgeable perspective is that these developments shatter the mystique for me.
What AI is showing is that mathematics is mostly just pattern searching and AI can do this far better, faster, and with a much wider base than humans can. When I was working on my thesis problem I realized that I worked much less than my fellow students. I was an average student in my program but even for the best students they had to spend a lot of time thinking about stuff. They put in a lot of effort.
Is the difference between me and Tao mostly effort and that he has a much better memory of mathematical facts than me?
This is only the "problem solving" side of mathematics. Completely missing the theory builders who have completely reshaped the world of mathematics (and far beyond). AI is a long way from matching original thinkers of the calibre of Euclid, Al-Khwarizmi, Newton, Leibniz, Euler, Galois, Riemann, Cantor, Hilbert, and Grothendieck. Or Turing, Gödel and Von Neumann?
I lean more towards the "proofs from the book" mindset - if there's a really beautiful proof of some theorem out there I would be happy to see it no matter whether it was discovered by a human or a computer, and conversely if a computer has churned through a search space and generated a clunky proof in 100000 lines of lean code that just means that people trying to find a nice proof can do so with the assurance that the theorem is true. note that mathematicians didn't give up on trying to find a better proof of the four colour theorem once a clunky computer assisted proof showed the theorem was true.
The question is, will universities continue to fund graduate programs to the extent they currently do so that people can find elegant proofs of AI derived theorems? I’m skeptical. A lot of good mathematicians tried to prove or disprove the Jacobian Conjecture and AI did easily. The value added by human mathematicians seems to be low return on the investment.
Just like in chess, at some point the problem at hand and its solution becomes so unwieldidly complex that you either make of it the work of your life or you use a math/chess engine to handle the complex stuff.
Just like you can find a forced mate in 120 moves for a given position, you can find a 120 pages of pure gibberish demonstration of some conjecture with its lean check.
The thing is to not become reliant on it and just cheer it up so it makes progress on its own in the Riemann hypothesis, but to use it like a lever to lift heavier stuff, as Dr. Tao does here.
I saw an interesting article in the Atlantic[^1] somewhat recently predicting that the people who will thrive in the AI age will be ones who enjoy mental effort. That is, even when AI could do something for them, these people will choose to do it themselves if there’s something to be learned from it.
This post seems to illustrate the point perfectly to me. AI wrote the proof. It was done, Lean checked it. And presented with that, Tao’s reaction is still to want to learn something—how to solve the problem himself—and then to meticulously untangle a 90k-line machine proof (utterly disregarding that there’s no clear upside for doing so—he can’t get a paper out of this) because it’s the only way to learn that. My bet is that it was worth it.
(I also think everyone saying “it doesn’t make sense to write code anymore” is crazy. The best learning tool of all time was just invented, and you want me to not use it? What the point of any of us if not to know things?)
Making things understandable is part of intelligence as much as producing the initial artifact is. Even if the proof checks out in Lean (or the code runs and passes QA) if it's a mess, it will be hard to use it to do anything further.
This does not only matter doing cutting-edge mathematics. This, about the 'digested' version versus the original, should feel familiar to some folks here:
> This formalization is more streamlined than the original formalization (it has about 15,000 lines of code, compared with around 90,000 for the original proof).
and if you've ever tried to turn an overly vibed piece of code into something that makes sense:
> it has taken me several days (with heavy AI assistance) to perform such a digestion, to place the proof in proper context with previous literature and to simplify and streamline the argument to highlight the main ideas
If you see something that is confusing or overly clever, please don't assume it must be for some good reason you don't understand and move on--ask questions, get it simplified, try to get it worked out. Future you will appreciate it.
Dude then proceeds to dump about 16 A4 pages worth of heavy-duty algebra which 99.999% of the humans on the surface of this planet are completely unable to read past the first two lines.
LOL, I guess language is a "remarkably" vague tool, where "elementary" means vastly different things to different people.
That doesn't diminish the achievement of course, but ... please, easy on the "remarkably elementary" next time, that's borderline insulting.
It's a habit of the community. Tao actually elaborates on what he means by this in the same paragraph.
I'd like to offer a charitable interpretation. By Tao labelling it as "remarkably elementary", he encourages less experienced mathematicians (including students) to go and read the proof for themselves. He's advertising a low barrier to entry for certain parts of his audience. This isn't always the case with whatever he reports on, so it's worth pointing out when it's true.
“Remarkably elementary” in mathematics means accessible to people who have finished the first 1-3 years of grad school where you go through the canonical entry level courses in research level mathematics. There’s no reason to think Terence’s blog is aimed at a general audience.
Mathematics is like this. You read the first symbol in the paper, it is a wiggly triangle, what does that mean? Well you will find out that symbol means the Constant or Operator or Set or Function belonging to So-and-So with the unfortunate name. Well now you know it is called Grossediche’s Member, what does that mean? You will find out it is defined in these dozen lines in Grossediche’s seminal paper, you will need to read the entire paper to make sense of these dozen lines, you will need to read everything he published in this particular decade to make sense of the paper. Each of the dozen lines is jam packed with other symbols, for each of those you will have to repeat this entire process, with another stack of papers, from another unfortunately named mathematician. Now you have a firm grasp on Grossediche’s Member, you return to the original paper. You read the second symbol in the paper, it is a half-melted letter t, what does that mean? Well, …
Behind each symbol is a whole paper, behind each paper is a whole life’s work, and so on. With this in mind, it is perhaps not so surprising that language models operating on embeddings are extraordinarily well-suited to this particular task.
That is research math.
If you read an introductory book (like Algebra: Chapter 0 by Aluffi, yeah the choice is a bit naughty), it doesn't assume (too many) prerequisites.
And after you've read enough of these (e.g. when you have a BSc in math), research papers are more accessible.
LLMs don't understand things as human mathematicians do, even though they are very good at finding analogies and similarities. Their advantage is a larger search space (experience) and search speed, not better understanding.
I gestured at it with “embeddings” but to spell it out, I’m more or less claiming that the only sense in which LLMs “understand” a given thing is as big list of all the things it is related to (implemented in the form of a vector embedding). And all those things it is related to, each one of those things is just a big list of yet more things it is related to, and so on. I do not mean that it is eventually hitting a “base case” that contains semantic meaning and then transforming it according to the relationship path it took to get there; rather, I mean that it follows enough n-th order relationship links that the shape of the relationship to the future thing (i.e. what it is generating) is constrained enough to pick output tokens on the basis of their relationship to the current token alone.
As an analogy: if I give you a stream of numbers and you notice that the delta between number n and number n+1 is always 2, you now know enough about the relationships between the numbers in the stream to pick the next number without ever knowing what the numbers were.
> LLMs don't understand things as human mathematicians do
You say it like it's a bad thing!
[dead]
While so many are complaining about AI on HN, an absolute master of his field is using it without any self-doubt or negativity. Just getting stuff done better and faster while remaining at the top.
> While tribe fear hot whispering rock, Wise number shaman wield it. Make cave painting faster, better. No fear. Shaman top mammoth hunter, king hill.
Other tribe not hate whispering rock. Tribe hate rock salesman saying it solve every problem. Thinking rock make many wrong marks! Shaman must check every mark himself! Whispering rock speak with big confidence even when wrong. Dangerous rock! Who clean mess? Shaman! Soon shaman forget how to hunt! Today rock help shaman. Tomorrow chief say no need shaman. Me worry.
> Thinking rock make many wrong marks
So do humans. Don't Lean proofs take care of that?
Also, whispering rock owned by big tribe far away. Big tribe can take away whispering rock.
In a recent talk (https://news.ycombinator.com/item?id=49056620), Terence Tao plainly says that AI generating and verifying proofs is only part of the picture. The process of making the proof usable/readable and then canonicalizing them so they can form a foundation for math built on that proof is the other half of the picture and those things are something that can only be done by human minds.
The second part can only be done by human minds... For now. Just like the first part could only be done by human minds until a few years (or decades) ago.
I'm not in the habit of counting my chickens before they've hatched and neither should anyone else. There are plenty of technologies, like fusion power, where supposedly another breakthrough or two is just around the corner that will make them viable but never comes.
Tao is on the advisory board for the AI for math fund:
https://terrytao.wordpress.com/2024/12/05/ai-for-math-fund/
He is leading another AI foundation:
https://sair.foundation/
He is partnering with the commercial startup math.inc (funny name, isn't it?):
https://www.math.inc/a-conversation-with-terry-tao
He is knee deep in the AI money. This submission is him desperately trying to simplify a spaghetti AI proof (i.e., menial work) to show that AI works. He didn't discover anything new.
I find his submission very valuable. It is not only digestible for humans but also summarizes the proof, explains what humans were missing, and highlights the methods that could help with stronger and similar conjectures (see his comments to the post).
I don’t see enough people here expressing awareness of the deep societal revolution that is about to unfold. I’m grateful to Terence Tao for doing his best in this strange time to discover how human mathematics can adapt, but I’m not sure why you think this means he’s some uncritical user of AI. And he’s definitely not so shallow as being primarily motivated by staying at “the top”. That’s just silly.
Tao: “There will be some places where we should use AI, but we should take initiative and decide what those are,” he said. “We set the rules on what’s acceptable or not, and we should not let external actors define those for us.”
https://www.simonsfoundation.org/2026/08/13/fields-medalist-...
> while remaining at the top.
isn't the linked post precisely an example of the opposite?
The impact on the psyche on some Mathematicians of this AI progress must be pretty brutal. To me, it breaks the mystique of Mathematics a lot.
You still need a lot of skill to digest and understand the proofs, but "this is the worse it will ever be." I'd imagine part of the motivation of a large set of mathematicians is to be the "first" or to crack the nut that others couldn't. If Mathematics becomes working with an AI to get a Lean certificate, and then essentially reverse engineering that into something digestible, then it's fundamentally a different pursuit.
Software Engineering feels a little less impacted? Though if you identify with loving coding, then perhaps similarly? I've always liked the outcome of what writing code can do, and enjoyed the craft hand coding for the past ~30 years. But I haven't once ever missed writing code by hand since Opus 4.6, I couldn't go back.
My motivation to do mathematics is some combination of wanting to understand the system of mathematics deeply and enjoying the craft and puzzle of working on research problems. If I never had to publish again and the computer was 1000x better than me, so that I can live on my 20k a year UBI, then I’m fine with that. The anxiety is that this isn’t realistic at all so I’ll likely have to spend my life doing something different than pondering math now.
Software Engineering feels a little less impacted?
I don't think so - software engineering has already been completely up-ended; we are showing mathematicians what is next for them.
Sure though wrt your point about mystique there is a difference in psychological importance and cultural meaning - maths at the highest level is far more intellectually challenging and even "glamorous" and represents one of the peaks of human achievement. Ironically though if we allow the invention of AI belongs to our (software engineering) field, this is the first time we've matched those peaks.
I agree with you on not missing manual coding, which in some way surprises me - but it's been a long time since I had the passion of my youth for it.
I am a mathematician and I never believed in this kind of mystique (maybe in other, more resilient mystiques).
I have always expected machines will be able to do math. Since late 2018, I expected them to be able to do math long before physical stuff (basically Moravec paradox).
it does not in any way break the mystique of mathematics for me, though that mystique continues to attach to proofs that are in some way beautiful or elegant, whether produced by humans or machines.
as for software engineering, I've definitely used claude to help with both complex problems that I could have worked through myself but with greater expenditure of time and effort, and with problems that I would not have been able to do without spending a lot of time learning my way around a whole new domain, but in both cases what I am most keenly aware of is that I am benefitting from some human (or many humans) having solved this problem before.
I am ABD in mathematics. That was a long time ago. I taught math for many years at a community college. My amateurish but knowledgeable perspective is that these developments shatter the mystique for me.
What AI is showing is that mathematics is mostly just pattern searching and AI can do this far better, faster, and with a much wider base than humans can. When I was working on my thesis problem I realized that I worked much less than my fellow students. I was an average student in my program but even for the best students they had to spend a lot of time thinking about stuff. They put in a lot of effort.
Is the difference between me and Tao mostly effort and that he has a much better memory of mathematical facts than me?
This is only the "problem solving" side of mathematics. Completely missing the theory builders who have completely reshaped the world of mathematics (and far beyond). AI is a long way from matching original thinkers of the calibre of Euclid, Al-Khwarizmi, Newton, Leibniz, Euler, Galois, Riemann, Cantor, Hilbert, and Grothendieck. Or Turing, Gödel and Von Neumann?
According to Tao and Gowers there are AI results that did proofs in clever ways. That’s one way new theories come about.
I lean more towards the "proofs from the book" mindset - if there's a really beautiful proof of some theorem out there I would be happy to see it no matter whether it was discovered by a human or a computer, and conversely if a computer has churned through a search space and generated a clunky proof in 100000 lines of lean code that just means that people trying to find a nice proof can do so with the assurance that the theorem is true. note that mathematicians didn't give up on trying to find a better proof of the four colour theorem once a clunky computer assisted proof showed the theorem was true.
The question is, will universities continue to fund graduate programs to the extent they currently do so that people can find elegant proofs of AI derived theorems? I’m skeptical. A lot of good mathematicians tried to prove or disprove the Jacobian Conjecture and AI did easily. The value added by human mathematicians seems to be low return on the investment.
that is a genuine concern, yeah :( but at least for me it's unrelated to the mystique of mathematics itself.
Just like in chess, at some point the problem at hand and its solution becomes so unwieldidly complex that you either make of it the work of your life or you use a math/chess engine to handle the complex stuff.
Just like you can find a forced mate in 120 moves for a given position, you can find a 120 pages of pure gibberish demonstration of some conjecture with its lean check.
The thing is to not become reliant on it and just cheer it up so it makes progress on its own in the Riemann hypothesis, but to use it like a lever to lift heavier stuff, as Dr. Tao does here.
I saw an interesting article in the Atlantic[^1] somewhat recently predicting that the people who will thrive in the AI age will be ones who enjoy mental effort. That is, even when AI could do something for them, these people will choose to do it themselves if there’s something to be learned from it.
This post seems to illustrate the point perfectly to me. AI wrote the proof. It was done, Lean checked it. And presented with that, Tao’s reaction is still to want to learn something—how to solve the problem himself—and then to meticulously untangle a 90k-line machine proof (utterly disregarding that there’s no clear upside for doing so—he can’t get a paper out of this) because it’s the only way to learn that. My bet is that it was worth it.
(I also think everyone saying “it doesn’t make sense to write code anymore” is crazy. The best learning tool of all time was just invented, and you want me to not use it? What the point of any of us if not to know things?)
[^1]: https://www.theatlantic.com/ideas/2026/06/ai-open-ai-anthrop...
Making things understandable is part of intelligence as much as producing the initial artifact is. Even if the proof checks out in Lean (or the code runs and passes QA) if it's a mess, it will be hard to use it to do anything further.
This does not only matter doing cutting-edge mathematics. This, about the 'digested' version versus the original, should feel familiar to some folks here:
> This formalization is more streamlined than the original formalization (it has about 15,000 lines of code, compared with around 90,000 for the original proof).
and if you've ever tried to turn an overly vibed piece of code into something that makes sense:
> it has taken me several days (with heavy AI assistance) to perform such a digestion, to place the proof in proper context with previous literature and to simplify and streamline the argument to highlight the main ideas
If you see something that is confusing or overly clever, please don't assume it must be for some good reason you don't understand and move on--ask questions, get it simplified, try to get it worked out. Future you will appreciate it.
"The proof ends up being remarkably elementary."
Dude then proceeds to dump about 16 A4 pages worth of heavy-duty algebra which 99.999% of the humans on the surface of this planet are completely unable to read past the first two lines.
LOL, I guess language is a "remarkably" vague tool, where "elementary" means vastly different things to different people.
That doesn't diminish the achievement of course, but ... please, easy on the "remarkably elementary" next time, that's borderline insulting.
"elementary" does not mean simple or easy, it refers to the domain of mathematics involved in the proof. https://en.wikipedia.org/wiki/Elementary_proof
Your definition of "elementary" is the one used by the other 100.0 - 99.999 %
Thank you for making my point for me.
Ivory tower much?
It's not the OP's definition, it's the definition of the word as used in mathematical practice, as evidenced by the Wikipedia article cited.
It's a habit of the community. Tao actually elaborates on what he means by this in the same paragraph.
I'd like to offer a charitable interpretation. By Tao labelling it as "remarkably elementary", he encourages less experienced mathematicians (including students) to go and read the proof for themselves. He's advertising a low barrier to entry for certain parts of his audience. This isn't always the case with whatever he reports on, so it's worth pointing out when it's true.
“Remarkably elementary” in mathematics means accessible to people who have finished the first 1-3 years of grad school where you go through the canonical entry level courses in research level mathematics. There’s no reason to think Terence’s blog is aimed at a general audience.
[dead]