NHacker Next
- new
- past
- show
- ask
- show
- jobs
- submit
login
▲How Terry Tao became an evangelist for AI in math (self.__VINEXT_RSC_CHUNKS__=self.__VINEXT_RSC_CHUNKS__||[];self.__VINEXT_RSC_CHUNKS__.push("2:I[\"aadde9aaef29\",[],\"default\",1]\n3:I[\"6e873226e03b\",[],\"Children\",1]\n5:I[\"bc2946a341c8\",[],\"LayoutSegmentProvider\",1]\n6:I[\"6e873226e03b\",[],\"Slot\",1]\n7:I[\"3506b3d116f7\",[],\"ErrorBoundary\",1]\n8:I[\"a9bbde40cf2d\",[],\"default\",1]\n9:I[\"3506b3d116f7\",[],\"NotFoundBoundary\",1]\na:\"$Sreact.suspense\"\n:HL[\"/assets/index-BLEkI_5r.css\",\"style\"]\n")="noopener noreferrer nofollow" target="_blank">quantamagazine.org)
Rendered at 02:55:08 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
Terry also took time to respond to comments I posted on his blog and on his google wave posts (I am old). Most of them were incredibly stupid but he took time to respond. Imagine a field medalist responding to a wannabe kid living somewhere in India.
Some of his real analysis notes were published in India that were cheaply available. I learnt about open/close set and convergence/cauchy series from it. I never thought I'd enjoy reading pure mathematics. Another mathematician I found very readable Daniel Spielman (I think it was his notes on smooth analysis). I once picked a book by William Tutte from the library! Never seen a book that was harder to read.
I don't know what the point of my post is.
That’s my interpretation of your comment, anyway.
> He predicted that in the future, instead of working alone or in small teams of two or three, mathematicians might work on projects with hundreds of other people at a time. And when these collaborations were over, he said — in his modest, understated way — the results might be checked not by human referees but by computers.
Fascinating stuff. My thought has always been that the AI will accelerate individuals and we'll get something like the economy for music or sports (the top few take almost all the revenue) but this may seem like an alternative pathway that might well develop (if only in Mathematics there) where AI systems drop the coordination cost to near zero by making checking cheap.
So far, and I am not foolish enough to say forever, agents are great at operating in the space of checkables and it's hard to get uniqueness out of them (I haven't succeeded in getting a real laugh from Fable) but perhaps there's a whole class of problems that we can now solve by turning humans into the search units. I love it!
lol
https://live.lean-lang.org/#codez=CYUwZgBAhgdgzgdxAJwgLgLwQC...
(I am fscking physics major! ;-)
A programmer translates a natural-language spec into a machine-readable spec, feeds it to an AI-assisted compiler, and out pops an implementation that's more optimized than any human could ever hope to write, along with a lean proof of its correctness.
It won't be a programmer doing this work, because they will have gone the way of the dodo.
It'll be workers specific to a certain domain (e.g. engineer, architect, accountant) doing this on top of their usual work.
The software industry will collapse.
Of course problems remain in both approaches: a human or AI needs to make sure the lean proof is proving the correct translation from natural language spec to a formal theorem, or the PBT is testing the right properties translated from natural language.
And PBT is so close to language level invariants/preconditions/post-conditions that I dream of
A lean proof is a sequence of instructions that starts with a list of facts, and combines them into new facts until a target fact is produced. Each instruction in the sequence is one of a few allowed tactics provided by lean that always produce correct facts from correct facts.
IF (1) you agree with the starting facts, (2) you are sure the target fact is what you're actually trying to prove and (3) the lean compiler says "yep, this is a valid sequence of instructions" THEN you can be sure the target fact is true.
You can be sure the final fact is true, even if you don't understand all the steps, because it's written in lean, and lean only allows steps that are free from omissions or errors
Why do we need a human for this?
Why are you looking forward to this, though?
more optimized than any human could ever hope to write, along with a lean proof of its correctness.
Deepmind is saying people are learning from the algorithms AlphaEvolve is generating. They say the programs tend to be short.
So maybe we will understand the algorithms
_____________________
[1] https://youtu.be/cdflu9ZXZGE?si=f1xi65r7kZM8s1JI
We mere mortals (I am a prof. of Maths at Uni) do not.
Just that. Tell my Uni to pay me 200€/month for tokens. They are just going to laugh it out.
Here’s one of the smarted guys who’s walked the earth, and out of his historical peers, he’ll be part of the first generation with big brains AND to have tools to give literal superhuman abilities.
Come on… TT doesn’t care about a little money for a biased plug. He could literally knock on the doors of Renascence Technologies and walk in with a straight face say “give me 1% of the Medallion Fund, I start today, an office with a nice window if possible”. And it would still come off charming like he always is.
I think we can all be a bit grounded and understand reality as we see it -- one of the smartest living mathematicians is using an important invention. Not necessary to believe in any conspiracy theory.
If that means that researchers like Tao have to work as consultants or adjuncts to OpenAI or other model developers, well... that's what the American people voted for when they elected Trump.
To clarify there was nothing like that in my comment above.
Quid pro quo or not, he got paid to say what he's already been saying for the last few years.
In that case, the anti-AI Luddite arguments are maximally impeached, since they are motivated by fear of personal disaster. Tao doesn't need AI to succeed; the Luddites desperately need it to fail. So they are willing to say anything, jumping right to ad hominem arguments when they lack any real substantive rebuttal.
Maybe you value non-tangible, non-durable things like experiences. That's great, but it would be weird to tell someone who's devoted their life to X "there's more to life than X." (Replace X with any of the fields mentioned above.)
It’s said that “productivity” is mistakenly connoted as scoped to work.
I was daydreaming about how someone would model symbolic algebra in computer code, and naively thought it would be easy, but the more I thought about it, it seems to get exponentially (pun intended) more complicated.
Fundamentally, there is a one-to-one correspondence between mathematical proofs and programming. Proofs are isomorphic to type checking.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
All that to find a path to true or false.
From the interviews I've seen with Tao, he's not some AGI maniac, he says things like here's where we can use this tool, here's where it's less likely to be useful. There's a lot of hallucinations, so we need to double check stuff. Most of the stuff the AI produces is nonsense, but there's occasionally a diamond in the rough.
A very tempered attitude, and likely what most sane people are experiencing when using AI.
It perhaps isn't too different from LLMs being able to coherently output short, a few hundred words, pieces of prose, or code, but not being able to assemble them into functional output with constant "nudging".
Happy to be corrected on this!
AI not only provides potential to cause society to become overly dependent on it, but it's being developed by/pushed for by the same fucking people who caused our societies smartphone addiction.
Once you recognize what we've lost already, it's hard to turn off your brain and just compartmentalize this away as a "just a tool". Nothing that is adopted so widely is "just a tool," and thinking of it in those terms eliminates the ability to analyze the potential downstream effects it will cause.
Not sure where you live, but I would guess the West (where we have the luxury to be worried about "smartphone addiction"). I assure you that the net positive of smartphones, especially cheap Androids, have had a significantly more positive effect on society than negative, particularly in the developing world.
And in relation to your first comment, most sane people would agree that "tools" don't exist in isolation - neither come into existence out of nowhere.
This reductionist position of treating extremely complex machines with deep social interactions as a tool like any other is objectively wrong, and I believe the reasons are highly obvious but I can expand on this if you disagree.
My point is that the tool which was meant to augment one particular aspect of life, has metastasized into being a cancer on many other aspects of our lives, and that has downstream consequences on society as a whole.
Keeping this in mind, being a bullish on AI seems foolish.
edit: Perhaps a better thesis for my reservations with rapid technological progress: smart phones were supposed to help us adjust to society, but society instead adjusted to them. AI is positioned to do the same, and we need to ask ourselves what those changes could look like, and if they're for the better, or for the worse.
>where we have the luxury to be worried about "smartphone addiction"
I reject this, and any similar framing that amounts to "because there are other, greater problems at play, worrying about this relatively lesser problem is worthless."
A problem that impacts people is a problem that deserves attention, especially if an absolute terms the number of people impacted are in the tens/hundreds of millions.
This is true of all important tools in history. From computers, to electricity, cars, steam, even agriculture. They reshape society and its practices. This has been documented multiple times. One I can remember on top of my head, but is not limited to, is historical materialism.
From an misesian perspective, this seems fairly obvious:
1. smartphones are extremely useful (being miniature computers and all);
2. people tend to optimize their actions with the best tools available (i.e. smartphones in this case);
3. people will see others using smartphone increasing and will try to leverage that for their own goals, thus further adopting smartphones (even if indirectly);
4. the economy is the sum of human action, so this progressive adoption changes the economy and the culture.
> A problem that impacts people is a problem that deserves attention, especially if an absolute terms the number of people impacted are in the tens/hundreds of millions.
The real issue with your post is that you seem to be trying to fix smartphones addiction by getting rid of phones, ignoring the benefits they brought and the previous problems they fixed.
Also, every problem impacts people.
Whether they are extremely useful or just some tool that has its uses depends a lot on your lifestyle.
> 2. people tend to optimize their actions with the best tools available (i.e. smartphones in this case);
What "best (tools)" means for you, depends a lot on your values. For example, if you value privacy, mobile phones and in particular smartphones are incredibly bad tool choices.
The "useful" then didn't refer to the individual value judgments of all individuals, but the presence of material affordances that a sufficiently big mass of people would find useful. I admit this was not the best wording, but I forgot (and can't find it right now) the formal term that encapsulates the material qualities that others may see usefulness.
> What "best (tools)" means for you, depends a lot on your values. For example, if you value privacy, mobile phones and in particular smartphones are incredibly bad tool choices.
Agreed, but this misses the point. I didn't mean to imply that the value of things are objective (this is a misesian perspective, SToV is implied), but that some people would find smartphones useful, adopting themselves, and that would further expand the opportunities smartphones are useful to others, creating a positive feedback loop.
No, my post is decidedly not that. I'm saying maybe we should stop and think about the consequences and plan accordingly.
Still, people (as in most individuals in the economy) can't simply be stopped, even less so to plan, specially in a free system such as enjoyed by most of the west. That requires a high degree of coordination and coersion that I think only Cuba and NK are currently capable of, slightly. Otherwise, people will just do their own thing, leading to a technological revolution again, given the material means.
A more practical approach is to continuously nudge the direction of change towards a better direction, constantly reevaluating approach, but avoiding having to stop everyone else.
I don't dispute that in aggregate the effect was positive. But I spend more time thinking about things which impact me directly, and I assure you that in my personal life it used to be a problem, and fixing it was an improvement.
That's just nonsense being pushed by social media to convince you to be upset (or ecstatic) about something.
Trying to upgrade the trolling to rational discourse, TT recently opined
https://mathstodon.xyz/@tao/116681024360293007
I do think that ethically, OpenAI and Anthropic, by training their models on the entire corpus of human knowledge, have certainly broken some rules, but these rules were already broken decades ago by Google—unless we really want to start splitting hairs about if indexing + processing is different than training, which is imo a distinction without a difference—, so it's hard to see who to exactly blame. In any case, that cat is out of the bag. (And for the record, I'm technically a stakeholder: I'm part of like two class actions because of a few books I wrote.) But that's neither here nor there.
[1] https://leidendeclaration.ai/#declaration
[2] https://arxiv.org/pdf/2603.24914
Which Tao is more equivocal about as 2 issues higher on his mind are
1. Funding, short and long term (so he is evangelising "at the bequest of" SAIR)
2. Indigestion from generative abundance (this has always been an issue but now even researchers with permanent positions are affected, over and aside of administrative responsibilities )
here he tries to redirect attention from the "harder" problem of attribution to the "softer" problem of digestion
https://mathstodon.xyz/@tao/116590271196962848
With a side effect of asking the tool-builders to reconsider what is "value"
That’s an Anti example. What’s a Pro example?
They started walking those claims back right around the time someone tried to set Sam Altman's house on fire.
Not making those claims anymore doesn't necessarily mean they don't still believe those claims, it is very possible they just realized saying the quiet part out loud was a bad look for them even if it was/is what they believed to be true.
Then, when money was cheap during COVID, companies over-hired unscrupulously. Now, given that markets are cooling off and there's some political, geopolitical, and economic uncertainty, companies are hedging their bets, and laying off is usually the right move, especially as interest rates are going back up.
There are perfectly viable explanations for the situation the industry finds itself in without invoking the AI boogeyman, especially considering that just about every study out there shows that AI use correlates with a fairly modest increase in productivity, and that it won't turn anyone into a "10x engineer" overnight.
Also, over-hiring by the very definition implies a sudden surplus of engineers on the market. I can't quite understand where did these engineers all of the sudden come from? The number of engineers outputted by the Universities YoY is pretty much close to O(1) so I am not convinced to this theory at all and I see it only as a good excuse that companies are making in order to make them look better.
I spoke with my friends few days ago, and one of them runs the company so he asked me on the opinion of the AI frenzy. I gave him my view and by the end of it he told me that he feels uneasy but that he has to let go part of his employees because he simply does not need them anymore - they are literally replaced by the AI model and one or two or N-M engineers operating the model. Yesterday he needed 10 people for the job, today it is 2 or 3 people.
So, I think that the AI has already changed the landscape dramatically, and what we are seeing are not the post-COVID effects.
I didn't counterpoint with a trivial example I just pointed out that where I'm from there are some bootcamp people being layed off. If you don't like someone counter pointing you, sorry that's your problem not mine. I was neither disrespectful or arrogant.
> None of the layoffs taking place do not involve laying off "bootcamp" people.
And how am I the arrogant one here? You're full of absolutes and certainties and get pisssy when someone argues against your point.
The problem I have with your "argument" is that it is unsubstantiated. And I already answered you earlier - it does not matter if such people exist because such people are not majority, unless you would like to support that hypothesis with some fact?
I'm not doxxing myself by sending you news from my country.
> if such people exist because such people are not majority
Which is different from your absolute "there are none" argument.
But I guess I’m not allowed to answer on the subthread that I started.
Why does it need to be beautiful? Once you proved it it's true and you can use its consequences in math, sciences and engineerings.
I am not talking about the supposed "beauty" of a proof (I do not believe in that concept, rather in "elegance", which is not the same), I am talking about the proof itself, and the insights it provides.
[1] https://www.ams.org/journals/bull/1994-30-02/S0273-0979-1994...
Probably AI mathematics needs a specially constructed or trained translation or compression system (likely also an AI system) that helps transmit dense Lean proofs back into human-style thinking. We may even see an entire field develop around creating human-comprehensible compressions of vast formal breakthroughs in mathematics. Such an activity would almost certainly be both art and science -- there's some objectivity in that certain abstractions or definitions inherently cover more ground more efficiently, yet there's also a deep creativity and artistry in finding compressions that are adapted to the specific 3+1D spatiotemporal intuition of the human mind. Perhaps with time this will keep a lot of the originality and creativity of research mathematics alive -- maybe with that work having even more centrality than it does today.
Instead of seeing this all as a loss of beauty in mathematics, I choose to see it as the beginning of a new age, which will bring entirely new problems to solve, yet also accelerate discovery at an exponential rate.
Unless, of course, we are willing to give machines the responsibility of building bridges. Subject on which I do not have a clear opinion yet.
But just hard drives (or whatever) filled with bytes representing strings representing nothing any human will ever understand... I am not for it (as of now). There are much more important problems to solve.
Maybe I didn't do a good job explaining it, but the rest of my prior comment was about connecting AI-generated results back into human-style thinking. Inevitably, in the far future, it's not unreasonable to assume the world will be dominated by synthetic robots controlled by artificial intelligence, and there will indeed be a point where AI builds not just bridges but vast planetary, interplanetary, and space-based infrastructure projects beyond the ability of our current civilization. At that point, mathematics may permanently move beyond the grasp of the human species. You can't teach a dog general relativity. Surely, there are truths in mathematics (and possibly physics) you cannot teach a human. Not to digress, but for me, this kind of threshold is what a term like "superintelligence" means -- the point where an intelligence is discovering truths that cannot be taught back to humans because we're not smart enough. So far, our contact with this kind of intelligence has been limited to one-off, highly specialized cases (like chess) that have little grand implication for civilization, but that won't always be the case.
But, for today and probably at least our lifetime, to make them useful major AI advances in math will need to be "compressed" back into the specific network and "towers" of concepts and abstractions that human minds specifically can understand and intuit about. So I think both directions of formalization are equally important: translating natural language statements (theorems, lemmas, etc.) faithfully into Lean and letting a theorem prover run and decoding a dense Lean proof back into natural language (which, in some ways, is the more creative and open-ended problem -- there is no one right answer).
Have you actually looked at LEAN proofs? They are typically split into small bite size definitions and proofs, making it easy to dive in where you want, and skip what you don't care about, while knowing that you can trust the conclusions.
I personally think that having hundreds of mathematicians working together as a team is a beautiful thing.
Of course, that is my view of it.
Why all that when you just need one thing: truth.
We basically subsidize the practice of mathematics as an art form, and if you try to take the artistry away, you might find that the artists don't want to play along. And I guess you can imagine future robo-math production lines without any human involvement, and then LLMs finding applications for the resulting theorems, but it's not possible today.
At the universities I’ve been to (as a student and now faculty), «applied mathematics» and «statistics» have been the two largest divisions. But perhaps that’s a bias from engineering-heavy universities?
Again, in the universities I’ve been to, «applied math» and «statistics» have generally been placed under the department of mathematics. I myself am a physicist, and consider applied physics, biophysics, etc. to be subfields of physics and not distinct fields of study, but I don’t know what outer physicists think.
*Completely made up statistic.
For any practical application, you are only interested in finite set of concrete identities, so anything beyond that is surplus to requirements, surely?
I do a lot of numerical work in settings where computational efficiency is useful.
In my work, most cases you can do numerically using integration or Monte Carlo sampling or whatever.
It’s slow. It often pays to find a closed-form solution. Even if it’s just a starting point that needs refinement.
To put in terms of the Pythagorean theorem: Proving the Pythagorean theorem gives you a relationship that’s reliable, fast to evaluate, and general. Proving individual tuples gives you none of this.
That doesn’t even touch on how theorems give us a glimpse at deeper structure and truths. Proving a bunch of right-triangle tuples will probably never lead you to the rest of the identities in trig.
"Beauty", IMO, signifies the idea that you're doing `something` for its own the sake where "its own sake" approximate the idea of getting/being closer to (or in proximity of) `something`/`anything`/`someone` you find "beautiful".
> Once you proved it it's true and you can use its consequences in math, sciences and engineerings (sic).
The expression "you can use its consequences in ..." suggests that the action is a "just a means" to "something else". However, not everyone is interested in the idea of "something else"; they're interested in the idea itself (in a broad sense) as that's one of the main reason they got started/involved in the first place.
---
We all do things as "just a means" to "something else". However, there must be an "end" to this chain of "something else"; otherwise, how do you find any "meaning" (or sense of fulfillment) in this whole enterprise (or chain of "something else"s)?
And if it can provide insightful “whys”, that still correlates with beauty then.
Given the slop-like nature of what current generative AI tends to produce, I wouldn’t however count on the latter quite yet.
> And if it can provide insightful “whys”, that still correlates with beauty then.
Yeah it can, you just have to ask it. It has a good interface for it - text! I think you misunderstand how this tech works, its not just spitting out things. It has the understanding also and you can verify it by asking!
“Beauty will save the world”
Supposedly even drowned their member that divulged their existence.
Meh. You can successfully argue that there is no objective anything. It's all just our perception and the emotions we associate with it. We built entire civilizations on subjective notions of good, evil, beauty, and so on. So where do you draw the line between "acceptably subjective" and "too subjective"? And are you sure it's not just a subjective code name for "the thing I don't like"?
Ultimately, people practice mathematics mostly for abstract reasons. It's not a field where you routinely ship products and get rich by meeting market demand. If 99% of contemporary mathematicians don't want to become prompt engineers, there's nothing that makes the transition to AI math inevitable. If not mathematicians, the only party with vested interest in that would be the PR departments of frontier labs.
Beautiful explanations are lovely when they exist, but we shouldn't wait for them if we can also find the truth through an ugly method.
Instead, you proceed in layers of abstraction. For example
1. the main claim may rest on some set of sub-claims, as well as some local (to teh main claim) work to "patch things together"
2. each of those sub-claims themselves may require other sub-claims + local work, etc
These can be collected into a dependency graph. In lean, this is often called a "blueprint". Here is the blueprint for the formalization of the Polynomial Frieman-Rusza conjecture (now a theorem, by Gowers, Green, Manners, and Tao).
https://teorth.github.io/pfr/blueprint/
This layer of abstractions is (roughly) equivalent a different way to format mathematics. You could remove the Lean component (let alone any AI), and create such a dependency graph for a paper. I would argue this is a clearer way to format mathematics (again, ignoring both the formal verification applications of it, as well as AI).
Any mathematics paper intrinsically has a graph such as this underlying it, and tries to make the various linkages in the graph clear via prose. Prose is only so powerful a way to organize things. I'm sure you're familiar with the way early mathematicians would describe various formula (e.g. the quadratic formula) via prose. It is very hard to understand.
Separately from this dependency-graph perspective, you can do things like
1. add formal verification. Now, each component in the dependency graph is verifiable with high confidence (though harder to write and read). This has some benefits and downsides. Harder to write and read is bad. Being able to have high confidence in the veracity of the result is *very* good. It allows larger collaborations in mathematics. Previously, a large collaboration would require all mathematicians to trust eachother to a large extent. This is (practically) difficult.
2. when each component can now be verified to high accuracy, you can now throw AI at it. I won't extoll the virtue of this. There are parts of it that seem interesting, but many "AI for Math" things currently are stil producing unformalized papers (in prose).
Maybe the main thing I'd say is that this type of "graph structure, with each component trusted" is already implicitly what mathematicians do. You write papers that cite other papers etc. Except now, instead of needing to look for status signals to trust papers (or invest personal effort), you can look for another (honestly fairer) signal to trust papers. So there's a sense in which formalization allows for the democratization of mathematics. I do think there's something beautiful about that.
wait what is the math with no utility
This is a clever piece reminding people of Tao's pre-AI Lean efforts. Now, however, Tao and especially Gowers are receiving AI money and have AI positions so they are far from unbiased.
Or maybe they have caught Feynman's "computer disease"? Either way, this is a hype piece.
Logic Theorist soon proved 38 of the first 52 theorems in chapter 2 of the Principia Mathematica. The proof of theorem 2.85 was actually more elegant than the proof produced laboriously by hand by Russell and Whitehead (2026-03-20: What is called here Theorem 2.85 is, in fact, numbered as 2.53 in the page 107 of the 1963 Cambridge University Press edition (https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_M...) and which appears, under the same 2.53 number, on page 112 of the 1910 CUP Edition, according to the digitalization on wikibooks (https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Pri...)). Simon was able to show the new proof to Russell himself who "responded with delight".[17] They attempted to publish the new proof in The Journal of Symbolic Logic, but it was rejected on the grounds that a new proof of an elementary mathematical theorem was not notable, apparently overlooking the fact that one of the authors was a computer program.[18][17]
https://en.wikipedia.org/wiki/Logic_Theorist#History
Maybe some people only understand "AI" to mean "LLMs" but, particularly in maths, LLMs ain't going nowhere without a symbolic solver (or a human mathematician) verifying their output.
> Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness.
Regardless, doubting the legitimacy of Quanta bc it's a Simons Foundation initiative is foolish.
Is there a Lean/OpenAI connection?