_______ __ _______
| | |.---.-..----.| |--..-----..----. | | |.-----..--.--.--..-----.
| || _ || __|| < | -__|| _| | || -__|| | | ||__ --|
|___|___||___._||____||__|__||_____||__| |__|____||_____||________||_____|
on Gopher (inofficial)
HTML Visit Hacker News on the Web
COMMENT PAGE FOR:
HTML How Terry Tao became an evangelist for AI in math
sylware wrote 1 day ago:
If good mathematicians are able to design ML recipes for maths (may be
field specific), using maths solvers, I wonder what will be the size of
their proofs...
All that to find a path to true or false.
dilawar wrote 1 day ago:
When I was in college, I posted a question on math.se about possibility
of universal gates like NOR and NAND in multi-level logic. Someone
found it interesting and posted it on the mathoverflow in more mathy
language . To my surprise, Terry wrote an answer to that question. I
still don't get it but I was flexing the whole month.
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.
thmorriss wrote 1 day ago:
google wave!!! so good
energy123 wrote 23 hours 56 min ago:
Developed by Terry's older brother at Google
brookst wrote 1 day ago:
Your point is contextualixing the humans involved, and it is a good
and righteous post.
andyferris wrote 1 day ago:
The brilliance of a mathematician like Terry is the the clarity they
can bring.
Thatâs my interpretation of your comment, anyway.
spondyl wrote 1 day ago:
I guess fandom is just in Terry's DNA:
HTML [1]: http://shanghikid.50megs.com/Otakudom/ContReal/contReal.htm
claw-el wrote 1 day ago:
>âOh, what's the unit? Do I care? I'm no fscking physics major!"
lol
ontouchstart wrote 11 hours 53 min ago:
42! [1] (I am fscking physics major! ;-)
HTML [1]: https://live.lean-lang.org/#codez=CYUwZgBAhgdgzgdxAJwgLgLw...
nhgiang wrote 1 day ago:
Thatâs rad
bsoles wrote 1 day ago:
As much as I like Terrence Tao, I think he is entering the crackpot
phase of his career. Much like Roger Penrose and many mathematicians
and physicists before him.
justanotherjoe wrote 1 day ago:
Yeah mathematicians tend to do that. Physicists not so much I think.
However, none of what he says about AI is such a strong prediction,
unlike the 'crackpots' that are probably on your mind.
cryo32 wrote 1 day ago:
As a mathematician who was married to a physicist, I disagree :)
limflick wrote 1 day ago:
That's what all the Physicists tell me.
rowanG077 wrote 1 day ago:
Wild take, without even substantiating it with a single statement.
arjie wrote 2 days ago:
Woah, guys, the article is actually super cool. I almost didn't read
the article because of the AI thing - I follow him on the microblog
networks and I know he's pretty good at using LLMs and so on so that's
not interesting. The unique stuff about him and gowers that it points
out is there idea for massively parallelizable mathematics problem
solving. It's definitely worth a read for how they got the first
Polymath publication and afterwards for how they want to use LLMs et
al. to do this:
> 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!
InkCanon wrote 1 day ago:
The checking has nothing to do with AI, despite the (massively
funded) marketing done to make you think so. It is based on formal
methods/theorem provers.
world2vec wrote 1 day ago:
From what I've seen on Tao's YouTube channel, he does use GitHub
Copilot via VSCode to write Lean4 code.
dellamonica wrote 1 day ago:
The point of the AI with respect to checking is to translate a
natural language theorem and its proof into the formal system. Most
of known math is not formalized because it is very hard to do so.
dvt wrote 2 days ago:
I think Terry Tao is a great litmus test for AI zealotry (both pro- and
anti-). Just in this thread, we have people twisting themselves into
knots about how he "sold out" or "not doing math the right way" or
whatever. To him, AI is a tool, like any other.
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.
pcrh wrote 1 day ago:
I enjoyed the article. I'm not a mathematician, but I did notice one
aspect: even with his enthusiasm for AI, Tao effectively showed that
for the uses he describes, AI can currently only handle small chunks
of a mathematical problem at a time. Humans, or non-LLM approaches
are still needed to stitch these together.
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!
keybored wrote 2 days ago:
> I think Terry Tao is a great litmus test for AI zealotry (both pro-
and anti-). Just in this thread, we have people twisting themselves
into knots about how he "sold out" or "not doing math the right way"
or whatever. To him, AI is a tool, like any other.
Thatâs an Anti example. Whatâs a Pro example?
dvt wrote 2 days ago:
We've been flooded with "AGI is 6 months away!" for a few years
now, mostly by Anthropic/OAI/XAI, which is clearly nonsensical
hype. Also, almost everyone has been walking back their previous
claims that "AI will replace ~80% of white-collar jobs."
bayarearefugee wrote 1 day ago:
> Also, almost everyone has been walking back their previous
claims that "AI will replace ~80% of white-collar jobs."
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.
keybored wrote 1 day ago:
Cool. Thatâs a new FUD line.
menaerus wrote 1 day ago:
In the last decade or so I have never seen so much layoffs across
the industry. This may be suggesting that evidence supporting the
latter hypothesis is not maybe too far fetched.
internet_points wrote 1 day ago:
[1] suggests AI is used as an excuse rather than being a real
reason.
HTML [1]: https://www.normaltech.ai/i/201537309/the-stories-of-a...
breezybottom wrote 1 day ago:
Ok what's the practical difference? The layoffs are still
happening.
internet_points wrote 1 day ago:
If "the latter hypothesis" of parent commenter was that "AI
will replace ~80% of white-collar jobs", then that
hypothesis clearly not supported by the current layoffs. AI
isn't replacing workers, AI just happens to be an easy
excuse for it. Could as well have been "COVID" or "tariffs"
or "the economy" or "the end of Zero interest-rate policy"
menaerus wrote 1 day ago:
Why not? I have literally got several first hand examples
where people are fired because of how good the AI models
became. Why do you find that questionable?
internet_points wrote 1 day ago:
Intriguing. You should notify Narayanan and Kapoor so
they can update their post with your counter-example :)
dvt wrote 1 day ago:
In the last decade, the software engineering industry has
turned into a grift that has pushed out hundreds of thousand of
low-quality "engineers" through coding bootcamps or online
courses. Many of these people have no passion for the craft or
interest in building products.
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.
menaerus wrote 1 day ago:
Over-hiring could be one way of explaining the effect we are
seeing, however, where are those "coding bootcamp" or "online
courses" engineers? I honestly ask because I have never
worked with one in almost 2 decades of being in the industry,
and I worked across many different domains. What I see is on
the contrary - the people who are getting laid off are people
with legit engineering degrees from legit engineering
Universities.
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.
witx wrote 1 day ago:
Where I'm from and peripheral countries, the industry is
riddled with bootcampers and button pushers. My company
even has a big bootcamp for reconversions
menaerus wrote 1 day ago:
What are you trying to suggest? That people without the
University degree who have been trained for monkey coding
do exist? Sure but that's not what I was saying nor does
it skew the picture in any significant way.
witx wrote 1 day ago:
What I'm trying to convey and you fail to understand is
the picture you have in your mind is very much affected
by your reality. The fact that you don't see these
bootcampers doesn't mean they don't exist.
menaerus wrote 1 day ago:
Not only you don't have a depth of thinking
critically, and understanding my point, but you're
also unbelievably arrogant.
witx wrote 1 day ago:
The only thing I did was to point out that
anedoctal data doesnt give you the full picture.
Why the insults though?
keybored wrote 1 day ago:
Do we have to rehash CEO statements about causality versus
objective reality yet again?
menaerus wrote 1 day ago:
Objective reality is that many people have lost and are still
loosing their jobs. If you don't have anything useful to add
to your response please refrain from polluting the
discussion.
keybored wrote 1 day ago:
Likewise with your "may be suggesting" unfounded
correlation speculation.
But I guess Iâm not allowed to answer on the subthread
that I started.
menaerus wrote 1 day ago:
No, it is not the same at all. I intentionally frame my
words by saying that after all there may be an indication
that such an event or correlation exists but I am
explicitly not stating anything, therefore it is rather
an invitation for discussion and not one-sided talk.
jplusequalt wrote 2 days ago:
A smart phone was just a tool at first, but over time society has
become overly depedent on them. Most of us are now addicted to our
smart phones in one way or another, and that has consequences that
play out across society as a whole.
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.
dvt wrote 2 days ago:
> pushed for by the same fucking people who caused our societies
smartphone addiction
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.
witx wrote 1 day ago:
These fking website sure loves to pull statistics out of the rear
end
breezybottom wrote 1 day ago:
That's an extremely broad statement to make "assuredly". I'd
wager you haven't figured environmental consequences into your
calculation. All the toxic waste from production is being routed
to the developing world.
ekjhgkejhgk wrote 1 day ago:
I'm not the person you were responding to, but I could've written
the same as they did, so here's my reply:
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.
pera wrote 2 days ago:
As a person from the developing world I feel obligated to say
that I find your assurance quite unconvincing: the negative
effects of smartphone at this point in time is invariant
globally, and whether they are a net positive or negative is at
least debatable.
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.
ForgotIdAgain wrote 2 days ago:
I come from a developping country, and this whole schtick about
"being concerned by tech addiction is a western luxury" is
tiring.
jplusequalt wrote 2 days ago:
>But 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.
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.
bit-anarchist wrote 2 days ago:
> 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.
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.
aleph_minus_one wrote 1 day ago:
> 1. smartphones are extremely useful (being miniature
computers and all);
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.
bit-anarchist wrote 1 day ago:
> Whether they are extremely useful or just some tool that
has its uses depends a lot on your lifestyle.
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.
jplusequalt wrote 2 days ago:
>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.
No, my post is decidedly not that. I'm saying maybe we should
stop and think about the consequences and plan accordingly.
bit-anarchist wrote 1 day ago:
My bad, then. If I may suggest something, give a small
acknowledgement and avoid words such as "cancer", which is
pretty loaded.
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.
2snakes wrote 2 days ago:
Social constructivism is tougher and tougher than âjust
tools.â Could the so-called âaddictivenessâ consist
partly of the many other devices smartphones replaced? Sure,
some attention economy but also just turn off the data?
pvillano wrote 2 days ago:
I really look forward to the day AI-driven algorithm design + formal
verification becomes the norm for performance critical computing.
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.
xg15 wrote 11 hours 20 min ago:
...and no human will be able to understand the algorithm either.
dyauspitr wrote 15 hours 45 min ago:
> A programmer translates a natural-language spec into a
machine-readable spec
Why do we need a human for this?
whattheheckheck wrote 19 hours 46 min ago:
How would you even be able to recognize the proof is valid? Or its
own proof that it understands its own proof....
This ain't the future
kccqzy wrote 1 day ago:
You can look forward to that, but today Iâm already experiencing
something worse but close enough for all but the most critical code:
AI-driven algorithm design + tests in your favorite property-based
testing library (like OG QuickCheck in Haskell or hypothesis in
Python).
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.
xpct wrote 1 day ago:
I'm sure a system that could do this is economically optimal.
Why are you looking forward to this, though?
AndrewKemendo wrote 1 day ago:
Not the OP but for me itâs:
more optimized than any human could ever hope to write, along with
a lean proof of its correctness.
jplusequalt wrote 2 days ago:
>A programmer
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.
CuriouslyC wrote 2 days ago:
The architect/accountant won't be doing it either, they'll just be
a liability lightning rod for people who are closer to devs than
architects doing the actual day to day work. Sort of like a doctor
will "manage" a team of nurse practitioners.
whattheheckheck wrote 19 hours 47 min ago:
Except medicine is 1000x older than software engineering as a
field
gosub100 wrote 2 days ago:
I have a tangent question: is there a formal language definition of
mathematical grammar the same way there is for a programming language?
If so, is it context sensitive or context free?
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.
317070 wrote 1 day ago:
Yes, people are using the programming language Lean for that, and
there are a few less popular alternatives as well.
Fundamentally, there is a one-to-one correspondence between
mathematical proofs and programming. Proofs are isomorphic to type
checking.
HTML [1]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
gosub100 wrote 1 day ago:
Thank you for this.
brcmthrowaway wrote 2 days ago:
It seems Cameron Zwarich has also joined OpenAI
Is there a Lean/OpenAI connection?
saagarjha wrote 1 day ago:
Where did you see that?
YeGoblynQueenne wrote 2 days ago:
I should really know better than to say something like that for a
figure as revered as Terry Tao, but, he has taken OpenAI's money to
shoot an advert for them [1] and, sorry but I can't believe he is
entirely unbiased; or very unbiased for that.
_____________________
HTML [1]: https://youtu.be/cdflu9ZXZGE?si=f1xi65r7kZM8s1JI
lupire wrote 1 day ago:
Do you have any evidence that he took their money?
fxwin wrote 1 day ago:
I think it helps his credibility that he has been working with and
speaking positively about AI assisted mathematics (especially for
formalizing proofs) for over a year now . I'm sure he isn't unbiased,
but as far as spokespeople in the AI space are concerned I'd count
him among the less biased ones.
simianwords wrote 2 days ago:
"Tao has sold out to the AI grifters to prop up the AI hype bubble"
is not a take I expected to see.
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.
CamperBob2 wrote 1 day ago:
Historically it's a little irregular for someone like that to get
involved commercially at this level, but the unfortunate reality is
that academic research at all levels is facing a drastic loss of
funding and political support right now. They are going to have to
do some things that they haven't had to do before, just to survive.
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.
YeGoblynQueenne wrote 1 day ago:
>> "Tao has sold out to the AI grifters to prop up the AI hype
bubble" is not a take I expected to see.
To clarify there was nothing like that in my comment above.
keybored wrote 2 days ago:
We donât even need to know addition to understand quid pro quo.
(edit Okay we may have to understand both plus and minus here. But
thatâs it.)
chipdale wrote 1 day ago:
Terry has always been curious & temperedly bullish on LLMs long
before OpenAI gave him any money.
Quid pro quo or not, he got paid to say what he's already been
saying for the last few years.
discreteevent wrote 1 day ago:
This could be true but, no matter what, a streetwise person
would never trust him after he has taken the money. If he
wanted his opinion on AI to be trusted then he should have made
his money some other way.
pfdietz wrote 1 day ago:
Character assassination is not a replacement for a good
argument. But hey, I'm sure you get a rush from that sense
of righteousness.
keybored wrote 1 day ago:
They stated a completely general principle of trust, not
tied to any person or character trait. Thatâs not
character assassination.
discreteevent wrote 1 day ago:
The "good" argument is that people trust other people's
opinion more who have not been paid to advertise. I trust
the doctor who personally recommends a drug more than the
doctor who was paid to recommend the drug - even if they
recommended the drug before they were paid. That's a fact
of life, it's not "character assassination". Tao didn't do
anything wrong by making an ad but he can't expect people
to take his opinion seriously after someone gave him a lot
of money to state an opinion that favors them.
pfdietz wrote 1 day ago:
It's proper to suspect arguments that are motivated by
self-interest. The stronger that self-interest, the more
one should suspect the argument. This is what you're
saying?
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.
keybored wrote 12 hours 52 min ago:
The billionaires shall inherit the Earth, for they are
minimally of want and need, only merely aspiring for
more accumulation of wealth as a sport.
pfdietz wrote 9 hours 48 min ago:
Or, we can judge what they say by the merits rather
than hypocritically applying ad hominem arguments to
them and not to others.
brookst wrote 1 day ago:
I donât know that Terry much cares about the opinions
of people who judge claims based on innuendo and cynicism
rather than the actual merits of the claim.
pfortuny wrote 2 days ago:
I do not know about this but, to be honest, he (or his Dpt, or
whatever) has the money and connections to try the
hidden-behind-closed-doors stuff.
We mere mortals (I am a prof. of Maths at Uni) do not.
fn-mote wrote 2 days ago:
I wonât downvote this thread but ⦠the first paragraph of the
article explains how Tao won some $3m award. Unless the going rate
for AI-shilling is much higher than I can believe, the amount of
money just is not going to be enough to get a world-class figure to
suddenly sell out. If you saw him selling his morals regularly in
the past, ok Iâll listen to the evidence. But suddenly now? After
so long writing (essentially for free) and building community?
Doesnât make sense.
YeGoblynQueenne wrote 1 day ago:
Thanks for not downvoting the thread I guess, but I don't think
that's how it works. If you take someone's money to say their
product is great, even if you genuinely believe it, you shouldn't
be trusted. There is such a thing as conflicts of interest after
all and it is not measured by the amount of interest; not least
because it's hard to know what that means. It suffices that there
is interest.
alfiedotwtf wrote 1 day ago:
Maybe heâs just friggen excited about the possibilities. Iâm
a developer by day, and even with the pending doom of our whole
craft, IâM EXCITED about what AI not only has already done for
me but what Iâm going to be able to do with it in the future.
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.
rowanG077 wrote 1 day ago:
This is my view as well. It's not like it's weird for people to
get paid for things they genuinely believe in even if they were
nor paid.
pfortuny wrote 1 day ago:
No, I am not saying he has sold out: but he has the money and the
contacts to see the insider-only version.
Just that. Tell my Uni to pay me 200â¬/month for tokens. They
are just going to laugh it out.
nilkn wrote 2 days ago:
I don't think Terence Tao sold out. However, just looking at it
from OpenAI's perspective, this kind of advertising is almost
certainly worth at least one order of magnitude more than $3M to
the company.
Quarrel wrote 1 day ago:
I'm a Terence Tao fan, but yes, OpenAI should at the very least
just be telling him to go crazy with the latest models on our
dime.
fragmede wrote 2 days ago:
A $100,000 investment into Anthropic or OpenAI a few years ago
would be worth a couple hundred million today, so $3m is ~nothing
in that scheme of things.
cryo32 wrote 2 days ago:
And I thought it was cocaine.
klmarks wrote 2 days ago:
Quantamagazine is essentially Renaissance Fund, which is heavily
invested in AI.
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.
dogmayor wrote 2 days ago:
Do you mean RenTech? Not sure how you'd know they're heavily invested
in anything given the notorious secrecy of the firm. Maybe their
public funds have invested in AI, but their most recent 13F shows a
23% tech sector allocation, and their public funds are maybe only
half of their total AUM.
Regardless, doubting the legitimacy of Quanta bc it's a Simons
Foundation initiative is foolish.
YeGoblynQueenne wrote 2 days ago:
Ahem. Define "Pre-AI". Automated theorem proving has been an AI task
right from the very beginning with Simon and Newell's Logic Theorist,
presented at the Dartmouth workshop in 1956.
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 ( [1] ) and which appears, under the same
2.53 number, on page 112 of the 1910 CUP Edition, according to the
digitalization on wikibooks ( [2] )). 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] [3] 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.
HTML [1]: https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_M...
HTML [2]: https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Pri...
HTML [3]: https://en.wikipedia.org/wiki/Logic_Theorist#History
lioeters wrote 2 days ago:
Automath is also an early example.
> 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.
TimorousBestie wrote 2 days ago:
Tao doesnât seem to have been all that corrupted by the AI money.
Heâs signatory to the Leiden Declaration after all.
bmitc wrote 1 day ago:
Doesn't that require you to just click a few buttons? It's not like
it's a binding pledge.
ruilov wrote 2 days ago:
the smartest people see AI as an incredible tool that enhances their
productivity.
bawis wrote 1 day ago:
The smartest people *usually* have little idea how *us* mortals can
abuse the GenAI tools, because they are aware of their limitations,
but we aint.
witx wrote 1 day ago:
You went so deep there champ
Jtarii wrote 2 days ago:
There is more to life than productivity.
Nevermark wrote 1 day ago:
Which is why we delegate it!
fasterik wrote 2 days ago:
Productivity is relative to whatever we value. That could be
building things, making art, making scientific discoveries, or
delivering food to people in poverty.
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.)
brookst wrote 1 day ago:
And experiences absolutely benefit from productivity
improvements. AI has helped me plan better trips, find places and
activities I had no idea about, better prepare for weather in
remote destinations.
Itâs said that âproductivityâ is mistakenly connoted as
scoped to work.
big-chungus4 wrote 2 days ago:
Just like me! I like AI because of how smart I am.
bigfishrunning wrote 2 days ago:
I'm suddenly missing the slashdot mod system. +5 funny.
vitriol83 wrote 2 days ago:
mathlib and lean are currently too cumbersome for many researchers to
use in say algebraic geometry, but maybe more suitable for
combinatorics where it has been applied recently.
nylonstrung wrote 5 days ago:
More accurate title would be "Terry Tao Became an Evangelist for Lean"
norir wrote 5 days ago:
Terry Tao is a next level vibe coder: he inspires people to do his vibe
coding for him. As someone with a background in advanced math, though
never even close to Tao's level, I find myself skeptical about this
type of mathematics. I don't personally find it beautiful and it feels
like the line between the profound and the trivial (as in of minimal
importance not difficulty) is blurry. One could argue for pure
mathematics that is of no practical utility but is aesthetically
beautiful, but I struggle to see the beauty in a gargantuan lean proof
constructed by 100 different people. Perhaps this work will lead to
deeper insight about the universe and the human condition, but I catch
a whiff of problem solving for the sake of problem solving untethered
from a deeper sense of purpose and meaning.
mswphd wrote 2 days ago:
the way to interpret the gigantic lean proof is not by inlining each
lemma, looking at all the lines, and thinking "yeah that's a lot".
That's also not the way to read a paper.
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). [1] 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.
HTML [1]: https://teorth.github.io/pfr/blueprint/
hashmap wrote 2 days ago:
> One could argue for pure mathematics that is of no practical
utility
wait what is the math with no utility
12345ieee wrote 2 days ago:
> I struggle to see the beauty in a gargantuan lean proof constructed
by 100 different people
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.
jvvw wrote 2 days ago:
The vast majority of research-level pure mathematics is never going
to get used in science or engineering. Obviously it is hard to
predict what will be useful, but for the type of mathematics that
is unlikely to be, there is a question as to why we care about it,
and that almost has to come down to beauty in some sense - some
mathematics gives us a new lens to look at parts of the
mathematical world and others chip away at problems in more mundane
ways in the hope that they inspire or contribute to new parts of
mathematics that are beautiful.
alasr wrote 2 days ago:
> Why does it need to be beautiful?
"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)?
layer8 wrote 2 days ago:
You want to understand why itâs true, and that often correlates
with beauty.
simianwords wrote 2 days ago:
How is this relevant here? AI helps you understand the why -- it
literally discovers the proof and hands it to you with
explanations. It hands you the proof that you would have
otherwise not found easily.
layer8 wrote 2 days ago:
If the proof is hundreds or thousands of lines of Lean, itâs
not clear that the AI will be able to provide an insightful
âwhyâ, instead of just dozens of microsteps.
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.
simianwords wrote 1 day ago:
I don't know how you think it only gives you Lean - it gives
you everything including the explanation. You can actually
ask it explanation using you know.. natural language.
> 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!
slopinthebag wrote 2 days ago:
> Why does it need to be beautiful?
âBeauty will save the worldâ
pfortuny wrote 2 days ago:
Much (most?) of math consists in transmission of it (according to
Thurston [1]), a 1000-page proof with no possibility of
transmission is mostly useless. The proof of Fermat's last Theorem
is important in itself, and adds much more than the mere result.
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.
HTML [1]: https://www.ams.org/journals/bull/1994-30-02/S0273-0979-19...
nilkn wrote 2 days ago:
An inscrutable 1000-page Lean proof may have low transmissibility
amongst humans, yet extremely high transmissibility amongst AI
mathematicians.
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.
pfortuny wrote 1 day ago:
Mathematics is a language for humans, not just for machines. We
may agree to let machines "do their thing" for as long as they
want but to what purpose? Just creating "results"? What is a
mathematical result by itself?
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.
nilkn wrote 1 day ago:
I'm not sure why we would assume that AI-generated or
AI-assisted mathematics would never amount to anything useful
in the real world. I would expect the opposite: the
usefulness and explanatory power of mathematics has been
riding an exponential over the last several centuries.
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).
simianwords wrote 2 days ago:
You are mixing a lot of categories here -- beauty, verbosity,
utility, elegance, insights.
Why all that when you just need one thing: truth.
cman1444 wrote 2 days ago:
What is the difference between "beauty" and "elegance" of a
proof?
pfortuny wrote 2 days ago:
"Beauty" is something I cannot define. "Elegance", as I use it,
is the use of tools as precisely as possible. It is a technical
term, whereas "beauty" I cannot define.
Of course, that is my view of it.
breezybottom wrote 1 day ago:
Maybe English isn't your first language, but these are
basically synonyms.
witx wrote 1 day ago:
Maybe English is also not your first language, because they
are not synonyms
cman1444 wrote 1 day ago:
HTML [1]: https://www.merriam-webster.com/thesaurus/beauty
menaerus wrote 1 day ago:
When writing code I also believed in the "beauty" and
"elegance" because IMO it opens up all kinds of different
opportunities that involve using or organically growing or
improving that code. It turns out that if it doesn't solve a
quantifiable problem, (mostly) nobody cares. And the pace of
innovating in the field outgrows the pace (by a large) of
keeping things "beautiful and elegant".
bwestergard wrote 2 days ago:
Why prove the Pythagorean theorem rather than just prove 3^2 + 4^2
= 5^2?
For any practical application, you are only interested in finite
set of concrete identities, so anything beyond that is surplus to
requirements, surely?
SJC_Hacker wrote 1 day ago:
The cardinality of that âfinite setâ could end up larger than
say, the number of particles in the entire universe
SiempreViernes wrote 2 days ago:
You meant this as satire, right?
fn-mote wrote 2 days ago:
The current commentators are surely missing the fact that this
comment is sarcastic.
moregrist wrote 2 days ago:
> For any practical application, you are only interested in
finite set of concrete identities
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.
spacemanspiffii wrote 2 days ago:
I think you may be interested in more abstract things. In this
case, let's say you're creating a program for a 3D printed thing,
and you have to fit a diagonal cardboard in a rectangular box,
you'd like to be sure that the Pythagorean theorem holds even in
cases where you haven't tried it out.
zerobees wrote 2 days ago:
Outside of some niche specializations like cryptography, math isn't
practiced because of "consequences". Most mathematicians take pride
in their work not having any obvious practical applications.
They're also overwhelmingly working in university settings where
they're not expected to generate revenue or deliver practical
results.
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.
chermi wrote 2 days ago:
Most mathematicians don't take pride in their results having no
applications. That's just not true. Maybe some quirky pure
logicians or something. But otherwise 90%+* of mathematicians I
know would be at least satisfied if not thrilled for their work
to be used by others.
*Completely made up statistic.
limflick wrote 1 day ago:
I've had the opposite experience with all the math nerds that I
know. End of the day it's all anecdotal ig
HTML [1]: https://en.wikipedia.org/wiki/A_Mathematician%27s_Apol...
bigmadshoe wrote 2 days ago:
You put it perfectly. And all these AI math startups don't
actually care about mathematics. They are just using it as a
proxy for general reasoning, with the VC pitch being some kind of
world domination after they crack these problems.
setopt wrote 2 days ago:
Are you sure thatâs «most» mathematicians?
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?
jubilanti wrote 2 days ago:
"Applied Math" and "Statistics" are distinct fields from
"Mathematics," not subfields of it. People in those two
departments are often closer to Computer Science or the
statistics subfield in a domain science field (e.g.
biostatistics, econometrics) than to Mathematics in terms of
what they actually teach and research.
setopt wrote 1 day ago:
That is perhaps fair, is that distinction common
internationally?
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.
empath75 wrote 2 days ago:
I think what people find beautiful in math is largely something that
enables the mathematics (or physics) to be translated to something
that they can think about intuitively, and what people can handle in
an intuitive way is largely an artifact of what the brain evolved to
be able to think about "naturally". But it's quite possible that
most things that are true about the universe or math are just ugly
and unintuitive, and the pursuit of truth shouldn't necessarily be
limited by what people can easily reason about and hold in their
heads.
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.
zem wrote 5 days ago:
the analogy with experimental physics is a good one - being sure
something is true is a good first step to developing an elegant proof
of its truth.
throwaway67678 wrote 5 days ago:
Arguments about beauty don't lead anywhere constructive because they
are too observer- and context-dependent. Poincaré himself was
decrying continuous non-differentiable functions as abominations. The
monster group is, well, just like that. What feels intellectually
ugly for one generation is natural for the next, and the field moves
on
zerobees wrote 2 days ago:
> Arguments about beauty don't lead anywhere constructive because
they are too observer- and context-dependent.
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.
threethirtytwo wrote 2 days ago:
Agreed, mathematics is ugly without ai. I feel beauty is in massive
complexity and intricacy. Every time I see a small proof it feels
too easy and trivial. Triviality and simplicity is ugly to me.
potbelly83 wrote 5 days ago:
That's not what op is arguing. To use your example, coming up with
singular examples of continuous non-differentiable functions is an
example of "ugly" mathematics, whereas putting them into a nice
framework where they can be analyzed as a whole (i.e. functional
analysis, density of such functions, etc...) is an example "elegant
and insightful" mathematics. The same with the monster group, on
its own maybe nothing special, but then you have the connections
with other branches of math. Tao seems so focused on the individual
problems and not their connections/generalizations.
throwaway67678 wrote 5 days ago:
Well one does have to come up with continuous non-differentiable
functions to begin with, right? Weierstrass had to shock the
community with his weird series that's almost everywhere
nondifferentiable before people could conceive of a nice
framework that includes them. People do not invent whole
encompassing abstractions out of nowhere
potbelly83 wrote 5 days ago:
Great point, I think the argument you could make about Tao
(fairly or unfairly) is he never tries to build that framework.
Ygg2 wrote 5 days ago:
According to legends Pythagoreans tried to surpress existence of
irrational numbers because they couldn't be expressed as ratio of
natural numbers
Supposedly even drowned their member that divulged their existence.
DIR <- back to front page