There is a finite capacity/time for a human mind to do difficult shit, if it can be slop forked in a microsecond before you even get to flesh it out there is no point
The people building AI claim it will surpass human intelligence in all
respects and prerhaps kill
us all. Should we just cease all human activity on the basis of what AI might do in future?
Personally, I doubt AI can surpass a good human explainer because explanation requires empathy, which benefits from being an instance of the kind of entity you are explaining the thing to. That gives you a way of exploring and evaluating the space of possible explanations that isn't available to an LLM.
Thanks for pointing me to this video - it's been interesting to follow the discussion! (I personally don't see that math has lost its purpose at all in the past months. I mean, where would we be, if we were thrown at these AI based mathematical proofs and had no mathematicians and specialists?! Much of this discussion is about a disciplin readjusting its way of work and tasks.)
It starts to sound like medieval science - "understanding" instead of proofs. And like a medieval army loosing a battle in the open field tries to retreat back into the fortress, people, facing the prospects of machine doing intelligent tasks better than humans, start to retreat into areas like intuition which supposedly aren't reachable by the machine. Some go even further starting to talk about religion. It is very Hegelian that the crown jewel achievement of our civilization starts to drive people away from the foundational principles of that civilization.
Basing science on proof (or anyway believing that you can) is Logical Positivism, a mindset that opposes the method of falsifiability. But of course mathematics is all about proof, and for that reason I was wary of it for a very long time.
Basing science on proof (or anyway believing that you can) is Logical Positivism, a mindset that opposes the method of falsifiability
not really. You can consider positive proof as an experiment confirming your theory and the negative proof and counter examples as an experiment falsifying your theory.
Yes, really. "Positive proof" opposes the concept of falsification. You can only have it within a system formal logic, and science can contain those, but isn't one.
"Positive proof" opposes the concept of falsification.
no. Positive proofs have nothing to do with falsification. They just tell you that there is no point in spending effort on searching for negative proofs and counter examples. They don't prevent nor prohibit you from spending that effort. They just advise you that that effort will be wasted.
It is like nobody prevents from experiments to turn lead into gold. Of from searching for a right angled triangle violating Pythagoras.
Understanding has been the point of mathematics for millenia. The idea that purpose of math is to produce machine-checkable proofs is an entirely modern idea.
While I understand and emphatically with Tao's concern I'm afraid it's missing the forest from the trees. Unless you can make a claim that AI will never be able to perform intellectually at the same level as any human at a much lower cost, there's an outstanding utility problem that remains unaddressed.
Sure enough, the AI may not have taste or goals, or many human traits, but that's irrelevant to the much thornier (and much broader than mathematics or even academia) question related to who's getting paid how much and for what.
The funding on mathematics is already one of the lowest accross science [0, 1], and theoretical math funding is probably much smaller than the applied math one already, so that's not even close to how much funding theoretical math gets.
So, we are talking about a field that already does not use that much funding anyway, and most high end theoretical mathematicians probably would make much more money in the industry anyway, so this seems like missing the forest for the tree imo.
There's an old joke about funding, goes something like:
"Why you are always demanding more funding? Why can't you be more like the mathematicians, all they need is a desk, some paper, and a pencil, and a garbage can, and they just do fine. Or how about philosophy, for that matter? They don't even need the garbage can"
I mean, obviously with modern computational mathematics, this doesn't hold so simply, but there is this confound about math research also not getting much funding also because much of it isn't that expensive, relatively speaking.
I enjoy learning math from LLM proofs with the help of LLMs https://github.com/htzh/flt_for_human . It is amazing how well models do when they are well grounded by formalized proof traces (even if created by other models).
I'd be interested in hearing a field report on this! For example, I can easily imagine that they're great at walking through the proof step by step, explaining background as necessary; but as TFA notes, one of the most important questions is "why is this definition the way it is?", and my bet would be that the Lean is not enough to help the LLMs meaningfully in answering that.
I’m reminded of that famous debate between Poincaré and Hilbert at the International Congress of Mathematicians in Paris in 1900. It was then that everyone decided to follow Hilbert’s path, and proof came to be valued more than intuition. I think modern math at school and at applied university kind of lost this intuitive part. I try to teach my students that mathematics is, first and foremost, a very precise language of communication. It’s sometimes amusing to ask those who don’t like math to do without it entirely, just to see how much harder it becomes to describe the things around them. Second thing I tell them, formulas are the essence of mechanisms in their purest form. And in this form, they’re much easier to grasp and mentally manipulate. It always amused me, after taking a mechanics course, to imagine that for any formula, you could visualize a mechanism or process that implements it. And third thing, I suppose, the ability to verify one’s own statements as proof. Although, of course, mathematicians would probably tear me apart here for my heresy:sorry, I’m not a mathematician, but an engineer. You can make mistakes by using incorrect assumptions, but at some point, analysis itself will show you that you were mistaken. There’s a wonderful book, How to Prove It by Daniel Velleman, which provides an introduction to proof for the uninitiated like me. I really enjoyed it.
People often hate math because it was not explained to them correctly, usually by people who are good mathematicians but know close to nothing about teaching.
It was so infuriating to see everyone in the class absolutely fail on a specific subject and the "teacher" assumed that everyone must be stupid then. No self reflection, no questioning himself why he is not getting gaussian distribution in marks, just straight Fs.
I have a hatred for people who think they can use this method.
If used incorrectly which it is a great percentage of the time it confuses the student. The person employing the socratic method must actually know the answer and where the student is in their mind. Failure on either account makes it pointless.
Ask anyone unfortunate enough to ask for help on IRC
That only works if the one you're trying to guide can figure it out mostly on their own and is interested in cooperating. Aka does not work for anything below university level.
usually by people who are good mathematicians but know close to nothing about teaching.
I higly doubt that. Maybe in university level courses. Most people’s only experience with mathematics is an elementary or high school teacher who were probably themselves at best mediocre at the subject. Simply because of selection factors. Those who are good at math are encouraged to go into STEM. There will be of course exceptions everywhere, but that is not what “usually” happens.
And thats just about being good at maths the school subject, which is distinct from being “ good mathematicians” the science / research topic. Mathematicians are few and far between, simply because it is a specialist subject. There just aren’t enough of them to go around for them to be the formative experience around math for most people.
I think the problem is partly circular. Most people do not like maths. This includes most primary school teachers - in places I know primary school teachers are not subject specialists so just reflect the population of those with the required level of education in terms of their attitude to maths.
My daughter hated maths when I took her out of school at the age of nine. A few years later she was very good at it and enjoying maths and STEM subjects. When she went to a sixth form college[1] she liked it well enough to pick it as one of her A levels[2].
Another response to math that makes me sad: "I must be too stupid to understand this," "my brain is too small for this," etc. Different people say it for different reasons, but it's almost always in response to a hand-wavey explanation that doesn't makes sense to anyone not already in the know. Math is so much more about humility and skepticism than it is prodigy.
This is tricky, because, in fact, hard math having an intelligence floor is one of the nastier realities of the human condition. Anyone who is even quite intelligent but has really pursued the rigorous stuff, unless they are in fact a prodigy, eventually realizes they have an abstraction ceiling (and this term is a common one thrown around in people studying mathematics, because intelligence denial is so obviously false when you do hit your abstraction ceiling).
Most people are correct that they lack the intelligence / mind for a lot of hard math (even epsilon-delta proofs are enough to eliminate the majority of the population, no matter how good a teacher you are, and these are just basic undergrad calc).
And yeah, sure, people have different kinds of intelligence and such, but there is still a g-factor, and people of low intelligence almost universally can't do hard math, whereas most people who can do e.g. advanced undergrad math can generally do almost all other advanced undergrad fields reasonably well. The world isn't fair here.
Anyone who is even quite intelligent but has really pursued the rigorous stuff, unless they are in fact a prodigy, eventually realizes they have an abstraction ceiling
Eh. I'm a math PhD who fled academia because it was too much for me. But I have never encountered this term "abstraction ceiling" nor did I succumb to it. I simply ran out of motivation to pursue higher math, especially when following through on learning and research became more and more labor. (It was always labor; but it was a labor I used to love.) I am far from a prodigy.
even epsilon-delta proofs are enough to eliminate the majority of the population, no matter how good a teacher you are
Disagree. It's a notoriously hard subject to teach, and with all the demands placed on e-d in so little time in your average curriculum, it doesn't require appeals to IQ to explain its infamy. With enough motivation and practice, the quantifier alternation is comprehensible to any sound mind. What your average mind (and student) lacks is exposure to formalism, abstraction, and how these things tie in with what they are familiar with, which is symbolic manipulation. With the exception of geometric proofs (another educational bugbear), they have little context for what formalism is or why it matters.
Eh. I'm a math PhD who fled academia because it was too much for me. But I have never encountered this term "abstraction ceiling" nor did I succumb to it.
This sounds a lot like you may have in fact succumbed to your abstraction ceiling, because in practice, the ceiling manifests as not as it being impossible for you to learn something, but that it would take you years and inordinate effort to master what you notice others mastering easily in just a fraction of the time. You may have not heard the exact term (comes from Douglas Hofstadter), and you may be talking about just the academic busywork, but I find it hard to believe you never encountered discussions about this kind of stuff. I would also politely suggest that unless you are Terry Tao posting under some kind of alt, you most certainly do have an abstraction ceiling (or your own mathematical limits) too.
It's a notoriously hard subject to teach, and with all the demands placed on e-d in so little time in your average curriculum, it doesn't require appeals to IQ to explain its infamy. With enough motivation and practice, the quantifier alternation is comprehensible to any sound mind
The latter statement is obviously false, but regardless, intelligence explains some of the difficulty, and much other difficulties far more parsimoniously than "everyone could just learn any math if they just tried hard enough and had good enough teachers". E-d is merely an obvious and generally familiar example, and nothing I said really relies on this very specific aspect of maths, obviously. We also shouldn't pretend your (almost certainly false) view of math and intelligence isn't also often harmful to struggling students in its own way.
People often hate math because it was not explained to them correctly
Spoiler: this is also why mathematicians hate vibe-math. AIs are outright terrible explainers even when they do have a watertight logical argument—and honestly, this is the load-bearing seam.
It goes beyond "proof vs. exposition": the logical derivations AI comes up with fail to even qualify as human-directed proof because of how terrible they are (far below even the most novice mathematician doing their roughest work) at the exposition part.
AIs are outright terrible explainers even when they do have a watertight logical argument
I think this only applies to cutting edge mathematics (novel proofs of hard problems). I have seen it reported more than once that such AI proofs are cumbersome to follow.
But in my experience, when it comes to explaining well-established math that is already in the training data, AIs can be very good teachers (at least with recent models). Especially if you use it along with a textbook and ask it about anything that might not be explained well in the textbook.
Similarly, programming is also a precise language of communication. Initially, we focused on direct machine behavior but every abstraction above the hardware (including assembly) has been to make that behavior legible to humans.
Developed notations and shared procedural abstractions have made thinking about computation more intentionally human and source control has established a protocol for conversing with other humans in the language of a program and changes to that program.
The moment just now feels like a neglecting of the idea of communication being central. If the program is a compile target but not sufficiently legible or if the conversation moves too quickly for us to keep up then we retain the effects of computation but loose its meaning as communication. We loose the understanding and the ability to develop and evolve further shared abstractions.
Open source programs could be more like motivated explanations of computation. For open source to survive, maybe we should start to make the distinction between free product distribution and programming as communication and community building.
Open source programs could be more like motivated explanations of computation.
It is already that. Every time a method/function is created, a structure is defined, a variable is added, a file is created or renamed,… It’s all for the purpose of human communication. The computer only need binary in a single file.
But people feels like they should be able to jumpninto curl code without any understanding of networking, or linux code with no knowlede of computer architecture. Few code are meant for total beginners.
As a math prof, I care(d) much more about proof than intuition, not because proof is more important, but exactly because intuition is (I'm a bit Chesterton-ish here haha). You cannot do proof without intuition hence, if you emphasize proof, intuition will take care of itself. Whereas if you emphasize intuition, students won't have any idea of what a rigorous proof should be.
Even if we can proof/disproof any statement in Math (not possible due to halting problem), Human still need to decide which statement to be called "theorem".
The theorem thing is invented by human to help other people better understand Math structure in a easier way.
It's interesting because, as far as I'm aware, the vast majority of people already believe that math is more than proof. A slightly smaller but still very large majority don't even include proofs in their mental concept of what math involves.
A majority? I doubt it, simply because the majority doesn't know what math is at all.
At university level introductory calculus, the person teaching class had to reassure students that math wasn't entirely arithmetic or adding up numbers. He did this because it's a common misunderstanding.
Haha, sort of. I guess I disagree with your claim the majority of people think math is "more" than proof. The majority of people think it's less: they think it's doing high school arithmetic. Most people don't know what a proof or a theorem are. They think math is doing calculations with numbers.
Also, his opinion of AI has continually changed in the past years, after the capabilities were demonstrated.
Ignoring the other ridiculous parts of your comment, isn't this exactly what you're supposed to do? Update your beliefs according to the newest information available?
One thing that concerns me from all this is "understanding" is very important to human progress. The fact it took 400 years to crack Fermat's theorem resulted in a lot of "Side Quests". These side quests helped grow other fields (for instance elliptical cryptography). Im concerned with AI that we will loose these side quests.
I do neither maths nor science with AI but in my experience most models are perfectly willing to burn tokens on a ton of sidequests at the earliest opportunity.
I can’t help but feel a little schadenfreude. STEM folks may soon find themselves masters of skills as esoteric as translating Ancient Greek poetry or analyzing 18th century novels. The ability to construct complex mathematical proofs will become a party trick, rather like the ability to mentally multiply 10 digit numbers. The arguments that STEM snobs dismissed in favor of the study of the humanities will be the very same arguments that they now turn to. We will hear about how math and science make you a better rounded person, have inherent as well as instrumental value, etc. etc.
Of course they can. My point is that mathematicians may increasingly find themselves in the same position as academics in the humanities. Mathematicians themselves will be able to see the inherent value of the work they're doing (just as experts on 18th century novels can in their own field), but it will be far less obvious to society at large why their work should be funded.
Its a reasonable view to take that "human math" [ math residing in human minds ] is the only math that counts.
Math that only resides in the weights of models, or arcane forms such as a long lean proof or even an unread textbook .. is not the math that we should be striving for.
Likewise all other technology [ and culture ].
LLMs and AI / AGI / ASI could lead to a new renaissance of math discussion and expansion of human math and science. Or the opposite, where we outsource all our thinking to the AI, and no new generation of artisans is trained by doing hard problems, and in a generation we have killed off human math.
Likewise all of the fields of human intellect. We need to make sure we protect future generations of doctors, biologists, software developers, architects, engineers, librarians, musicians, artists ...
A moratorium on AI development might be the only way to achieve this preservation of human culture.
one of the obvious applications of novel mathematical results is in building stronger AI models.
This gets repeated a lot and seems to be one of the primary stated goals of making AI solve math problems, but I still have no idea by what mechanism this is even supposed to happen. I guess they could make some minor improvements to matrix multiplication algorithms or whatever but I don't see what groundbreaking theorem could possibly significantly improve LLMs.
It's the kind of thing where it's sort of expected that you wouldn't know, right?
I think we don't really understand why deep learning works as well as it does, the thinking around that is, as far as I can tell, mostly a collection of empirical observations.
A fundamental theory of learning that can be used to predict optimal network architectures might enable smaller models that consume less energy.
Likewise all of the fields of human intellect. We need to make sure we protect future generations of doctors, biologists, software developers, architects, engineers, librarians, musicians, artists ...
So many thoughts come to mind at once, they're a jumble in my head rather than a single coherent narrative.
John Henry comes to mind. As does Agent Smith's "I say your civilization because as soon as we started thinking for you, it really became our civilization, which is, of course, what this is all about" monologue in The Matrix. I've not read (or listened to) "With Folded Hands ..." or "The Machine Stops", but I have read the Wikipedia plot summary of both.
Do we want to have comfortable lives, or do we want to serve each other?
"Computer" used to be a profession; I grew up around adults bemoaning that "kids these days can't do mental arithmetic", the Pi Zero I've not switched on for probably a year now could beat all humans simultaneously at that (even if everyone was as good as the current world record holder) and yet we still teach arithmetic in schools.
Nobody needs to knit, and yet we do so for fun. Youtube's "Primitive Technology" channel, which has spent around a decade speechlessly making iron from bacterial slime found in a creek, using only clay and sticks and leaves and vines naturally found next to that creek.
Like I said, no coherent narrative. It's been a while since my stream of consciousness became a river delta; usually at worst it only meanders a bit.
The math field is confronting something that coders have been dealing with for a few years now, only far more violently. Today's moat for software seems to be that AI can automate tasks but not a full job (yet). But for a large proportion of mathematicians, doing these tasks really was _the_ job. It's the bit they wanted to do, and if they completed a sufficiently difficult set of tasks, they got tenure. Now this model is failing, they frantically need to pivot the role of humans to save their profession from funding cuts.
I remember when "writing code was never the point" became a mantra here. There was truth in it, but removing the coding has certainly taken away a lot of the texture of the work and enjoyment of the craft. Many of us feel this loss as we tech-lead teams of agents as our source of income. I am not optimistic the mathematics pivot is going to work, but I'm certain that most will be depressed with the outcome even if they succeed.
We are all staring at the same existential dread, just seeing it unfold slower. We're being told that utopia is to be obsolete, and that is a jarring idea to contend with.
The last days we are served these high goals about understanding, "digestion" and so on.
But if you look at the practice of present mathematics, in the last 20 years it is all about publishing solutions to problems.
There are famous problems to be solved, there is a hierachy of conjectures to be solved. A quick search here on HN gives pearls like "Theory building papers are dime a dozen and don't get published in high tier journals unless they solve a problem".
And all of a sudden it turns out that problem solving can be automatized.
So then what will problem solvers do? Well, from now on they will "digest" problems solved by AI.
In a way or another they will find a way to stay on top.
That's the goal, at least, but mathematics as a living practice does not have much to do with these games of power.
Yes. AI is a useful tool and we are going to adapt and use it.
The phd student will be forced to publish 10 breaktrough articles, the university department which does not offer "free" access to AI (for its members) will see the its ratings going down, when compared with the other universities.
It will be "use AI or perish" for academic management so on the side of academic management the ones with vision will thrive and the ones without will perish.
But what about the publishers? In the last decades the academic research was made into a feeder for publishers. The main goal of a researcher is to write articles, which are later sold back to other researchers.
This economic system is under big stres now, because for a while at least the academic management and publishers will have contradictory goals.
And that is why this scare which is induced by those who profit the most from the present system.
“You are right. There is nothing in yesterday’s mathematics that you can prove with
exterior algebra that could not also be proved without it. Exterior algebra is not
meant to prove old facts, it is meant to disclose a new world. Disclosing new worlds
is as worthwile a mathematical enterprise as proving old conjectures.”
Gian-Carlo Rota in “Indiscrete Thoughts”
1. We humans have managed to take huge amount of information and compress it using a loss function containing some bias we have about the information.
2. We now ask ourselves to decompress the same information with some additional cross-entropy. As a side effect of this process we sometimes spurt out information that may or may not have any meaning since the compression was lossy.
3. Now, we ask ourselves to present this some-what newly decompressed information with brevity in order to understand what we've learned from it.
Knowing that this process is happening on a larger scale, this resurfaces the argument if meaning can be reduced to computation only.
Although some might favor this argument but we are at the risk of anthropomorphizing this process.
The idea presented in the post itself is perspicuous (in Grant Sanderson own words) as he always does.
Part of the controversy here is that now the skill advantage that some Field Medalist had is much narrower. The fact that fields medals have an age limit implies that it favors brain power over understanding. And that was the guiding light award of the community. So i find it "funny" (and natural) when they are offended by AI.
That is the main "crisis" of mathematics.
In my opinion there has never been a better time to be a mathematitian, and there has never been a better time to be a software builder.
But there has never been a worst time to have the need to prove your economic value as a mathematitian or software developer alone. Because "understanding" is not something you can prove in one afternoon, its something that you prove with a life.
In my opinion there has never been a better time to be a mathemetician...
As an ex-mathematician I assure you this is very wrong, and every working mathematician I know right now is completely miserable, and/or trying to flee the field as fast as possible. It's like telling a chair-maker during the industrial revolution that there had never been a better time for them, since now they could operate chair-making machines instead of toiling away at the wood themselves. It assumes that they were purely in it for their passion for mass-producing chairs. The majority of mathematicians get into the field because they love problem solving, and the gauntlet thrown down by challenging math tasks.
Many parts of this will never be useful for society on a grander scale - but this is reflected in the finances - pure math is closer in funding-terms to a humanity than to hard science. Now even this is _massively_ under threat, and Tao and co need to pivot quickly to stop this from becoming a bloodbath.
Probably true for the dedicated problem solvers (of which Tao is one IMO). But I doubt there's ever been a better time to be a theory builder (more like Peter Scholze, or Grothendieck).
Some up with an idea and leave the system to check it 15 different ways, and see whether you can simplify an existing body of theory. It'd be like having an army of lightning-fast grad students.
I'd even say Scholze is not a great example here. Most of the work he's known for is progression towards the Langlands program - which is very much a problem to be solved, and one I would imagine he'd not be thrilled for an AI to one-shot. I agree that it is somewhat 'up the chain', in the same way that software engineering has not immediately disappeared now that performing coding tasks is largely automatable.
But I also take issue with 'never been a better time' - e.g. is this really the greatest time to be a software engineer? Everyone has AI psychosis and feels like they're a couple of breakthroughs away from being unemployable. The same is even more true in math - we've gone from failing IMO problem 6 last year, to solving NS. The rate of change is formidable, it feels like there may not be many places to hide in a few years.
Im an ex mathematitian too. And if i was in academia I would probably have the same reaction. Thats what i say that its the worst time for proving economic value.
But if you are in for theory building and understanding, then you are not constrained anymore by your motivation to grind through countless hours of formal theorem proving. And you do not need to have superhuman formal manipulation skills and memory.
For me mathematics is not the formal system, so LLMs will never be able to do end to end maths.
Hmmh. I like motivated explanations, but, as acknowledged in the text, this is a subjective thing to measure. What is a great motivated explanation for Tao, might be hard to grasp for me. So I guess judging how well an explanation motivates something depends on two things: 1) My way of thinking, and 2) what I already know and how well I recall it in this context.
There is a third thing: how well does the motivation chime with or go against my current belief system? You would think this is not much of an issue in mathematics, but it can be, and I had my fair share of frustrations because of it.
Anyway, all of the above points to one thing: the best motivated explanation will be generated by an AI, knowing the subject and you in a deep way that no other human will, and being able to interact with you during the explanation.
The blog post says that the statement "AI really did solve a problem in mathematics." is wrong. But a formal proof showing that Navier-Stokes equations can blow up is certainly such a solution, by AI. There is not much in this world that is more objective than a formal proof, so any disagreement on this is based on how we see the world. Michael Harris will agree with the statement being wrong, Jacob Tsimerman will not.
Hilbert famously battled Brouwer's view of mathematics. From my point of view, Hilbert was right: intuitionistic logic is certainly interesting; but I like to study it using "normal" (= classical) mathematics.
My personal frustrations are about how hard it is to publish my work on abstraction logic. I would never have thought it is that difficult, mathematics being objective and all. It seems essential to take out as much motivation out of your paper as possible, because it might offend your reviewers and their belief system. By now my papers come with full Isabelle/HOL formalisations, let's see if that helps.
1) My way of thinking, and 2) what I already know and how well I recall it in this context.
I don't think we're discussing pedagogy. Good _research_ exposition is instead related to communicate your intuition and way of seeing things. The conceptualization of a given situation or problem is what is valuable, how you connect it with other stuff, etc. It is then up to you to memorize and interiorize it.
It would be interesting to see what would happen if we had two competing mathematical institutes, a sort of First/Second Foundations:
1) Rejection of AI for anything but trivial applications while still using computers at their full capacity. Researchers would ensure full human understanding of proofs and methods. This Institute believes on Math as a process of discovery, Mathematicians as explorers/poets/storytellers and not proof machines.
2) Unrestricted, all-embracing use of the latest AI, including potentially research in creating even better AIs as part of the program. These researchers would be okay with not understanding proofs if verified to be correct. This group is focused on rapid problem resolution and believes Mathematicians are theorem creators and provers.
After X years (100?), which one would advance Mathematics and humanity the most (we'd need to define "advance")?
Mathematicians worry about proofs and the intrinsic value of something as elusive as 'understanding'. They are deeply ingrained in the study, deeply concerned with anything effecting the field. Yet they're still emotional beings looking for beauty and meaning in life that might come from an understanding how the universe works purely from a math perspective. I'm glad Mathematicians exist, I certainly can't do that type of work.
And I trust their results: technology wouldn't be possible without advancing our understanding of the world in various fields, including math.
Your idea sounds great for the Mathematicians.
There's a more pragmatic view though, and unrelated to proofs themselves: does understanding a proof help us to advance Humanity in some way?
Do we have better lives afterwards? What if we give up understanding proofs and focus only on results.
In other words, if an AI solves a problem for you, but you don't understand how it works, should you continue building anything on top?
I suppose the results are truly what matter. If AI solved cancer, disease, anything that lowers quality of life, but you have no idea how it did it: is that good enough?
What if there is no true beauty in Math, the way Dirac and Einstein wanted?
I'll answer one of your points partially: if AI builds a better sorting algorithm and proves its performance characteristics, it's useful. I'd be able to use it to make my programs faster even if I don't/couldn't understand it.
It would be a bit disappointing but still useful and make humanity slightly better.
Software is logic applied to intersubjective truth. It's not physical truth which is the subject of the hard scientific fields such as physics and chemistry, as well as biology for the most part.
It was a short film called Outside In, perhaps the earliest example of a viral video about substantive math, visualizing the key idea of Thurston’s own construction for sphere eversion.
This goes in a necessary direction, from my personal take away of Gower's recent post on the subject.
Mathematics is suffering from Goodhart's Law:
"When a measure becomes a target, it ceases to be a good measure."
Doing something difficult was a signal that you:
a- understood it and all the background information it requires
b- internalized techniques and methods that are helpful in problem solving in general
Now it just means nothing
Now it means we can move on to other difficult shit.
There is a finite capacity/time for a human mind to do difficult shit, if it can be slop forked in a microsecond before you even get to flesh it out there is no point
Well then you have time to invent some new difficult shit.
3Blue1Brown: The last IMO problem AI could not solve:
https://www.youtube.com/watch?v=Nbwv5wHQoj0
Timothy Gower
Jacob Tsimerman claims [1] we might have superhuman expositors by April, so then what?
[1] https://youtu.be/H7_d_sgui6o?t=4436 (timestamped url)
It's all good until we have superhuman appreciators :)
The people building AI claim it will surpass human intelligence in all respects and prerhaps kill us all. Should we just cease all human activity on the basis of what AI might do in future?
Personally, I doubt AI can surpass a good human explainer because explanation requires empathy, which benefits from being an instance of the kind of entity you are explaining the thing to. That gives you a way of exploring and evaluating the space of possible explanations that isn't available to an LLM.
Thanks for pointing me to this video - it's been interesting to follow the discussion! (I personally don't see that math has lost its purpose at all in the past months. I mean, where would we be, if we were thrown at these AI based mathematical proofs and had no mathematicians and specialists?! Much of this discussion is about a disciplin readjusting its way of work and tasks.)
It starts to sound like medieval science - "understanding" instead of proofs. And like a medieval army loosing a battle in the open field tries to retreat back into the fortress, people, facing the prospects of machine doing intelligent tasks better than humans, start to retreat into areas like intuition which supposedly aren't reachable by the machine. Some go even further starting to talk about religion. It is very Hegelian that the crown jewel achievement of our civilization starts to drive people away from the foundational principles of that civilization.
Basing science on proof (or anyway believing that you can) is Logical Positivism, a mindset that opposes the method of falsifiability. But of course mathematics is all about proof, and for that reason I was wary of it for a very long time.
not really. You can consider positive proof as an experiment confirming your theory and the negative proof and counter examples as an experiment falsifying your theory.
Yes, really. "Positive proof" opposes the concept of falsification. You can only have it within a system formal logic, and science can contain those, but isn't one.
no. Positive proofs have nothing to do with falsification. They just tell you that there is no point in spending effort on searching for negative proofs and counter examples. They don't prevent nor prohibit you from spending that effort. They just advise you that that effort will be wasted.
It is like nobody prevents from experiments to turn lead into gold. Of from searching for a right angled triangle violating Pythagoras.
Fortunately this is not basing science on proof. It's just making it much easier to do proofs when that is what we choose to do
Understanding has been the point of mathematics for millenia. The idea that purpose of math is to produce machine-checkable proofs is an entirely modern idea.
While I understand and emphatically with Tao's concern I'm afraid it's missing the forest from the trees. Unless you can make a claim that AI will never be able to perform intellectually at the same level as any human at a much lower cost, there's an outstanding utility problem that remains unaddressed. Sure enough, the AI may not have taste or goals, or many human traits, but that's irrelevant to the much thornier (and much broader than mathematics or even academia) question related to who's getting paid how much and for what.
The funding on mathematics is already one of the lowest accross science [0, 1], and theoretical math funding is probably much smaller than the applied math one already, so that's not even close to how much funding theoretical math gets.
So, we are talking about a field that already does not use that much funding anyway, and most high end theoretical mathematicians probably would make much more money in the industry anyway, so this seems like missing the forest for the tree imo.
[0] Table in page 1 in https://nsf-gov-resources.nsf.gov/files/71_fy2025.pdf?Versio...
[1] Figure DISC-13 in https://ncses.nsf.gov/pubs/nsb20257/academic-r-d
There's an old joke about funding, goes something like:
"Why you are always demanding more funding? Why can't you be more like the mathematicians, all they need is a desk, some paper, and a pencil, and a garbage can, and they just do fine. Or how about philosophy, for that matter? They don't even need the garbage can"
I mean, obviously with modern computational mathematics, this doesn't hold so simply, but there is this confound about math research also not getting much funding also because much of it isn't that expensive, relatively speaking.
The article isn’t by Tao, it’s a guest post by Grant Sanderson (aka 3Blue1Brown).
I enjoy learning math from LLM proofs with the help of LLMs https://github.com/htzh/flt_for_human . It is amazing how well models do when they are well grounded by formalized proof traces (even if created by other models).
I'd be interested in hearing a field report on this! For example, I can easily imagine that they're great at walking through the proof step by step, explaining background as necessary; but as TFA notes, one of the most important questions is "why is this definition the way it is?", and my bet would be that the Lean is not enough to help the LLMs meaningfully in answering that.
Fortunately LLMs are smart enough to handle that already.
I’m reminded of that famous debate between Poincaré and Hilbert at the International Congress of Mathematicians in Paris in 1900. It was then that everyone decided to follow Hilbert’s path, and proof came to be valued more than intuition. I think modern math at school and at applied university kind of lost this intuitive part. I try to teach my students that mathematics is, first and foremost, a very precise language of communication. It’s sometimes amusing to ask those who don’t like math to do without it entirely, just to see how much harder it becomes to describe the things around them. Second thing I tell them, formulas are the essence of mechanisms in their purest form. And in this form, they’re much easier to grasp and mentally manipulate. It always amused me, after taking a mechanics course, to imagine that for any formula, you could visualize a mechanism or process that implements it. And third thing, I suppose, the ability to verify one’s own statements as proof. Although, of course, mathematicians would probably tear me apart here for my heresy:sorry, I’m not a mathematician, but an engineer. You can make mistakes by using incorrect assumptions, but at some point, analysis itself will show you that you were mistaken. There’s a wonderful book, How to Prove It by Daniel Velleman, which provides an introduction to proof for the uninitiated like me. I really enjoyed it.
People often hate math because it was not explained to them correctly, usually by people who are good mathematicians but know close to nothing about teaching.
It was so infuriating to see everyone in the class absolutely fail on a specific subject and the "teacher" assumed that everyone must be stupid then. No self reflection, no questioning himself why he is not getting gaussian distribution in marks, just straight Fs.
a good teacher remembers the journey, not just the destination.
socratic method exists. almost none follows it.
I have a hatred for people who think they can use this method.
If used incorrectly which it is a great percentage of the time it confuses the student. The person employing the socratic method must actually know the answer and where the student is in their mind. Failure on either account makes it pointless.
Ask anyone unfortunate enough to ask for help on IRC
I sometimes ask more questions than utter new things when trying to explain something.
But that's because I'm trying to focus down and determine exactly where they're at before I just randomly make things worse by accident :-P.
I'm not sure if that's the actual socratic method. But people accuse me of using it. Either way, it does seem to work for me.
That only works if the one you're trying to guide can figure it out mostly on their own and is interested in cooperating. Aka does not work for anything below university level.
I higly doubt that. Maybe in university level courses. Most people’s only experience with mathematics is an elementary or high school teacher who were probably themselves at best mediocre at the subject. Simply because of selection factors. Those who are good at math are encouraged to go into STEM. There will be of course exceptions everywhere, but that is not what “usually” happens.
And thats just about being good at maths the school subject, which is distinct from being “ good mathematicians” the science / research topic. Mathematicians are few and far between, simply because it is a specialist subject. There just aren’t enough of them to go around for them to be the formative experience around math for most people.
I think the problem is partly circular. Most people do not like maths. This includes most primary school teachers - in places I know primary school teachers are not subject specialists so just reflect the population of those with the required level of education in terms of their attitude to maths.
If you do not enjoy a subject, any subject, you cannot make it fun for those you teach. In the case of maths specifically its pretty bad: https://worrydream.com/refs/Lockhart_2002_-_A_Mathematician%...
My daughter hated maths when I took her out of school at the age of nine. A few years later she was very good at it and enjoying maths and STEM subjects. When she went to a sixth form college[1] she liked it well enough to pick it as one of her A levels[2].
[1] https://en.wikipedia.org/wiki/Sixth_form_college
[2] https://en.wikipedia.org/wiki/A-level
Another response to math that makes me sad: "I must be too stupid to understand this," "my brain is too small for this," etc. Different people say it for different reasons, but it's almost always in response to a hand-wavey explanation that doesn't makes sense to anyone not already in the know. Math is so much more about humility and skepticism than it is prodigy.
This is tricky, because, in fact, hard math having an intelligence floor is one of the nastier realities of the human condition. Anyone who is even quite intelligent but has really pursued the rigorous stuff, unless they are in fact a prodigy, eventually realizes they have an abstraction ceiling (and this term is a common one thrown around in people studying mathematics, because intelligence denial is so obviously false when you do hit your abstraction ceiling).
Most people are correct that they lack the intelligence / mind for a lot of hard math (even epsilon-delta proofs are enough to eliminate the majority of the population, no matter how good a teacher you are, and these are just basic undergrad calc).
And yeah, sure, people have different kinds of intelligence and such, but there is still a g-factor, and people of low intelligence almost universally can't do hard math, whereas most people who can do e.g. advanced undergrad math can generally do almost all other advanced undergrad fields reasonably well. The world isn't fair here.
I would even go as far as saying that mental conditioning and training is also required, on top of mental capabilities.
Eh. I'm a math PhD who fled academia because it was too much for me. But I have never encountered this term "abstraction ceiling" nor did I succumb to it. I simply ran out of motivation to pursue higher math, especially when following through on learning and research became more and more labor. (It was always labor; but it was a labor I used to love.) I am far from a prodigy.
Disagree. It's a notoriously hard subject to teach, and with all the demands placed on e-d in so little time in your average curriculum, it doesn't require appeals to IQ to explain its infamy. With enough motivation and practice, the quantifier alternation is comprehensible to any sound mind. What your average mind (and student) lacks is exposure to formalism, abstraction, and how these things tie in with what they are familiar with, which is symbolic manipulation. With the exception of geometric proofs (another educational bugbear), they have little context for what formalism is or why it matters.
This sounds a lot like you may have in fact succumbed to your abstraction ceiling, because in practice, the ceiling manifests as not as it being impossible for you to learn something, but that it would take you years and inordinate effort to master what you notice others mastering easily in just a fraction of the time. You may have not heard the exact term (comes from Douglas Hofstadter), and you may be talking about just the academic busywork, but I find it hard to believe you never encountered discussions about this kind of stuff. I would also politely suggest that unless you are Terry Tao posting under some kind of alt, you most certainly do have an abstraction ceiling (or your own mathematical limits) too.
The latter statement is obviously false, but regardless, intelligence explains some of the difficulty, and much other difficulties far more parsimoniously than "everyone could just learn any math if they just tried hard enough and had good enough teachers". E-d is merely an obvious and generally familiar example, and nothing I said really relies on this very specific aspect of maths, obviously. We also shouldn't pretend your (almost certainly false) view of math and intelligence isn't also often harmful to struggling students in its own way.
Spoiler: this is also why mathematicians hate vibe-math. AIs are outright terrible explainers even when they do have a watertight logical argument—and honestly, this is the load-bearing seam.
It goes beyond "proof vs. exposition": the logical derivations AI comes up with fail to even qualify as human-directed proof because of how terrible they are (far below even the most novice mathematician doing their roughest work) at the exposition part.
I think this only applies to cutting edge mathematics (novel proofs of hard problems). I have seen it reported more than once that such AI proofs are cumbersome to follow.
But in my experience, when it comes to explaining well-established math that is already in the training data, AIs can be very good teachers (at least with recent models). Especially if you use it along with a textbook and ask it about anything that might not be explained well in the textbook.
Gemini's explanations are very good.
Similarly, programming is also a precise language of communication. Initially, we focused on direct machine behavior but every abstraction above the hardware (including assembly) has been to make that behavior legible to humans.
Developed notations and shared procedural abstractions have made thinking about computation more intentionally human and source control has established a protocol for conversing with other humans in the language of a program and changes to that program.
The moment just now feels like a neglecting of the idea of communication being central. If the program is a compile target but not sufficiently legible or if the conversation moves too quickly for us to keep up then we retain the effects of computation but loose its meaning as communication. We loose the understanding and the ability to develop and evolve further shared abstractions.
Open source programs could be more like motivated explanations of computation. For open source to survive, maybe we should start to make the distinction between free product distribution and programming as communication and community building.
It is already that. Every time a method/function is created, a structure is defined, a variable is added, a file is created or renamed,… It’s all for the purpose of human communication. The computer only need binary in a single file.
But people feels like they should be able to jumpninto curl code without any understanding of networking, or linux code with no knowlede of computer architecture. Few code are meant for total beginners.
As a math prof, I care(d) much more about proof than intuition, not because proof is more important, but exactly because intuition is (I'm a bit Chesterton-ish here haha). You cannot do proof without intuition hence, if you emphasize proof, intuition will take care of itself. Whereas if you emphasize intuition, students won't have any idea of what a rigorous proof should be.
Even if we can proof/disproof any statement in Math (not possible due to halting problem), Human still need to decide which statement to be called "theorem".
The theorem thing is invented by human to help other people better understand Math structure in a easier way.
Interesting headline.
It's interesting because, as far as I'm aware, the vast majority of people already believe that math is more than proof. A slightly smaller but still very large majority don't even include proofs in their mental concept of what math involves.
Technically, the largest majority are the people who go: "What are proofs?" :P
A majority? I doubt it, simply because the majority doesn't know what math is at all.
At university level introductory calculus, the person teaching class had to reassure students that math wasn't entirely arithmetic or adding up numbers. He did this because it's a common misunderstanding.
So, you disagree with my comment because you think I'm right?
Those students he was reassuring, did they think math was nothing but proofs?
Haha, sort of. I guess I disagree with your claim the majority of people think math is "more" than proof. The majority of people think it's less: they think it's doing high school arithmetic. Most people don't know what a proof or a theorem are. They think math is doing calculations with numbers.
Mr. Tao is an excellent politician. Lots of awards and texts, yet no major problem solved.
It seems now that NS is solved he is mobilizing the community to convince taxpayers continue to pay even though AI may do a better job in his work.
Also, his opinion of AI has continually changed in the past years, after the capabilities were demonstrated.
Gr8 b8 m8
Ignoring the other ridiculous parts of your comment, isn't this exactly what you're supposed to do? Update your beliefs according to the newest information available?
Math academia 2025
Math academia 2026
I think people are overblowing this though. Wake me up when GPT-whatever writes gcc from scratch, then by the Curry-Howard I'd be impressed
You missed this from last year
https://github.com/anthropics/claudes-c-compiler
Also I dunno why you should be impressed by this - gcc isn't anything near eg navier stokes
One thing that concerns me from all this is "understanding" is very important to human progress. The fact it took 400 years to crack Fermat's theorem resulted in a lot of "Side Quests". These side quests helped grow other fields (for instance elliptical cryptography). Im concerned with AI that we will loose these side quests.
I do neither maths nor science with AI but in my experience most models are perfectly willing to burn tokens on a ton of sidequests at the earliest opportunity.
Yeah but do you read through and find if one of those side quests is useful?
Yes, why not?
They're often directly applicable: minor bugs, inconsistencies, missing tests, commonly also stuff I already now (like some infra config details).
We'll get innovations in AI as a side effect.
I can’t help but feel a little schadenfreude. STEM folks may soon find themselves masters of skills as esoteric as translating Ancient Greek poetry or analyzing 18th century novels. The ability to construct complex mathematical proofs will become a party trick, rather like the ability to mentally multiply 10 digit numbers. The arguments that STEM snobs dismissed in favor of the study of the humanities will be the very same arguments that they now turn to. We will hear about how math and science make you a better rounded person, have inherent as well as instrumental value, etc. etc.
You don't think LLMs can translate Ancient Greek poetry or analyze 18th century novels?
Of course they can. My point is that mathematicians may increasingly find themselves in the same position as academics in the humanities. Mathematicians themselves will be able to see the inherent value of the work they're doing (just as experts on 18th century novels can in their own field), but it will be far less obvious to society at large why their work should be funded.
Its a reasonable view to take that "human math" [ math residing in human minds ] is the only math that counts.
Math that only resides in the weights of models, or arcane forms such as a long lean proof or even an unread textbook .. is not the math that we should be striving for.
Likewise all other technology [ and culture ].
LLMs and AI / AGI / ASI could lead to a new renaissance of math discussion and expansion of human math and science. Or the opposite, where we outsource all our thinking to the AI, and no new generation of artisans is trained by doing hard problems, and in a generation we have killed off human math.
Likewise all of the fields of human intellect. We need to make sure we protect future generations of doctors, biologists, software developers, architects, engineers, librarians, musicians, artists ...
A moratorium on AI development might be the only way to achieve this preservation of human culture.
I want to agree with this, but I have a hard time seeing how it can be done.
Tao is speaking of a very particular kind of mathematics, that done out of pure curiosity.
But maths, even at the highest levels, often finds applications sooner or later.
It will be economically impossible to justify boycotting correct mathematics that no humans understand on grounds only of purity.
This may happen very soon: one of the obvious applications of novel mathematical results is in building stronger AI models.
Tao isn’t the article author, it’s a guest post.
This gets repeated a lot and seems to be one of the primary stated goals of making AI solve math problems, but I still have no idea by what mechanism this is even supposed to happen. I guess they could make some minor improvements to matrix multiplication algorithms or whatever but I don't see what groundbreaking theorem could possibly significantly improve LLMs.
It's the kind of thing where it's sort of expected that you wouldn't know, right?
I think we don't really understand why deep learning works as well as it does, the thinking around that is, as far as I can tell, mostly a collection of empirical observations.
A fundamental theory of learning that can be used to predict optimal network architectures might enable smaller models that consume less energy.
So many thoughts come to mind at once, they're a jumble in my head rather than a single coherent narrative.
John Henry comes to mind. As does Agent Smith's "I say your civilization because as soon as we started thinking for you, it really became our civilization, which is, of course, what this is all about" monologue in The Matrix. I've not read (or listened to) "With Folded Hands ..." or "The Machine Stops", but I have read the Wikipedia plot summary of both.
Do we want to have comfortable lives, or do we want to serve each other?
"Computer" used to be a profession; I grew up around adults bemoaning that "kids these days can't do mental arithmetic", the Pi Zero I've not switched on for probably a year now could beat all humans simultaneously at that (even if everyone was as good as the current world record holder) and yet we still teach arithmetic in schools.
Nobody needs to knit, and yet we do so for fun. Youtube's "Primitive Technology" channel, which has spent around a decade speechlessly making iron from bacterial slime found in a creek, using only clay and sticks and leaves and vines naturally found next to that creek.
Like I said, no coherent narrative. It's been a while since my stream of consciousness became a river delta; usually at worst it only meanders a bit.
The math field is confronting something that coders have been dealing with for a few years now, only far more violently. Today's moat for software seems to be that AI can automate tasks but not a full job (yet). But for a large proportion of mathematicians, doing these tasks really was _the_ job. It's the bit they wanted to do, and if they completed a sufficiently difficult set of tasks, they got tenure. Now this model is failing, they frantically need to pivot the role of humans to save their profession from funding cuts.
I remember when "writing code was never the point" became a mantra here. There was truth in it, but removing the coding has certainly taken away a lot of the texture of the work and enjoyment of the craft. Many of us feel this loss as we tech-lead teams of agents as our source of income. I am not optimistic the mathematics pivot is going to work, but I'm certain that most will be depressed with the outcome even if they succeed.
We are all staring at the same existential dread, just seeing it unfold slower. We're being told that utopia is to be obsolete, and that is a jarring idea to contend with.
The last days we are served these high goals about understanding, "digestion" and so on.
But if you look at the practice of present mathematics, in the last 20 years it is all about publishing solutions to problems.
There are famous problems to be solved, there is a hierachy of conjectures to be solved. A quick search here on HN gives pearls like "Theory building papers are dime a dozen and don't get published in high tier journals unless they solve a problem".
And all of a sudden it turns out that problem solving can be automatized.
So then what will problem solvers do? Well, from now on they will "digest" problems solved by AI.
In a way or another they will find a way to stay on top.
That's the goal, at least, but mathematics as a living practice does not have much to do with these games of power.
The issue here is not AI--it's academic papermill culture and paywalled journals.
AI gives us greater freedom to "stop and smell the roses", explore hidden structures, etc in mathematics. It is a dream come true for curious minds.
Yes. AI is a useful tool and we are going to adapt and use it.
The phd student will be forced to publish 10 breaktrough articles, the university department which does not offer "free" access to AI (for its members) will see the its ratings going down, when compared with the other universities.
It will be "use AI or perish" for academic management so on the side of academic management the ones with vision will thrive and the ones without will perish.
But what about the publishers? In the last decades the academic research was made into a feeder for publishers. The main goal of a researcher is to write articles, which are later sold back to other researchers.
This economic system is under big stres now, because for a while at least the academic management and publishers will have contradictory goals.
And that is why this scare which is induced by those who profit the most from the present system.
With hammers do we build our mud huts more easily and sit back to rot? Or do we build more complicated structures and do it more quickly?
“You are right. There is nothing in yesterday’s mathematics that you can prove with exterior algebra that could not also be proved without it. Exterior algebra is not meant to prove old facts, it is meant to disclose a new world. Disclosing new worlds is as worthwile a mathematical enterprise as proving old conjectures.” Gian-Carlo Rota in “Indiscrete Thoughts”
If I have to take the risk of simplifying,
1. We humans have managed to take huge amount of information and compress it using a loss function containing some bias we have about the information.
2. We now ask ourselves to decompress the same information with some additional cross-entropy. As a side effect of this process we sometimes spurt out information that may or may not have any meaning since the compression was lossy.
3. Now, we ask ourselves to present this some-what newly decompressed information with brevity in order to understand what we've learned from it.
Knowing that this process is happening on a larger scale, this resurfaces the argument if meaning can be reduced to computation only.
Although some might favor this argument but we are at the risk of anthropomorphizing this process.
The idea presented in the post itself is perspicuous (in Grant Sanderson own words) as he always does.
Taught proofs too, and plenty of students fake intuition with pattern matching.
Part of the controversy here is that now the skill advantage that some Field Medalist had is much narrower. The fact that fields medals have an age limit implies that it favors brain power over understanding. And that was the guiding light award of the community. So i find it "funny" (and natural) when they are offended by AI. That is the main "crisis" of mathematics.
In my opinion there has never been a better time to be a mathematitian, and there has never been a better time to be a software builder.
But there has never been a worst time to have the need to prove your economic value as a mathematitian or software developer alone. Because "understanding" is not something you can prove in one afternoon, its something that you prove with a life.
As an ex-mathematician I assure you this is very wrong, and every working mathematician I know right now is completely miserable, and/or trying to flee the field as fast as possible. It's like telling a chair-maker during the industrial revolution that there had never been a better time for them, since now they could operate chair-making machines instead of toiling away at the wood themselves. It assumes that they were purely in it for their passion for mass-producing chairs. The majority of mathematicians get into the field because they love problem solving, and the gauntlet thrown down by challenging math tasks.
Many parts of this will never be useful for society on a grander scale - but this is reflected in the finances - pure math is closer in funding-terms to a humanity than to hard science. Now even this is _massively_ under threat, and Tao and co need to pivot quickly to stop this from becoming a bloodbath.
Probably true for the dedicated problem solvers (of which Tao is one IMO). But I doubt there's ever been a better time to be a theory builder (more like Peter Scholze, or Grothendieck).
Some up with an idea and leave the system to check it 15 different ways, and see whether you can simplify an existing body of theory. It'd be like having an army of lightning-fast grad students.
I'd even say Scholze is not a great example here. Most of the work he's known for is progression towards the Langlands program - which is very much a problem to be solved, and one I would imagine he'd not be thrilled for an AI to one-shot. I agree that it is somewhat 'up the chain', in the same way that software engineering has not immediately disappeared now that performing coding tasks is largely automatable.
But I also take issue with 'never been a better time' - e.g. is this really the greatest time to be a software engineer? Everyone has AI psychosis and feels like they're a couple of breakthroughs away from being unemployable. The same is even more true in math - we've gone from failing IMO problem 6 last year, to solving NS. The rate of change is formidable, it feels like there may not be many places to hide in a few years.
Im an ex mathematitian too. And if i was in academia I would probably have the same reaction. Thats what i say that its the worst time for proving economic value.
But if you are in for theory building and understanding, then you are not constrained anymore by your motivation to grind through countless hours of formal theorem proving. And you do not need to have superhuman formal manipulation skills and memory.
For me mathematics is not the formal system, so LLMs will never be able to do end to end maths.
Spot on. I agree. There has never been a better time to be a software builder or a mathematician.
Seekers whose primary motive is validation instead of understanding are the ones who are getting paranoid.
Thoroughly enjoyed your thoughts. The age limit is a joke if what you care about is true understanding.
How about we stop moralizing technology so much and start focusing on how we want to spend our time in the real world which now contains it
Hmmh. I like motivated explanations, but, as acknowledged in the text, this is a subjective thing to measure. What is a great motivated explanation for Tao, might be hard to grasp for me. So I guess judging how well an explanation motivates something depends on two things: 1) My way of thinking, and 2) what I already know and how well I recall it in this context.
There is a third thing: how well does the motivation chime with or go against my current belief system? You would think this is not much of an issue in mathematics, but it can be, and I had my fair share of frustrations because of it.
Anyway, all of the above points to one thing: the best motivated explanation will be generated by an AI, knowing the subject and you in a deep way that no other human will, and being able to interact with you during the explanation.
What's an example of your belief system conflicting with a motivated example? I'd love to understand that a bit more.
One example is what currently plays out, see the previous guest post on Tao's page: https://terrytao.wordpress.com/2026/09/12/after-math/
The blog post says that the statement "AI really did solve a problem in mathematics." is wrong. But a formal proof showing that Navier-Stokes equations can blow up is certainly such a solution, by AI. There is not much in this world that is more objective than a formal proof, so any disagreement on this is based on how we see the world. Michael Harris will agree with the statement being wrong, Jacob Tsimerman will not.
Hilbert famously battled Brouwer's view of mathematics. From my point of view, Hilbert was right: intuitionistic logic is certainly interesting; but I like to study it using "normal" (= classical) mathematics.
My personal frustrations are about how hard it is to publish my work on abstraction logic. I would never have thought it is that difficult, mathematics being objective and all. It seems essential to take out as much motivation out of your paper as possible, because it might offend your reviewers and their belief system. By now my papers come with full Isabelle/HOL formalisations, let's see if that helps.
I don't think we're discussing pedagogy. Good _research_ exposition is instead related to communicate your intuition and way of seeing things. The conceptualization of a given situation or problem is what is valuable, how you connect it with other stuff, etc. It is then up to you to memorize and interiorize it.
It would be interesting to see what would happen if we had two competing mathematical institutes, a sort of First/Second Foundations:
1) Rejection of AI for anything but trivial applications while still using computers at their full capacity. Researchers would ensure full human understanding of proofs and methods. This Institute believes on Math as a process of discovery, Mathematicians as explorers/poets/storytellers and not proof machines.
2) Unrestricted, all-embracing use of the latest AI, including potentially research in creating even better AIs as part of the program. These researchers would be okay with not understanding proofs if verified to be correct. This group is focused on rapid problem resolution and believes Mathematicians are theorem creators and provers.
After X years (100?), which one would advance Mathematics and humanity the most (we'd need to define "advance")?
Mathematicians worry about proofs and the intrinsic value of something as elusive as 'understanding'. They are deeply ingrained in the study, deeply concerned with anything effecting the field. Yet they're still emotional beings looking for beauty and meaning in life that might come from an understanding how the universe works purely from a math perspective. I'm glad Mathematicians exist, I certainly can't do that type of work.
And I trust their results: technology wouldn't be possible without advancing our understanding of the world in various fields, including math.
Your idea sounds great for the Mathematicians.
There's a more pragmatic view though, and unrelated to proofs themselves: does understanding a proof help us to advance Humanity in some way?
Do we have better lives afterwards? What if we give up understanding proofs and focus only on results.
In other words, if an AI solves a problem for you, but you don't understand how it works, should you continue building anything on top?
I suppose the results are truly what matter. If AI solved cancer, disease, anything that lowers quality of life, but you have no idea how it did it: is that good enough?
What if there is no true beauty in Math, the way Dirac and Einstein wanted?
I'll answer one of your points partially: if AI builds a better sorting algorithm and proves its performance characteristics, it's useful. I'd be able to use it to make my programs faster even if I don't/couldn't understand it.
It would be a bit disappointing but still useful and make humanity slightly better.
I don't see the point. No one is proposing a complete rejection of AI tools.
Logic is the foundational weapon operating on sentences.
The act of stitching together, a series of sentences as true is what logic is.
If you make the stitching as airtight as possible, congratulations, you are in the realm of math.
If you are stitching together reasonably similiar to how the masses do, congratulations you have common sense.
If you stitch together completely random sentences, you are in the realm of nonsense and you may be classified as a retard.
The weapon is the same. The discipline differs and hence the effort to produce the chain.
So I am not at all worried about LLMs producing math proofs.
Godel with his incompleteness theorem helps one sleep easy. Rest assured no LLM can fly above Godel Incompleteness theorem.
There will always be statements that are true. So yes, it is time to celebrate.
Software is logic applied to intersubjective truth. It's not physical truth which is the subject of the hard scientific fields such as physics and chemistry, as well as biology for the most part.
So no, software is much less than science.
This is really interesting and available here: https://www.youtube.com/watch?v=IbGNZQvobkc