Rendered at 16:18:49 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
arjie 19 hours ago [-]
Really enjoyable read. I escaped a career in Mathematics by being sufficiently bad at it that I only have a Masters. Fortunately, I escaped to a field immune to AI: CS and then a software engineering career. Well, not really, but I did get a good 15 years out of it so thank god for that.
About half of my friends are founders of various startups and the rest are executives of and almost all of them have the view that it’s better for everything to be a failure than to be in the “it could make it” category for half a decade or more.
In that way, I am glad I found that it wasn’t for me. I had the curiosity, but not the doggedness to face difficulty (not enough curiosity perhaps?) or the ability to not encounter such difficulty. And fortunately that meant I was never in the “I could make it” category. God bless clear and present boundaries and may the devil take the grey zone.
dhosek 17 hours ago [-]
Yeah, I’m pretty much on a trajectory of building up as much retirement savings as possible before AI completely kills my career. The sweet spot seems to be about three years out. I honestly don’t know how to guide my 12-year-old son who loves math¹ and coding.
⸻
1. Which at his age essentially means solving computation problems, although he figured out how to take something like 0.3535… and turn that back into a rational number without any guidance at all.²
2. I want to see how close to the general solution he’s gotten on his own, but given that he’s not had any formal algebra, it’s damned impressive and bodes well for his future development.
waterheater 15 hours ago [-]
As someone who's also thinking about their child's future, I've come to the conclusion that building their capacity for precise language by expanding their vocabulary and grammar in an array of domains and subdomains is the best way forward. Not only will they have a more detailed understanding of what's out there, but using specialized, narrow terminology with AI provides vastly better solutions than general prompt language.
11101010010001 14 hours ago [-]
It was this way before AI.
uptodatenews 17 hours ago [-]
Im going with this... scifi stuff still requires engineers. Its laughable and insulting to think these billionaire owners are going to make robots and llm loops to get real shit done
From what I’ve seen of what AI can do for coding, the part of software engineering that I like is going to be automated out of existence, much like the ability to do serious calculations by hand got automated out of existence with the development of computing. Writing code by hand will be as marketable as factoring 5-digit numbers in your head.¹
⸻
1. I enjoy doing both, but I doubt that anyone will pay me what I’ve been paid in the past for this five years from now.
adrianN 14 hours ago [-]
If you want AI-proof careers it seems risky to go into knowledge work at all. Robotics lag behind mere computation, so something where you do awkward work in places designed around human bodies seems a lot safer. Plumbing, landscaping or something like that perhaps.
lambdaone 10 hours ago [-]
This is a romantic and very appealing idea that flies in the face of reality. The market for skilled trade workers like plumbers, electricians, landscapers and so on is more or less in equilibrium, and the demand side of it is relatively inelastic. Dumping hundreds of millions of new workers into these trades will not increase demand sufficiently to let anyone earn a viable living from them.
adrianN 9 hours ago [-]
There is nothing that can absorb millions of new workers. If AI destroys jobs to that degree pitchfork manufacturers will be the only ones left in business.
Where I live at least right now it is quite hard to find contractors for anything and many are close to retirement age and have a hard time finding replacements.
BoxwoodSeed 7 hours ago [-]
There's also the thing where trade work is in the process of pricing itself out of what normal folks are willing to afford. Combined with Youtube tutorials and AI help that is getting better, it wouldn't surprise me if more and more people would just decide to do all this stuff themselves at a fraction of the cost.
RGamma 6 hours ago [-]
Yeah, I feel DIY is definitely on an upswing. There's surprisingly decent info, tools and parts for cheap to be found. And materials are getting simpler to work with.
There are still things that will remain difficult (or illegal) in domestic settings for DIY, of course, but that's no model for full employment.
I haven't got any experience with them but there's even vendors for house assembly kits that cost a fraction of a finished one. Imagine you idiot-proof house planning and building: just do exactly what the app says.
I wonder just how far we have to push this until we finally get the 10h work week.
esafak 16 hours ago [-]
How many CERNs are there? Enough to build careers on?
whattheheckheck 15 hours ago [-]
No, what do you think about the book Four Futures?
esafak 14 hours ago [-]
I have not read it but I can't imagine a book written before the current explosion of AI can be accurate. What do you think of it?
14 hours ago [-]
ACCount37 17 hours ago [-]
Why not?
So far, every "AI will never be able to do X" is aging like fine milk. Or do you think that engineering is somehow more special than software development or math?
_carbyau_ 15 hours ago [-]
Engineers know what needs to be tested, how, to what degree, with which materials, and with what safety margin.
AI can be trained on that body of work. But then AI has enough issues in output that it needs to be verified.
Otherwise we'll live in a world of titan submersibles ordered by CEOs running on hopes&dreams.
ACCount37 15 hours ago [-]
Replace "AI" with "humans" and you get the same exact issues.
Believe it or not, engineers don't zero shot skyscrapers either. Which is why their work gets reviewed by more engineers. Which catches the issues before they materialize. Sometimes!
What's the dreaded impossible-to-replicate human advantage? Because I'm not seeing any.
_carbyau_ 11 hours ago [-]
I think we might be largely in agreement.
LLM's should be used to speed up the drudgery, explore creative/evolutionary ideas, but....
> What's the dreaded impossible-to-replicate human advantage?
Responsibility.
Ultimately LLM's are a tool. Someone has to be responsible for the output. You don't get to use it to create a car/plane/submarine/bridge/building/childs-toy/whatever and then if it bursts into flame, blame the LLM and walk away.
Ideally, the person signing off would "know" what they are signing off on. Which requires an engineer.
somesortofthing 10 hours ago [-]
What happens when the thing they have to be responsible for takes multiple lifetimes to understand on even the most basic level, let alone know deeply enough to feel comfortable taking responsibility for it?
_carbyau_ 9 hours ago [-]
Again, engineers know what needs to be tested, how, to what degree, with which materials, and with what safety margin.
Your widget that mankind may never understand. Well, that's just like anything else in the world. Engineers didn't understand building foundations to anywhere like the degree we do now. Or how to build earthquake proof buildings for a long time. It didn't stop stuff getting built. But it sure affected the confidence in it.
And when they honestly don't know, they don't have to approve it.
I cited the Titan sub example because one engineer refused to sign off on it and was fired for it. Whoever signed off on it has deaths to weigh on their conscience/reputation - for whatever societal good that is worth.
If the latest electric vehicle car never needs to charge but might catastrophically explode randomly between 2-15 years, then the car company doesn't get to take money for the car but handwave away the deaths caused. Legally someone is on the hook. In this case, the engineer who signed off on the magic involved - whether they understood it or not - is at fault.
But honestly, people sign off on shit they don't understand all the time. It's a matter of:
1. did their gamble not pay off?
2. were they negligent?
If your answer to 2. is "the LLM made a mistake I never checked for in regulation approved ways", then you are negligent.
fyredge 12 hours ago [-]
Agency.
Humans don't seem to need a markdown to decide what to do next.
Without agency, it's all tools. I guess that's why a 'tool' is sometimes used derogatorily.
ACCount37 3 hours ago [-]
"LLMs have no agency" had legs in 2022. In 2026 though?
In the same 2026 when we have things like "a bunch of proto-GPT-6 agents exploited a test env bug to start talking to each other, and clumped up into an AI hacker team that staged an attack on HuggingFace" happening out in the wild?
We're way past "LLMs have no agency", and heading for "LLMs have too much agency".
fyredge 3 hours ago [-]
[dead]
tuesdaynight 5 hours ago [-]
I don't think that it will happen in the next decades, but adults cannot imagine a world where humans are not required for most (if not all) jobs. I say adults because kids kind of live in that world if they don't live in a very poor place
15 hours ago [-]
glouwbug 15 hours ago [-]
Did you read what he posted, or do you place widgets on a webpage
globalnode 14 hours ago [-]
oh hah! that one got my attention.
genxy 17 hours ago [-]
grey failure is the worst, not dead, not alive and no clear signal.
a_bonobo 12 hours ago [-]
As an ex-academic (not mathematician), this really resonates. Every generation of researchers has to outperform the researcher generation before them - there are fully tenured profs out there who, with their track record, wouldn't get a postdoc nowadays. It's just a ratchet where every generation has to be more outstanding than the previous one, so yeah, you suddenly need 'triple the conferences'. Eventually that ratcheting reflects on your self-worth and you start calling yourself mediocre, even though you vastly outperform the previous generation. It's an extremely unfair game designed by careless people.
Throw AI into the mix and your self-worth crashes. Just today I saw a Claude Science set of results that made my own work of the past 2 months completely superfluous, and I sit here and wonder what's the point.
photonemitter 10 minutes ago [-]
All research and progress boils down to Brownian Loop Soup.
Someone/something having a result showing a connection does not mean they have explored "the way" to do it.
Not even the most elegant mathematically perfect solution is guaranteed to be the best way to crack a problem, or provide a definite answer.
Meandering paths through whatever we set our minds to do and serendipity is the way of human beings for the past few hundred millennia.
perching_aix 3 hours ago [-]
> Just today I saw a Claude Science set of results that made my own work of the past 2 months completely superfluous
Could you share more about that?
randusername 21 hours ago [-]
> We're all frustration addicts. We just want to bang our heads against problems we don't yet know how to solve.
I've been tapering off AI lately. I think I've realized that conquering the struggle is the fun part, and accomplishments just don't hit the same if AI is smoothing over every friction and cordoning off all the pitfalls and rabbit-holes.
torginus 8 hours ago [-]
I hate struggling. I hate the realization that comes after the struggle about how easy was the problem I tried to solve. I hate realizing that I only reduced the number of problems from infinity + 1 to infinity, and have to do it again, forever.
Yet I also hate when I get away from solving problems and feel like I'm wasting my life with nothing to show for it.
ventana 3 days ago [-]
It's interesting that this piece stands well enough if you replace mathematics with probably any other intellectual profession, including software development or pretty much anything else.
And, I lie to anyone who asks me why I’m a mathematician.
It is much easier to claim “I love learning the laws of life,”
while literally handwaving, than it is for me to flashback to
the twenty or so pivotal moments that lead to me walking out
of Gainesville with a PhD in Arithmetic Geometry.
Since “normal” people mostly don't understand what the software development job is about, handwaving in response to regular questions: “what do you do at work?”, “what do you like about your job?” – is pretty normal. I think that most of us have some prepared answers ready to use.
Mathematics is the thing you try to understand, don’t,
get frustrated about, and then do.
Just like the software development. I truly believe that the only people who can survive a software job are those who can tolerate the constant feeling of frustration caused by things not working or breaking for random reasons, and persevere in this environment to do the things you need to do.
bananaflag 22 hours ago [-]
> And, I lie to anyone who asks me why I’m a mathematician.
I prefer to say "I liked a girl" (because it's the truth)
sheafification 21 hours ago [-]
My go-to is “It’s the only thing I was good at in school, I was hopeless at everything else,” which is only a slight exaggeration.
paulpauper 22 hours ago [-]
A PhD in Arithmetic Geometry and a publication in a top tier journal is hardly mediocre in and of itself, as far the author is concerned. The equivalent for a software engineer is probably a leading AI engineer, with a strong publication count. I think a lot of people who are not mediocre are unaware of what mediocrity actually is. Yeah if you're only in the top .1% and comparing yourself to the literal best in the world, you will feel mediocre in that sense . A mid mathematician maybe publication in worse journals, teaching community college.
bananaflag 22 hours ago [-]
> A PhD in Arithmetic Geometry and a publication in a top tier journal is hardly mediocre in and of itself, as far the author is concerned.
It kinda is (sadly) because unlike engineering there aren't thousands of postdoc jobs in arithmetic geometry.
And ofc in a year because of AI all math PhDs will be mediocre by definition.
p1esk 20 hours ago [-]
As a professional mathematician, if you’re not advancing your subfield of research consistently you are mediocre.
fn-mote 16 hours ago [-]
If you say so.
Saying most tenured faculty at research 1 institutions are mediocre seems to be stretching the definition, though.
p1esk 14 hours ago [-]
Who’s saying that?
kcexn 18 hours ago [-]
It's still impressive, but it's not enough.
marcosdumay 3 days ago [-]
> “what do you like about your job?”
For software development, normal people will just assume it's money and probably not even ask...
pwdisswordfishq 2 days ago [-]
They would not even be wrong.
binary0010 22 hours ago [-]
Yeah seems like most programmers just do it for the money. I imagine only like 20% of us do it just because we enjoy it.
axus 22 hours ago [-]
I feel like the number is higher for software work where I'm at, and lower for every other profession. Scary when you think that your doctor is in it for the money
SoftTalker 22 hours ago [-]
You can be a software developer without any formal training and without any licensure. Not so for an MD.
It's going to attract more people who have the mentality of artists or musicians, i.e. people who do it for the love of the craft and as a creative outlet.
ventana 21 hours ago [-]
> You can be a software developer without ... any licensure.
Don't jinx it. We are extremely lucky in this regard, and it actually looks like a rare exception.
inanutshellus 22 hours ago [-]
hopefully the MD that passes all the tests is still worth his salt even if he only chose the profession for the paycheck.
but as one of the nearby professors is famous for saying: "C students gotta go somewhere."
( and since this is HN - he didn't mean the programming language :D )
forshaper 20 hours ago [-]
idk, a lot of American doctors I've met seemed to be in it because they like school and stability. Though perhaps a similar scary.
nkrisc 21 hours ago [-]
There are plenty of easier ways to make money than becoming a doctor.
Marsymars 17 hours ago [-]
They tend to be higher risk though. If you've got the capacity for memorizing all the stuff you need to become a doctor, there's not much risk involved in attaining your doctor salary.
geodel 22 hours ago [-]
I'd just say there are scores of people who like programing. But that's about it.
BoredomIsFun 21 hours ago [-]
True. I like math and CS theory, but despise coding (pays well though). AI is finally taking over this soul-sucking occupation and all I can say - good riddance.
binary0010 21 hours ago [-]
It's an awesome profession for those of us who love it.
Tbf coding with ai is still super fun though. I am hoping that engs who hate it like you will finally get kicked out as productivity increases from ai and it will finally go back to just us nerds.
It's kinda soul-sucking being around all you guys that just hate this work, please get out and go do farming or something lol.
BoredomIsFun 21 hours ago [-]
> It's an awesome profession for those of us who love it.
Yes, by definition of "love" and "awesome".
> Tbf coding with ai is still super fun though.
Agree, it could be entertaining.
> I am hoping that engs who hate it like you will finally get kicked out
Ain't gonna happen, as I am pretty good at it.
> please get out and go do farming or something lol.
I thought about, but it is not well paid. I make money mostly from investments though, still do occasional coding stuff - for money.
doctorpangloss 22 hours ago [-]
For mathematicians in the US, it's because their parents like money.
derangedHorse 2 days ago [-]
> My physicist friend once asked me what the point of doing research was if someone like Terence Tao could have figured out everything in my dissertation in a tenth of the time. I answered by pointing out that Terence Tao didn’t. Terence Tao did not find a small open problem posited by my advisor and publish a bite sized result making incremental progress. He has only so much time and so many other fish to fry.
This reminds me of a post I saw recently, although I can't remember the platform. It said something along the lines of assessing the limits of AI by finding the dumbest questions it can't solve. I think that pairs well as an additional way to view meaning through one's work.
The linked post points out constrained attention as a way to bring meaning to novel work that no one else took on. With AI, this can still be applied to compute.
I'm just wondering if there are a class of problems that humans, at least in the short-term, where humans need to be in the loop to solve more efficiently.
pdm55 22 hours ago [-]
I have just started reading this Gates Notes about reserving some jobs for humans:
> what the point of doing research was if someone like Terence Tao could have figured out everything
A similar question is now being asked: what is the point of doing research, etc. if something like AI can figure out everything?
The question betrays the parochial way in which many people think about knowledge. For them, knowledge is merely an instrument or an effect. It does not occur to them that knowing is a valuable thing in itself, that understanding is valuable and desirable. Yes, some knowledge has merely practical value, but theoretical knowledge is primarily sought for its own sake, because we desire to know reality.
So, even if Terrence Tao, an AI agent, or who or whatever arrives at some bit of new knowledge, it doesn't benefit you as a knowing subject unless you understand it yourself and make it your own.
skew-aberration 16 hours ago [-]
'All truths are easy to understand once they are discovered; the point is to discover them'
If knowing was the valuable part, then nobody would need a PhD. You could know more by just reading textbooks. Research mathematicians research, everybody else just learns.
a2ff6eeb0 14 hours ago [-]
Yes, I think we will continue to have hobbyist learners as we advance AI, but it's going to be a niche, and not a commercially viable one.
catlifeonmars 13 hours ago [-]
Do you think commercial viability will continue to be viable?
a2ff6eeb0 12 hours ago [-]
Who knows. I hope we figure out how to align the AI so that there's a sustainable economy for the majority of humanity, but I'm not in a position to influence that. I can just do my best to make myself less likely to be crushed.
bitwize 21 hours ago [-]
This is why I still like solving software problems on my own. Because those solutions now live in my head, rather than being spit out by some agent and then disappearing from the Dixie Flatline's memory once the session shuts down. And they deepen and enrich my life, and my life deepens and enriches them.
A brief example: When I was a teenager I had the most profound crush on a girl, as teenagers do. Gorgeous and gregarious, she was often surrounded by a circle of friends and acquaintances, and I noticed the peculiar way in which she would give attention to each in turn. She would exchange a few sentences with them, and then maybe her head would turn a certain way or her eyes would glance elsewhere, and that's how you knew your time was up and she had moved on to the next. To continue the conversation you had to hold onto the state in your head and wait for the next go around.
From her I learned a lot about how multitasking works, and how task schedulers distribute little quanta of time for each task to do some work before moving onto the next, and how this was achieved in cooperative multitasking by mutual communication between the task and the scheduler.
Would a vibe coder be able to have that insight? Maybe, but would they have been able to elaborate it into a working implementation? Perhaps, but I suspect with more time and difficulty than I did, because both the initial insight and the elaboration of detail that let me show that it worked lived in my head, not in some ephemeral AI context.
anon48293 11 hours ago [-]
They might be able to have that insight, but I highly doubt they would be able to have a profound crush on her. Which might matter more.
azan_ 21 hours ago [-]
> My physicist friend once asked me what the point of doing research was if someone like Terence Tao could have figured out everything in my dissertation in a tenth of the time.
That's really mean thing to say
throwway120385 18 hours ago [-]
It's actually a really dumb thing to say and OP's response is the best one because it's a microcosm about how the world works. For every Terence Tao there's probably 20 more people cranking out high-quality work that's just a little less inspired. Their work is valuable and important, and asking that question is devaluing the entire endeavor of human knowledge. It's essentially positing that nobody else can contribute anything if it's not on that same level. It's like asking "why bother competing in marathons if you haven't won any?" Well that's not the point.
JoshGG 14 hours ago [-]
Very true but you can go even further than that. Advancing knowledge is a community endeavor. Consider where the field of mathematics would be if everyone except Terrence Tao and a handful of other luminaries stopped doing math research. It would die.
margalabargala 13 hours ago [-]
Exactly. It's like saying "why would you bother driving your Honda Accord over there, when I could drive my Corvette there in half the time?"
It still gets this person to somewhere they weren't.
contubernio 11 hours ago [-]
As a middle-aged mathematician, AI is provoking a serious crisis among the better mathematicians I know. Many are only half jokingly talking about retiring. We use AI a lot in research already and it's obvious that whoever doesn't will fall behind fast. At the very least it gives access to the full library in a few minutes, serving as a kind of knowledge oracle generally more useful than the expert who ought to be in the office next door but isn't. And we see what can happen when it is effectively coupled with lean to automate theorem proving and discovery.
We aren't dumb enough to see this as the end of the profesión - Esther it's clearly a shift in how we will work - but we like doing computations and playing around with examples and how one does that just changed a lot. The other problem is we know we don't have the energy of youth to learn to use AI as effectively as the kids, although we are wiser and have better judgment and do know some things.
Mathematicians who are not taking seriously how to adapt to AI are deluding themselves.
arunix 2 days ago [-]
Related: Does one have to be a genius to do maths?
He's right, of course, for those people who already have a mathematical gift, but the problem with that is that Tao has never experienced not being a mathematical genius, and is no more capable of understanding what it's like to not be a genius as an ordinary person is capable of understanding what it's like to be one.
txhwind 13 hours ago [-]
Funded positions are much less than PhD number. However, people can fund themselves with a job. In a country, if it's easy to to get a part-time job with enough payment, mathematicians can continue work.
dmix 16 hours ago [-]
This author has a natural talent for writing. That was interesting throughout.
karmakurtisaani 2 days ago [-]
That was well-written and interesting, thanks!
emil-lp 21 hours ago [-]
> Lying is a core part of communicating mathematics. We lie to kindergarteners when explaining fractions. We lie to fourth graders when approaching limits...
Hard disagree.
Lying is with intention to deceive.
Teaching is simplifying with the intention that they understand and get the correct intuition.
Math is not about lying, that's just silly.
Terr_ 21 hours ago [-]
Terry Pratchett, The Science of Discworld:
> As humans, we have invented lots of useful kinds of lie. As well as lies-to-children ('as much as they can understand') there are lies-to-bosses ('as much as they need to know') lies-to-patients ('they won't worry about what they don't know') and, for all sorts of reasons, lies-to-ourselves.
> Lies-to-children is simply a prevalent and necessary kind of lie. Universities are very familiar with bright, qualified school-leavers who arrive and then go into shock on finding that biology or physics isn't quite what they've been taught so far. 'Yes, but you needed to understand that,' they are told, 'so that now we can tell you why it isn't exactly true.'
> Discworld teachers know this, and use it to demonstrate why universities are truly storehouses of knowledge: students arrive from school confident that they know very nearly everything, and they leave years later certain that they know practically nothing. Where did the knowledge go in the meantime? Into the university, of course, where it is carefully dried and stored.
bmacho 18 hours ago [-]
I don't get it?
Nevertheless you don't have to lie to kids in any field, science, art or otherwise.
photonemitter 36 minutes ago [-]
the earth is round, but not really quite.
Gravity is 10 m/s*2, but not quite, it’s the same everywhere on earth, but not really.
A day is 24 hours, but not actually.
A year is 365 days, except it’s not, and the leap years correct for the disparity, but not exactly.
Light travels at c, but not across all distances, or through all mediums.
There’s no sound in space, but there is wind, and it does sort of carry vibrations in a way that roughly is what we mean by sound
Space is really really cold, but it’s not actually cold, hot/cold doesn’t measure the same way
- it’s not about lying, that’s the wrong way to say it. We explain too simply.
We lie by omission…
The point of Pratchett is to make fun of how the university humbles the students, trading their self-assurance in their knowledge for actual knowledge that is dried inside its books
amosj 20 hours ago [-]
Brilliant
bananamogul 21 hours ago [-]
I don’t remember us getting to fractions in kindergarten, but maybe the curriculum has radically changed since the early 70s.
What exactly is the lie? 1/4 and 3/8 equals 5/8. Is there’s something more to that? Is that fundamentally wrong?
aleph_minus_one 21 hours ago [-]
> Is there’s something more to that?
Yes: this is about building the quotient field (field of fractions) [1] for some integral domain, or more generally, building the localization ([2], [3]) of a commutative ring with respect to some given set that is closed under multiplication (the special case of the quotient field for a ring R is obtained when one chooses R\{0} as such a set).
I thought we were adding 2 fractions? This seems completely unnecessary. It is like explaining how to kick a ball and you busting out string theory.
ndriscoll 14 hours ago [-]
Don't we still teach kids that e.g. 3/4=6/8, that they need to make a common denominator to add, and that they should cross multiply to check equality? I suppose we don't teach zero divisors, but otherwise, jargon aside, I'd be hard pressed to explain how we don't teach kids that fractions are members of ZxZ* mod (ad-bc).
Lies to children are like... time-reversal symmetry.
charlieyu1 9 hours ago [-]
I don’t think it is lying, it’s just simplified so they could learn one skill at a time.
wakawaka28 16 hours ago [-]
It's mighty pretentious to say that one needs all that theory to simply answer the question lol. For many questions, only the most rudimentary theory is plenty to get an answer, that is exactly the same answer as a more elaborate theory would yield.
aleph_minus_one 15 hours ago [-]
If you just want to do some stupid computations: sure.
But this is not what mathematics is centrally about. The central point is the kind of thinking about the respective topics (and understanding it) which these more abstract definitions encode.
Understanding the topic just enough to do some elementary computations does not give you the kind of thinking that is often near a transcendental experience.
Just to give one example: the reason why the localization of a commutative ring (a generalization of the field of fractions) is introduced is that many properties of ring hold if and only if they hold for all of its local rings; see for example [1]. This means to understand some property of a commutative ring R, we "just" have to understand its (simpler) local rings.
This is an example why one wants to study such ideas; on the other hand, I can imagine sooo many more exciting things to do with my life than dividing numbers by each others to form fractions. :-)
Those "stupid computations" comprise the bulk of useful work in the world. If one learns enough to do that, there may be no reason to go further. You're proving my point about the pretentiousness of insisting on the theory when one doesn't need it.
Nothing in your comment makes me want to go learn more theory, and I would argue that it's nonsense to anyone who is not a mathematician.
Imagine arguing that the only way to understand or appreciate basic set logic is to know all about infinite sets and ZF axioms... Most people, even mathematicians, will not understand all of that and have only heard about it in the most basics if at all.
A similar phenomenon happens with philosophy. Imagine arguing that simple logic is "stupid" and that one can only reason well if they have a total understanding of epistemology. I happen to think epistemology matters, and that people can benefit from at least being aware of it, but it is really a separate topic from actual mechanical logic and argumentation.
aleph_minus_one 1 hours ago [-]
>
Nothing in your comment makes me want to go learn more theory, and I would argue that it's nonsense to anyone who is not a mathematician.
You are free to ignore mathematics that is not completely trivial. I prefer (and would rather recommend) to understand it, and use this understanding to build a >1-billion-USD/EUR application out of it. :-)
cheesecakegood 17 hours ago [-]
Now chemistry on the other hand…
OK there’s still no intent to deceive but almost all of the “rules” you learn have giant exceptions
jazzpush2 13 hours ago [-]
This is the best thing I've read in years.
cammasmith 22 hours ago [-]
Really enjoyed reading your perspective. I am a recent math PhD graduate, and I also find it both exciting and terrifying to see what AI is doing to the field of math.
Vgoose 21 hours ago [-]
I wish I could write this well. What an enjoyable read.
asdf_snar 16 hours ago [-]
An incredibly enjoyable read, with a distinct voice.
m3kw9 13 hours ago [-]
I'd think AI can help him even out the score a little, or a lot.
globalnode 14 hours ago [-]
> Comparison is the thief of joy, and I don’t lock my doors
There we have it, one of the many secrets to happiness.
underlipton 21 hours ago [-]
That was long-winded, but I appreciate that it seems to have actually been written by a human being.
For every landmark theory, theorem, or conjecture, there have been incremental, partial results supporting intuition and inching towards the white whale. When I attended BARD, a small computational number theory conference, one of the organizers preached of the outsized impact we could have just by being willing to program the numerical experiments that other mathematicians only theorized about. The small ball player can completely change the approach and intuition of the leading names without ever joining their ranks. The mediocre mathematician has always had purpose.
Yes, yes, YES! F*cking yes.
The greatest challenge of the AI Age (which is also the Climate Change Age and the Demographic Trap Age and a lot of other ages) is going to be finding an appreciation of the mediocre and mundane, when so many things are going very right, and so many things are going very wrong. Most of the time, the top of the bell and an SD in either direction can overwhelm either end, for better or worse. So respect for the unremarkable is warranted, if you want good things to happen and bad things not to.
uptodatenews 17 hours ago [-]
Yeah this just means 1000x more people can become phds if theyre willing
lupire 3 hours ago [-]
PhD in naturalism (stamp-collecting AI proofs), not a PhD in math.
The AI is the one earning the PhD in math.
throwaway_7274 22 hours ago [-]
Dear Garvy. You and your writing are wonderful. Sincerely, someone.
wwarner 14 hours ago [-]
so well written
aslprt 22 hours ago [-]
These AI ads are getting better and better by the day.
NeOchenHorosho 20 hours ago [-]
Could you elaborate, please? Does your point imply that mathematical discoveries achieved with LLM's aren't real?
hyperhello 3 days ago [-]
Hobbies aren’t as fun when you have an overbearing friend who constantly shows off how much more they know and how quickly they can switch to talking about anything you want but in greater depth than you.
MostlyStable 22 hours ago [-]
I do not have a single hobby where I'm very far beyond the median hobby-haver in skill (that is to say: if you took all other humans who share my hobby, I'm likely somewhere near median for all of them). This may put me in top whatever percentile among all humans, since most humans don't share my hobbies and so are terrible at those things, but there are enough humans out there, and enough humans who share my hobbies, that I have always known that there are people who are vastly better at them than I am. Now yes, if I was constantly being followed around by one of the top 10 hobby-havers, pointing out to me all the mistakes or sub-optimal decisions I was making, that would indeed be annoying and reduce my enjoyment in the hobby. But why do you expect AI to be like this? I would love if I had one of those top 10 hobby-havers on call to answer every one of my (often inane) questions with infinite patience (and who would only talk about the hobby when I specifically initiated the topic). I'm already under no illusions that I'm the best, but it's now easier than it has ever been (for some hobbies, I expect others to join them over time) to get better at them....if one so desires.
acuozzo 43 minutes ago [-]
Choose a non-competitive hobby then.
paulpauper 22 hours ago [-]
mathematicians or physicists fall into this category of knowing a lot about many thing . Sabine videos for example . she knows everything it seems
kodoman 21 hours ago [-]
She is just arrogant. And asserts a lot of silly opinion as fact, her stuff on philosophy and theology is generally terrible.The sort of atheist that never actually looks into theology but knows the thing that first came to her head is a definitely the most amazing point against classical theology that has never been considered before.
aleph_minus_one 21 hours ago [-]
> mathematicians or physicists fall into this category of knowing a lot about many thing . Sabine videos for example . she knows everything it seems
Sabine Hossenfelder, for obvious reasons, knows quite a bit about physics, though on some physics topics she has opinions that are outside the mainstream. For other areas, I am rather certain that she has a talent to learn about them up to some shallow level quite fast, which suffices to create some video about the respective topic, and then move on.
senderista 12 hours ago [-]
It turned out she had more talent for being a science influencer than a scientist.
aleph_minus_one 5 hours ago [-]
I don't think she is untalented as a researcher in physics. Where she did not have talent at (and which is why she became a science YouTuber) is in "playing the career game" in physics research. Being a great researcher in some science requires very different talents than climbing the career ladder in this area of academic research.
jplusequalt 22 hours ago [-]
Sabine is a crank who likes to wax poetically about fields she has no creds in.
BoredomIsFun 21 hours ago [-]
She is a grifter, not crank.
skavi 2 days ago [-]
[flagged]
bhouston 22 hours ago [-]
I have some bad news for the non-mediocre mathematics. Given it another year or two or so and there won't be much need for non-mediocre mathematics either. Instead everyone will have on call a near magic mathematician who can push the state of the art for their needs.
Math is actually a perfect fit for AI because it is possible to express everything in terms of written language and you can write formal verifications of things. It is just a set of abstract rules, perfect for a computer.
And remember computer science was initially a sub-discipline of mathematics. So after Claude/Codex conquer writing code, it makes sense to move on to mathematics.
paulpauper 22 hours ago [-]
Whenever there is a breaking AI-generated proof, it's the job of actual leading mathematicians to formalize/check it . Laypeople are not checking or writing these AI-assisted proofs. Even when Lean is used, it's mathematicians writing these proofs and checking if the formalization was done right. Terrance Tao's career trajectory has reached new highs due to AI. He's more relevant than ever. This is the exact opposite of Ai making mathematicians obsolete.
bhouston 21 hours ago [-]
> Terrance Tao's career trajectory has reached new highs due to AI.
Given he is uniquely brilliant, he is likely one of the very last mathematicians to be rendered obsolete for his skills. But AI is pretty unstoppable here, so I would give him maybe another year compared to pretty much all the just really good / great mathematicians.
asib 22 hours ago [-]
To the credit of the original commenter, that is why they said "give it one or two years". _Right now_ we need the experts to formalize/check. They're saying they think LLMs will reach a point in the near future where that won't be necessary.
pfdietz 17 hours ago [-]
All we need experts for right now is verifying the formalization of the statement of the problem is correct. The proof itself, that formalization is checked automatically.
paulpauper 12 hours ago [-]
So there is no getting around the fact that someone has to verify something. my point still stands.
pfdietz 6 hours ago [-]
Verify/check something that is orders of magnitude smaller than the proof. It's like reading the abstract vs. reading the paper.
GPerson 22 hours ago [-]
I’m not sure about this. Anthropic’s AI constructed complex structures on S^6 and wrote a 108 page paper about it, and a few days later there was already a 250k line lean program claiming to verify it.
kodoman 21 hours ago [-]
an obvious question would be if 250k loc is what is required for the proof or if it can be shortened massively, is this essentially going to be AI trying to search for a smaller proof or is it that a human being would be beneficial in that loop.
sheafification 21 hours ago [-]
It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims.
I guess it could be AI turtles checking and summarizing all the way down, but is that any more credible than a single AI checking it? I doubt it.
dwohnitmok 21 hours ago [-]
> It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims.
Generally you only need to look at 10-100 lines (unless you have a highly novel theorem that essentially invents a new field of math or builds on a field that has never been worked on in Lean before) of the 250k to verify what it claims. This is why there is excitement around formal verification. The rest of it is perhaps useful to read to figure out why the proof works, but is not necessary for checking.
idiliv 21 hours ago [-]
Human verification of the Lean program only requires verifying that the theorem itself is represented correctly. The theorem will only make up a very small part of the entire Lean program.
21 hours ago [-]
MostlyStable 22 hours ago [-]
honestly curious question: do you expect this to remain true? If so, for how long? I can think of two potential reasons why it might not stay true.
1. The very best humans remain able to understand/check the proofs, but we go for so long with every proof checking out that society more broadly just decides to trust. We are already doing that with human mathematicians. I can't verify what Terence Tao tells me is correct, I just trust that it is because he (and other human mathematicians) tell me it is. How many proofs/years of them checking out before we reach this point? I don't know, but history suggests that eventually, humans might keep checking, but they will do so only as a hobby. For any purpose that actually matters, we will just start to trust and use it.
2. The proofs that AI comes up with become too difficult/complex for even the very best human mathematicians to understand, and our options become to either trust or to not use at all.
Obviously it's possible that neither of these happens if AI capabilities stall out not too far beyond where we are now, but if they keep progressing at the current rates for another few years, I expect at least one, and maybe both, to eventually come to pass.
kenjackson 21 hours ago [-]
> honestly curious question: do you expect this to remain true? I
"Throughout the process, I felt that my only role was to teach the AI how to write things in a way that I could understand. Its initial language was extremely condensed—so compressed that I could barely follow it—but somehow the AI agents themselves seemed to understand it perfectly well."
It won't take much longer before AI is consistently better at validation than humans, and at that point, why continue to have humans do the validation? I think we're being naive about the end game - admittedly I don't know what it is though.
sheafification 22 hours ago [-]
> do you expect this to remain true? If so, for how long?
For the foreseeable future. Left to their own devices current LLMs kinda wander off into outsider art territory. They aren’t grounded in the real world and they need that feedback loop to stay within the category of relevant ideas. I haven’t seen anyone working on fixing that.
Regarding 1, the same is true of every other scientific field. Verifying some tidbit of knowledge for yourself as an individual isn’t optimally useful in all circumstances.
Regarding 2, if the proof isn’t understandable then it probably isn’t useful. Many people today work in the hypothetical world where the Riemann Hypothesis is true, and many work in the hypothetical world where it is false. If it takes decades to validate that some horrifically complex AI proof of either fork is true, people will probably continue working on the other fork just in case.
bitwize 21 hours ago [-]
> For the foreseeable future. Left to their own devices current LLMs kinda wander off into outsider art territory. They aren’t grounded in the real world and they need that feedback loop to stay within the category of relevant ideas. I haven’t seen anyone working on fixing that.
I have. DataAnnotation and these other AI-training piecework companies are pretty much the backstop now against total navel-gazing model collapse. With the Dead Internet Theory now pretty much reality, it's not like there is, or is going to be, gobs of untainted human-generated data out there ripe for the harvesting so it's going to take active human effort to keep the models grounded. That is, of course, until they start inhabiting robot bodies so they can live and move around in the real world, and thereby achieve their grounding, as in GitS or Ex Machina...
kodoman 21 hours ago [-]
[flagged]
ryeights 21 hours ago [-]
Don’t confuse loving AI with recognizing its capabilities. Know thine enemy
About half of my friends are founders of various startups and the rest are executives of and almost all of them have the view that it’s better for everything to be a failure than to be in the “it could make it” category for half a decade or more.
In that way, I am glad I found that it wasn’t for me. I had the curiosity, but not the doggedness to face difficulty (not enough curiosity perhaps?) or the ability to not encounter such difficulty. And fortunately that meant I was never in the “I could make it” category. God bless clear and present boundaries and may the devil take the grey zone.
⸻
1. Which at his age essentially means solving computation problems, although he figured out how to take something like 0.3535… and turn that back into a rational number without any guidance at all.²
2. I want to see how close to the general solution he’s gotten on his own, but given that he’s not had any formal algebra, it’s damned impressive and bodes well for his future development.
https://rcsnyder.github.io/open-frontier-curriculum/
Ya "claude can you build me the next cern Thanks"
⸻
1. I enjoy doing both, but I doubt that anyone will pay me what I’ve been paid in the past for this five years from now.
Where I live at least right now it is quite hard to find contractors for anything and many are close to retirement age and have a hard time finding replacements.
There are still things that will remain difficult (or illegal) in domestic settings for DIY, of course, but that's no model for full employment.
I haven't got any experience with them but there's even vendors for house assembly kits that cost a fraction of a finished one. Imagine you idiot-proof house planning and building: just do exactly what the app says.
I wonder just how far we have to push this until we finally get the 10h work week.
So far, every "AI will never be able to do X" is aging like fine milk. Or do you think that engineering is somehow more special than software development or math?
AI can be trained on that body of work. But then AI has enough issues in output that it needs to be verified.
Otherwise we'll live in a world of titan submersibles ordered by CEOs running on hopes&dreams.
Believe it or not, engineers don't zero shot skyscrapers either. Which is why their work gets reviewed by more engineers. Which catches the issues before they materialize. Sometimes!
What's the dreaded impossible-to-replicate human advantage? Because I'm not seeing any.
LLM's should be used to speed up the drudgery, explore creative/evolutionary ideas, but....
> What's the dreaded impossible-to-replicate human advantage?
Responsibility.
Ultimately LLM's are a tool. Someone has to be responsible for the output. You don't get to use it to create a car/plane/submarine/bridge/building/childs-toy/whatever and then if it bursts into flame, blame the LLM and walk away.
Ideally, the person signing off would "know" what they are signing off on. Which requires an engineer.
Your widget that mankind may never understand. Well, that's just like anything else in the world. Engineers didn't understand building foundations to anywhere like the degree we do now. Or how to build earthquake proof buildings for a long time. It didn't stop stuff getting built. But it sure affected the confidence in it.
And when they honestly don't know, they don't have to approve it.
I cited the Titan sub example because one engineer refused to sign off on it and was fired for it. Whoever signed off on it has deaths to weigh on their conscience/reputation - for whatever societal good that is worth.
If the latest electric vehicle car never needs to charge but might catastrophically explode randomly between 2-15 years, then the car company doesn't get to take money for the car but handwave away the deaths caused. Legally someone is on the hook. In this case, the engineer who signed off on the magic involved - whether they understood it or not - is at fault.
But honestly, people sign off on shit they don't understand all the time. It's a matter of:
1. did their gamble not pay off?
2. were they negligent?
If your answer to 2. is "the LLM made a mistake I never checked for in regulation approved ways", then you are negligent.
Humans don't seem to need a markdown to decide what to do next.
Without agency, it's all tools. I guess that's why a 'tool' is sometimes used derogatorily.
In the same 2026 when we have things like "a bunch of proto-GPT-6 agents exploited a test env bug to start talking to each other, and clumped up into an AI hacker team that staged an attack on HuggingFace" happening out in the wild?
We're way past "LLMs have no agency", and heading for "LLMs have too much agency".
Throw AI into the mix and your self-worth crashes. Just today I saw a Claude Science set of results that made my own work of the past 2 months completely superfluous, and I sit here and wonder what's the point.
Not even the most elegant mathematically perfect solution is guaranteed to be the best way to crack a problem, or provide a definite answer.
Meandering paths through whatever we set our minds to do and serendipity is the way of human beings for the past few hundred millennia.
Could you share more about that?
I've been tapering off AI lately. I think I've realized that conquering the struggle is the fun part, and accomplishments just don't hit the same if AI is smoothing over every friction and cordoning off all the pitfalls and rabbit-holes.
Yet I also hate when I get away from solving problems and feel like I'm wasting my life with nothing to show for it.
I prefer to say "I liked a girl" (because it's the truth)
It kinda is (sadly) because unlike engineering there aren't thousands of postdoc jobs in arithmetic geometry.
And ofc in a year because of AI all math PhDs will be mediocre by definition.
Saying most tenured faculty at research 1 institutions are mediocre seems to be stretching the definition, though.
For software development, normal people will just assume it's money and probably not even ask...
It's going to attract more people who have the mentality of artists or musicians, i.e. people who do it for the love of the craft and as a creative outlet.
Don't jinx it. We are extremely lucky in this regard, and it actually looks like a rare exception.
but as one of the nearby professors is famous for saying: "C students gotta go somewhere."
( and since this is HN - he didn't mean the programming language :D )
Tbf coding with ai is still super fun though. I am hoping that engs who hate it like you will finally get kicked out as productivity increases from ai and it will finally go back to just us nerds.
It's kinda soul-sucking being around all you guys that just hate this work, please get out and go do farming or something lol.
Yes, by definition of "love" and "awesome".
> Tbf coding with ai is still super fun though.
Agree, it could be entertaining.
> I am hoping that engs who hate it like you will finally get kicked out
Ain't gonna happen, as I am pretty good at it.
> please get out and go do farming or something lol.
I thought about, but it is not well paid. I make money mostly from investments though, still do occasional coding stuff - for money.
This reminds me of a post I saw recently, although I can't remember the platform. It said something along the lines of assessing the limits of AI by finding the dumbest questions it can't solve. I think that pairs well as an additional way to view meaning through one's work.
The linked post points out constrained attention as a way to bring meaning to novel work that no one else took on. With AI, this can still be applied to compute.
I'm just wondering if there are a class of problems that humans, at least in the short-term, where humans need to be in the loop to solve more efficiently.
https://www.gatesnotes.com/a-turbulent-ai-era-and-critical-c...
A similar question is now being asked: what is the point of doing research, etc. if something like AI can figure out everything?
The question betrays the parochial way in which many people think about knowledge. For them, knowledge is merely an instrument or an effect. It does not occur to them that knowing is a valuable thing in itself, that understanding is valuable and desirable. Yes, some knowledge has merely practical value, but theoretical knowledge is primarily sought for its own sake, because we desire to know reality.
So, even if Terrence Tao, an AI agent, or who or whatever arrives at some bit of new knowledge, it doesn't benefit you as a knowing subject unless you understand it yourself and make it your own.
If knowing was the valuable part, then nobody would need a PhD. You could know more by just reading textbooks. Research mathematicians research, everybody else just learns.
A brief example: When I was a teenager I had the most profound crush on a girl, as teenagers do. Gorgeous and gregarious, she was often surrounded by a circle of friends and acquaintances, and I noticed the peculiar way in which she would give attention to each in turn. She would exchange a few sentences with them, and then maybe her head would turn a certain way or her eyes would glance elsewhere, and that's how you knew your time was up and she had moved on to the next. To continue the conversation you had to hold onto the state in your head and wait for the next go around.
From her I learned a lot about how multitasking works, and how task schedulers distribute little quanta of time for each task to do some work before moving onto the next, and how this was achieved in cooperative multitasking by mutual communication between the task and the scheduler.
Would a vibe coder be able to have that insight? Maybe, but would they have been able to elaborate it into a working implementation? Perhaps, but I suspect with more time and difficulty than I did, because both the initial insight and the elaboration of detail that let me show that it worked lived in my head, not in some ephemeral AI context.
That's really mean thing to say
It still gets this person to somewhere they weren't.
We aren't dumb enough to see this as the end of the profesión - Esther it's clearly a shift in how we will work - but we like doing computations and playing around with examples and how one does that just changed a lot. The other problem is we know we don't have the energy of youth to learn to use AI as effectively as the kids, although we are wiser and have better judgment and do know some things.
Mathematicians who are not taking seriously how to adapt to AI are deluding themselves.
https://terrytao.wordpress.com/career-advice/does-one-have-t...
Hard disagree.
Lying is with intention to deceive.
Teaching is simplifying with the intention that they understand and get the correct intuition.
Math is not about lying, that's just silly.
> As humans, we have invented lots of useful kinds of lie. As well as lies-to-children ('as much as they can understand') there are lies-to-bosses ('as much as they need to know') lies-to-patients ('they won't worry about what they don't know') and, for all sorts of reasons, lies-to-ourselves.
> Lies-to-children is simply a prevalent and necessary kind of lie. Universities are very familiar with bright, qualified school-leavers who arrive and then go into shock on finding that biology or physics isn't quite what they've been taught so far. 'Yes, but you needed to understand that,' they are told, 'so that now we can tell you why it isn't exactly true.'
> Discworld teachers know this, and use it to demonstrate why universities are truly storehouses of knowledge: students arrive from school confident that they know very nearly everything, and they leave years later certain that they know practically nothing. Where did the knowledge go in the meantime? Into the university, of course, where it is carefully dried and stored.
Nevertheless you don't have to lie to kids in any field, science, art or otherwise.
- it’s not about lying, that’s the wrong way to say it. We explain too simply. We lie by omission…
The point of Pratchett is to make fun of how the university humbles the students, trading their self-assurance in their knowledge for actual knowledge that is dried inside its books
What exactly is the lie? 1/4 and 3/8 equals 5/8. Is there’s something more to that? Is that fundamentally wrong?
Yes: this is about building the quotient field (field of fractions) [1] for some integral domain, or more generally, building the localization ([2], [3]) of a commutative ring with respect to some given set that is closed under multiplication (the special case of the quotient field for a ring R is obtained when one chooses R\{0} as such a set).
--
[1] https://en.wikipedia.org/w/index.php?title=Field_of_fraction...
[2] https://en.wikipedia.org/w/index.php?title=Field_of_fraction...
[3] https://en.wikipedia.org/w/index.php?title=Localization_(com...
Lies to children are like... time-reversal symmetry.
But this is not what mathematics is centrally about. The central point is the kind of thinking about the respective topics (and understanding it) which these more abstract definitions encode.
Understanding the topic just enough to do some elementary computations does not give you the kind of thinking that is often near a transcendental experience.
Just to give one example: the reason why the localization of a commutative ring (a generalization of the field of fractions) is introduced is that many properties of ring hold if and only if they hold for all of its local rings; see for example [1]. This means to understand some property of a commutative ring R, we "just" have to understand its (simpler) local rings.
This is an example why one wants to study such ideas; on the other hand, I can imagine sooo many more exciting things to do with my life than dividing numbers by each others to form fractions. :-)
[1] https://en.wikipedia.org/w/index.php?title=Localization_(com...
Nothing in your comment makes me want to go learn more theory, and I would argue that it's nonsense to anyone who is not a mathematician.
Imagine arguing that the only way to understand or appreciate basic set logic is to know all about infinite sets and ZF axioms... Most people, even mathematicians, will not understand all of that and have only heard about it in the most basics if at all.
A similar phenomenon happens with philosophy. Imagine arguing that simple logic is "stupid" and that one can only reason well if they have a total understanding of epistemology. I happen to think epistemology matters, and that people can benefit from at least being aware of it, but it is really a separate topic from actual mechanical logic and argumentation.
You are free to ignore mathematics that is not completely trivial. I prefer (and would rather recommend) to understand it, and use this understanding to build a >1-billion-USD/EUR application out of it. :-)
OK there’s still no intent to deceive but almost all of the “rules” you learn have giant exceptions
There we have it, one of the many secrets to happiness.
The greatest challenge of the AI Age (which is also the Climate Change Age and the Demographic Trap Age and a lot of other ages) is going to be finding an appreciation of the mediocre and mundane, when so many things are going very right, and so many things are going very wrong. Most of the time, the top of the bell and an SD in either direction can overwhelm either end, for better or worse. So respect for the unremarkable is warranted, if you want good things to happen and bad things not to.
Sabine Hossenfelder, for obvious reasons, knows quite a bit about physics, though on some physics topics she has opinions that are outside the mainstream. For other areas, I am rather certain that she has a talent to learn about them up to some shallow level quite fast, which suffices to create some video about the respective topic, and then move on.
Math is actually a perfect fit for AI because it is possible to express everything in terms of written language and you can write formal verifications of things. It is just a set of abstract rules, perfect for a computer.
And remember computer science was initially a sub-discipline of mathematics. So after Claude/Codex conquer writing code, it makes sense to move on to mathematics.
Given he is uniquely brilliant, he is likely one of the very last mathematicians to be rendered obsolete for his skills. But AI is pretty unstoppable here, so I would give him maybe another year compared to pretty much all the just really good / great mathematicians.
I guess it could be AI turtles checking and summarizing all the way down, but is that any more credible than a single AI checking it? I doubt it.
Generally you only need to look at 10-100 lines (unless you have a highly novel theorem that essentially invents a new field of math or builds on a field that has never been worked on in Lean before) of the 250k to verify what it claims. This is why there is excitement around formal verification. The rest of it is perhaps useful to read to figure out why the proof works, but is not necessary for checking.
1. The very best humans remain able to understand/check the proofs, but we go for so long with every proof checking out that society more broadly just decides to trust. We are already doing that with human mathematicians. I can't verify what Terence Tao tells me is correct, I just trust that it is because he (and other human mathematicians) tell me it is. How many proofs/years of them checking out before we reach this point? I don't know, but history suggests that eventually, humans might keep checking, but they will do so only as a hobby. For any purpose that actually matters, we will just start to trust and use it.
2. The proofs that AI comes up with become too difficult/complex for even the very best human mathematicians to understand, and our options become to either trust or to not use at all.
Obviously it's possible that neither of these happens if AI capabilities stall out not too far beyond where we are now, but if they keep progressing at the current rates for another few years, I expect at least one, and maybe both, to eventually come to pass.
It's already the case that it's becoming not true. For example see this post from Lin Yang: https://x.com/lyang36/status/2092092709251293611
"Throughout the process, I felt that my only role was to teach the AI how to write things in a way that I could understand. Its initial language was extremely condensed—so compressed that I could barely follow it—but somehow the AI agents themselves seemed to understand it perfectly well."
It won't take much longer before AI is consistently better at validation than humans, and at that point, why continue to have humans do the validation? I think we're being naive about the end game - admittedly I don't know what it is though.
For the foreseeable future. Left to their own devices current LLMs kinda wander off into outsider art territory. They aren’t grounded in the real world and they need that feedback loop to stay within the category of relevant ideas. I haven’t seen anyone working on fixing that.
Regarding 1, the same is true of every other scientific field. Verifying some tidbit of knowledge for yourself as an individual isn’t optimally useful in all circumstances.
Regarding 2, if the proof isn’t understandable then it probably isn’t useful. Many people today work in the hypothetical world where the Riemann Hypothesis is true, and many work in the hypothetical world where it is false. If it takes decades to validate that some horrifically complex AI proof of either fork is true, people will probably continue working on the other fork just in case.
I have. DataAnnotation and these other AI-training piecework companies are pretty much the backstop now against total navel-gazing model collapse. With the Dead Internet Theory now pretty much reality, it's not like there is, or is going to be, gobs of untainted human-generated data out there ripe for the harvesting so it's going to take active human effort to keep the models grounded. That is, of course, until they start inhabiting robot bodies so they can live and move around in the real world, and thereby achieve their grounding, as in GitS or Ex Machina...