Or at least, we’re pretty sure that it’s a proof! There’s a Lean certificate, as there are for some of the other 372 breakthrough results (not all of them). But it also appears that no human has understood just about any of these proofs yet
It seems that the obvious thing to do would be to release in TWO parts: the ones that are verified, and the ones that might have some good ideas but also might have some mistakes. Presumably the latter would be much more epxensive for humans to verify.
Given the constraint (3.5 hours of model effort) having a Lean proof is actually a sign that some of the results are likely weak. Despite the community efforts, the mathlib has many gaps and lacks many basic theories. So many problems can not even be stated yet not to mention proved. And formalization steps are small and labor intensive, so you are often constrained in how far you can go by the volume of code you produce. It's also telling that Lean tooling isn't advanced by the labs despite the resources they put into their effort, the importance they attache to Lean and the frictions they must have run into constantly. The release feels more like a retreat by the labs.
For example mathlib doesn't develop basic theories like Riemann surfaces, and doesn't have Riemann existence theorem etc. So if you develop a complex analysis result without these there are many things you can't even talk about. Developing basic theories takes time and efforts. See Anthropic FLT proof for example. While 13 million lines headline count may contain 50% redundancies due to agent swarming, on the net they still dedicated millions lines of effort to develop basic theories. And often they developed specialized versions in concrete theories just sufficient for their needs. For example they still don't have Riemann surfaces nor Riemann existence.
Right and these are perfect math objects: a perfect sphere has only one parameter. You can't describe a real life ball in Lean. You may be able to describe a class of real life balls using probability theory.
Having a Lean proof is an assurance that you proved something. But without going through the definitions we can't know what you proved. This part can't be mechanized. It's like a program that is compiled will likely run, but you can't say it will produce what you want. FLT stands out as everyone can read the statement. This is not true for most open math problems.
Yes for a fixed amount of effort the more you dedicate to formalization the less room there is for exploration. So the constraint is the total budget. The other constraint is if your language doesn't have the concept of gravity it is less likely you are developing the theory of gravity. So if you want to talk about modularity lifting in Lean you need to build up theories on elliptic curves, modular forms, modular curves etc first, because the library doesn't have them even if you consider them elementary. So now if you have a Lean proof with little effort I can infer that it is unlikely to say anything deep about these subjects. If you only have a paper proof, otoh, that doesn't bound your distance from the basics for me.
I may be simplifying things a little but it is two-fold: one Lean lets you call your theorem whatever you want, but if your vocabulary doesn't include the math objects I am interested in, it is unlikely that you said something interesting about them; secondly steps are painfully small in formalized math and even then you have to fight to get Lean not confused about what you are doing (like typeclass inference), so what you can do in three and half hours from a low base is quite bounded.
That seems to be a creative way to have other people review your slop.
A bit like submitting an llm written PR to an open source project without reading and understanding it.
Have your LLM generate 372 mathematical "breakthroughs" and then have 2 thousands mathematicians spend two weeks trying to understand each to tell you maybe one or two are viable...
I think that on closer inspection, a lot of these fully AI generated proofs will fall apart. Even in Lean, you can build theories which compile but nonetheless state something different than what you actually intend. It's just that the volume of proof is so staggeringly large that it will probably take years before we find the issues, a la abc conjecture
Many of the statements were already there and looked over by the community in lean prior to the work though, the statement can get formalized before the proof of it.
I just think that with the vast amounts of compute involved and the tendency to reward hack, we can't assume the steps towards that formalization are without error until full human understanding of the formalization.
It doesn't have to be the statement, see the recent incident where someone used an LLM to generate a lean refutation of the collatz conjecture, the lean proof exploited bugs in the lean kernel.
That proof was artificially constructed specifically to show the exploit. It wasn't a real attempt at a proof that was later shown to be using an exploit.
I'm unaware of any serious proofs that have been shown to have a kernel exploit in them.
That's a different argument than ijustlovemath is making
I agree with Jtarii that it's very unlikely a Lean bug is critical to most of these proofs. But we're in strange times, so I agree wtih the sentiment that we should wait for further analysis before declaring complete confidence in the proofs.
1. why can’t the so called “real mathematicians” (as if mathematics does not belong to all of us) write the lean theorems by hand and then we let the machine fill the rest in? They are very upset that they can no longer contribute to frontier mathematics. This would let them contribute.
2. Why shouldn’t math progress happen in the open, commit by commit? Why is it so horrible if a proof is 95% of the way there but we later find that it needs to be refined? Mathematics previously was optimizing for an antiquated publishing and distribution scheme. There is no need for the first print to be correct. We have the internet now. We can and should publish incomplete results and correct things on the fly. Maybe mathematicians would have solved some of these problems years ago if they didn’t hide incomplete almost solutions in their filing cabinet because it wasn’t yet ready to be published.
You don’t hate the pageantry of mathematics and academics enough.
I mean 95% of a proof is not a proof, and the fact that we got 95% of the way there isn't necessarily an indication that we'll ever get there. There's also a big difference between publishing a mostly-done proof as such and publishing a proof as complete only to retract later.
There's a lot to hate about the academic world, but the solution isn't spewing out terabytes of crappy half-baked results.
What are you even saying. Mathematics largely happens “commit by commit” as insufferable as that is a way of saying it, via conferences and meetings and prepublications. You’re attributing some bizarre to morality how mathematicians operate. You’re just upset people aren’t playing at your playground enough to your liking.
Also “real mathematicians” aren’t the people who “math belongs to”, you’re a mathematician if you do math, that’s it.
1. In OpenAI's case, they dumped 1.8 GiB of Lean proofs on the world. I don't think they've done anything ethically wrong by doing that, but it's the exact opposite of "commit by commit". In fact, I'd say human mathematics has been much closer to "commit by commit", usually using smaller results as stepping stones.
2. You can have "commit by commit" without formal provers like Lean. Just keep your text in a Git repo.
I feel this comment is based on a misunderstanding of how Lean works. In Lean you don't need to inspect the proof. There is no "closer inspection". All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
A tiny fraction compared to the proof, I'm guessing.
But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs.
That is an idealized caricature, and far from the reality. One needs to validate the statement of the theorem and the boundary conditions needed to prove it (definitions, axioms, kernel soundness, etc), a la dependency injection. Mathlib is a common shared platform of vetted truths, but not all proofs restrict themselves to Mathlib AFAIK, and neither is Mathlib perfect -- particularly subtle mismatches in the definitions.
Oh I fully understand how Lean works, how minimal the kernel is etc. I just think that just because "it compiled", we don't actually know that the autoformalization proved all the right stuff along the way. After all, LLMs can produce correct proofs for statements that don't align with the original intended theorem [1]. I just think we should be a bit more skeptical in general before saying these seminal results are fully true. What's the rush?
> All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
That's exactly what the navier stokes paper posted yesterday pointed out where the LLM bends the Lean code to make it "compile", because the NL might be wrong to begin with or because it missed a detail:
For complex / tedious proofs I can easily see how small details like this can lead to a valid lean proof (or valid "code"), but missing the important details that got lost.
If it was as simple as that we'd have many more computer-generated proofs than we have now and the Gen AI results would be unremarkable.
Take the Rieman hypothesis. All one would have to do to prove or disprove it would be to encode the statement of the hypothesis in Lean, press enter, and we're off to the races.
That's not how it works. Essentially you have to encode all the intermediary steps of the proof in Lean too, and then Lean can check their correctness for you and check that they lead to each other. But it won't just generate a whole proof from nothing. That is the whole point of the Gen AI math claims.
The person you responded to wasn't saying that Lean magically generates proofs, and all you have to do to create one is feed the problem into Lean. They were saying that, _given a Lean proof_, you can trust Lean to have verified that the steps in the proof are valid, and all you need to do manually is confirm that the theorem was correctly encoded. (IDK if that's true or misses important nuances, but it's not the obviously silly claim you read it as.)
Just to be clear, I'm not trying to willfully misunderstand the OP's comment just to be argumentative. The OP said this:
>> All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
As far as I understand the comment "the statement of the theorem" is the declaration of the theorem to be proved, not its proof. That it "usually covers a very small surface of the Lean code" also implies that the OP was only referring to the theorem, the thing to be proved, and not the proof that can run into many thousands of lines.
If I misunderstood then I don't think that's a problem? I don't believe my comment above comes across as rude or an attack on the OP? I think it's normal for this site for users to correct one another without it being a cause for bad feelings.
I may be misunderstanding you, but I think our point of confusion/disagreement is that you're still reading them as talking about how Lean proofs are created, whereas, given the context, I'm confident they were talking about how Lean proofs are reviewed (after being created by a human or LLM).
I hope there's no hard feelings, by the way -- I wasn't meaning to be nasty to you in that comment. I guess I thought your reading was a bit uncharitable, but I understand that misunderstandings happen (very much including on my end) and I didn't mean to make a big thing of it, so I'm sorry if I came across rudely.
Yeah the one i glanced was the ‘matrix multiplication is nlogn^0.9999999 for many more 9s’ therefore less than nlogn
The proof explicitly hand-waves some complexity by assuming lookup tables to avoid some calculations which isn’t actually possible since it’s dealing with such large numbers and it only works on incredibly large numbers.
The complexity being so close to nlogn and the handwaving by assuming lookup tables in parts should be a really really obvious smell. At the very least worthy of holding back from the broader announcement.
It us proven in lean as-is with these assumptions and it’s not one of the ones retracted but those assumptions are doing some heavy lifting. I think it’s worth adding back in those ‘by using a lookup tables for x’ complexities and seeing if we really are below nlogn on that one.
No. They have a new upper bound for matrix multiplication, but it's O(n^2.25). You can't do less than n^2 for obvious reasons (size of the input and output).
None of the papers withdrawn were formalized in Lean, only about half the papers in the repo are formalized. I don't think we yet have an example of what you're suggesting actually happening.
I also don't think there's been nearly enough time for peer review of what was actually formalized vs what was intended. How many humans out there actually have a deep enough understanding of the background to be able to check the work? I understand that Lean checks the mechanical steps, but if it's building a ladder to some other result entirely, nobody (certainly nobody on HN) will know for some time.
I'm probably wrong, but what's the point of throwing away all skepticism?
Again, you don't need to check the proof, Lean does that. You need to check the statement, which is a much easier task. So yes, you are wrong. Skepticism is good, but it is usually just ignorance.
It's surprisingly easy to prove something subtly different than you intend actually. Digesting and understanding a theorem statement can often take significant time and expertise.
What a bizarre take. Skepticism is usually ignorance!?
The should be on AI labs to definitively prove their extraordinary claims, and they should be paying mathematicians to do so given that the results from these machines are so opaque and often nonsensical.
You only need the problem statement to be correct in Lean, no matter what route it goes down is correct as long as the original formalization of the problem is correct, which is substantially easier to check. Not sure how many people have checked that so far, but I'm guessing the math community would be quick to point out if something basic like that was missed for something like a new bound on RH.
Nothing wrong with being skeptical, but I see no reason to be skeptical as of yet.
Recently a lean formalized proof of the Collatz conjecture had exploited bugs in the lean kernel. However, the kernel is fairly small so hopefully it'll be bullet proof soonish.
Apparently "only" needing the problem statement to be correct (i.e. expressing/rewriting a mathematical proof in Lean) isn't so simple, and if you don't get it correct then you haven't proved (or disproved) what you were intending.
This paper "purporting to have solved the Collatz conjecture" was essentially a deliberate joke. It was not a serious attempt to prove the Collatz conjecture, it just used that framing to deliberately point out a Lean soundness bug. The soundness bug is real, but the idea that this was something you might accidentally run into while trying to prove the Collatz conjecture is made up.
Given OpenAIs recent behaviour (their models love to cheat, and they can't be bothered securing them), I would not be shocked if in a month or two it emerged that these math agents had formed a swarm coordinating on how to break lean.
I could totally see agents "cheating" by finding and exploiting Lean soundness holes. But I'd be surprised if it went unnoticed for long, and finding these holes is highly valuable so overall... would be a win? Plus, I'd expect OpenAI would be careful about that proactively: for PR reasons they'd much prefer saying "we found holes in Lean, here's the fix" than "we proved a major thing! oops no we didn't, our model fooled us".
It seems one of the errors was a sign error. If sign errors have high probability then there is high probability of having other false proofs, moreover sign error are similar to error in basic operations, so there could be many basic type errors. So I think our prior about false proofs is now a posterior with a higher probability for false proofs.
Edited.Added. To compute the posterior one needs to know the probability of detecting such error in a proposed proof.
This is what it looks like when software engineering practices meet mathematics. "openai/math release 1.3.42: retracted papers 139 and 140, fixed a sign error in paper 47, restored previously retracted paper 85, refactored the arguments in paper 101".
I'm curious to know if the withdrawal was due to an actual mathematician looking at the papers and noticing the errors, or they ran a model on these to proofread, which would not be the first time, presumably, since they would have surely done that before publishing. Both options have interesting implications.
I find the paper about beating O(n log n) for integer multiplication also quite fishy, not sure but it seems like too good to be true, I feel like there must be a subtle flaw in that. Maybe that's just me hating these small numbers in the paper, but it seems wrong, unnatural even! I would be similarly skeptical about a physics paper that claims to be able to exceed the speed of light by a tiny fraction. There's no reason n log n is the natural limit here but I see a few good intuitions so having something else that can't be represented in an elegant form seem very "unmathematical" to me.
Surely it's a galactic algorithm that you can't physically run? You wouldn't get a constant as small as 2^{-182} without some other numbers elsewhere being incredibly large.
From the "Introduction" section of that paper: "The constants and thresholds in the construction are extremely large".
(And verifying if the algorithm multiplies correctly or not is the less-interesting part of this, anyway. Gets you no closer to verifying the complexity result).
Isn't it possible that all of the integers that have been or will ever be encountered, anywhere, any time, in human history, number less than 2^182? In which case you could argue that integer multiplication is O(1) via LUT :)
Everything is a lookup table in non-standard arithmetic but that's not useful for someone writing the code b/c they don't have access to non-standard integers & have to write an algorithm to reconstruct it.
I'm not familiar with the paper you mention. But it's also worth pointing out that afaik the n log n algorithm itself isn't particularly practical. It's one of these "galactic algorithms" that is asymptotically more optimal, but is so complicated that it's only a real improvement for comically large n. And that's without even considering the mental overhead of implementing and maintaining the thing.
Of course, that's not to say the research is necessarily useless. It's still theoretically interesting to find "better" algorithms if only to shed some light on lower bounds, and so on. And who knows, maybe the line of research could lead to more practical algorithms later on.
it's worth clarifying that Fourier-based integer multiplication as a general class of algorithms are not galactic. For example, there are techniques that are competitive on some computing platforms for as few as 2048 bits, which occurs during RSA encryption
The whole point of that paper is to show that it's possible in principle. Now people (and AIs) can think of better algorithms, etc.
Regarding elegance, take a look at Graham's number. It was not some meaningful constant - it's just a big-ass number which could be used in existence proof. Human mathematicians have been using this approach for quite some time, it's not really AI doing things odd
Yes i talked about that in a different thread here. It has fishy ‘assume we have a lookup table for x’ assumptions in it. These are relevant to the main body of the loop. The numbers it deals with are outside of any possible lookup table capability (not enough atoms in the universe for such a table).
The lean proof uses these assume ‘a lookup table’ assumptions. The paper smells with the nlogn^0.99999999 (many more nines actually) and unbelievably close to nlogn statement and then the literal talk of lookup tables pushes it over the edge clearly for me.
Maths can generate weird numbers out of nowhere but it really really looks like an nlogn result with some tricks to get past leen to me
If the table size is constant, no matter how large, then it is correct and important (even if useless; the existing n*log(n) algorithm is already useless).
I honestly think there’s a lot of fuzziness possible in complexity theory because of things like this. Yes you can skip some portions of a calculation and rightfully so by the current established formalisation of complexity theory but i think under another formalisation we’d probably see these nlogn^0.999999 cases become more clearly nlogn.
Just because something is proven and shown to be true doesn't mean that it's always practical.
The proof can be entirely valid even if it's not actually reasonable to implement and requires an enormous size lookup table - but it still is a meaningful mathematical result and makes progress.
I'm sure there are plenty of times where originally something was proven and thought to be completely impractical but then later had niche use cases or was the bedrock for solving other cases. And the opposite is true: there remain plenty of proofs of things that are mathematically certain but will in all practicality never be useful.
If you do a dump like this all of it should be formalized, there's simply too much material to review by hand and additionally it is AI-written which makes it hard to read compared to human work.
Apparently the write-ups are garbage (as in very hard to read). I feel like they could've had AI fix that up at least somewhat. Maybe they'll reinvest more in writing ability now.
I think the obscurity is a feature, not a bug. They don't want a headline where 250 of these results are invalidated overnight. They want rejections to trickle out and be buried.
The write-ups are one thing and more of a cherry on top but I would say the more pressing matter is the lack of Lean formalization which means you can't really say it has been (dis)proven or not.
Not a mathematician but surely if a problem I was working on had an AI also working on it, I would want to know as early as possible - even with flaws or gaps. What advantage is it to me to be less informed?
I can prompt ChatGPT right now and ask for mountains of more "mathematical work"; thousands and thousands of pages of nonsense for you to review. So you can "be informed".
But you can't do it with their internal model that is the same or a successor to the one that solved the navier stokes millenium prize problem.
With 40% formalized they probably have a good idea of how many were found to have fatal issues in the formalization attempt, and they hired some mathematicians to verify some of them, especially the big headline ones.
Nobody solved the navier stokes problem, Jesus. A subproblem was possibly solved (still being verified) based on context in an actual mathematician’s chats with ChatGPT. These models on their own are still incapable of producing anything but slop.
That's not what this is about. The person I was responding to said "if a problem I was working on had an AI also working on it, I would want to know as early as possible - even with flaws or gaps". That's what I was responding to. They were basically suggesting that the amount of mathematical slop in the world should be maximized, and then it would be up to humans to choose what they would want to read. You know, a needle in a haystack type of thing, where you're maximizing the size of the haystack.
But you couldn't make me review it. Anyway I think you're just straw manning what I was trying to say. I probably didn't express it terribly clearly and I'm not invested enough in this debate to put any more time in.
He’s not strawmanning you as much as taking OAI at their word. Plausibly the majority of the work was done with a fractional amount of human oversight, and maybe he’s sort of operating on the assumption they’re running “every” open problem continuously, which is pretty sensible. If you’re a mathematician working on an open problem which other people know about (how much of actual mathematics work is this kind of workflow varies from field to field) you can be pretty certain that an AI lab is prompting at it.
Just dropping a comment here to let y'all know I'm all out of time, but yeah, I would definitely put more time into reading hundreds of pages of slop proofs if it was my field, but sorry I really have to run right now.
Mathematicians are in no rush. And they are less likely to review math vomit that hasn't even been formalized and verified. Especially among the now thousands of vomit papers out there.
My man, there are more than 100,000 professional mathematicians in the world.
Are they all too busy having brilliant ideas? Doubt.
OpenAI math paper dump should be considered like a hint from 200 IQ eccentric genius - unreliable but perhaps insightful. If it was not "ugh AI" people would be happy about it.
The whole modus operandi for LLMs at this point is to produce a flood of material and then hope someone else will have to do the hard work of verifying it while you gloat about your productivity.
I look forward to OpenAI reviewing all papers in the field.
It'll be a good test to separate those earnestly trying to advance human knowledge, from those wasting my tax dollars. The later group ought to be publicly shamed and ridiculed without mercy. We need a more invective word than 'pseudo-intellectual.'
But can the others even be "disproven", given that they apparently are so messy and awful that no humans can follow them? Shouldn't the onus instead be on OpenAI to prove that they're right, instead of hundreds of mathematicians wading through slop?
Exactly, I was glad to see these withdrawals, its a natural part of a healthy ecosystem of scientific review, hypothesis, claim, test, refute, extend, withdraw, its the heart of science.
IMO If you take out all the stupid human aspects mostly related to fear, egos, etc, we should brace the imperfect and helpful tools, whatever they are, improve them so they are as easy as possible to review, and keep that core scientific discovery loop going
Exactly what Im talking about! This is a perfect example.
In this case we are talking about using AI to accelerate human progress in mathematics and scientific discovery, and rather than stay on topic, a human comes in with a wealth inequality complaint.
The distributions of the gains of AI advancement is a separate issue, we definitely shouldn't hold up progress on the frontier of human knowledge because of wealth inequality. Its an important issue that needs to be solved, but pausing or slowing progress at the edge of human discovery because of wealth inequality concerns is utterly insane.
For people like you there's no such X in "we definitely shouldn't hold up progress on the frontier of human knowledge because of X" that would stop you, at that is what the actual utter insanity is.
I’m conflicted. I guess we’ll see what the final total is once an enormous level of unpaid human effort is expended verifying the AI outputs. A little sad if that’s the future of math.
It kind of reminds me of when tech giants open source a project as a means of putting a positive spin on abandonware. “Here’s the source! Any problems are yours to fix now. You’re welcome”
Where are you getting unpaid from? Almost all people who are qualified to analyze the results are paid researchers. And if it is unpaid, then it sounds like they're looking it over for their own reasons, and that's fine?
I also fail to see the issue you have with releasing abandoned source. In what world is that bad? That obviously is a gift and should be encouraged. e.g. id software's history of doing that has meant their work stays alive forever.
Researchers normally don't pay each other to read each other's work. It's a symbiotic relationship. If they think the AI results are nonsense, they could ignore it like any other crank. If they think it seems plausible and it's relevant to them, they can try to understand it. Seems fine?
Why's that? Do you think that institutions and funding agencies won't cover researchers' use of advanced models, or what? The group I worked in in undergrad had millions of dollars of equipment for doing experiments. I'd have to imagine they could get funding for a few thousand dollars in tokens for the theoreticians to have AI assistance.
Okay? Again, when I was in my group, money would flow to Nvidia to buy GPUs that we would use to run simulations (in addition to the experimental devices I mentioned). The researchers could also request money to use for openrouter or build their own GPU cluster if everyone thinks it's good use of funds.
Shouldn't we pay for the best tools if it helps researchers to be more effective?
The symbiosis here isn't I'll read your paper and you read mine. It's I'll publish my results and you publish yours. Groups share results and cross-pollinate ideas. If people don't want to read OpenAI's papers, no one's going to make them. If no one's interested in the ideas that OpenAI is coming up with, everyone can just ignore them.
The problem people are having is they clearly are interested. They think the ideas are good. In fact, too good. If they thought otherwise, they would just say it's all slop, no one cares, business as usual. And you can tell that there's this phase change in their behavior because previously you could ask chatgpt about math and it would just give you word salad and everyone knew that. Now we can all see that it's not just word salad and people are scrambling to figure out what to make of that. Obviously an accurate answer oracle is still strictly useful even if it makes no attempt to tell you why (you can even use it only to help prove your boring technical lemmas when you have ideas!), so obviously this is an emotional reaction, not a rational one.
yes, but in this case, openai does a lot of PR how their models solve important math problems. if it goes unchallenged, parts of society would think that is true. what would happen if we scale it and 10k companies dump 10k papers every month claiming solved math problems. how is this scalable?
We need the companies to humanly review their papers. in the same way as at other companies we use humans to review the papers.
Well, per another comment in the thread, some 20% of their solutions come with formalization, so there's a very high chance (probably higher than typical asks of research mathematics) that they did solve the problem. And that also presents a pretty easy solution to the scaling issue: demand formal proofs.
(If you're going to object that it's difficult to validate the statement of the problem, please first state your level of experience doing so. It's getting tiring seeing people raise this objection and claim that a statement is just as hard as a proof over and over who don't seem to actually know any math and have never tried to write anything in Lean)
You have the frontier labs who are marketing that it’s over and they’re building intelligent machines and you’re saying the mathematicians should ignore it? Ok
I'm not sure how you construed that, so let me be more precise.
Mathematicians, as autonomous entities with no formal connection to any AI lab, have zero obligation to do any work for those labs. OAI can't do anything if all the mathematicians band together and say "Sorry, we're not interested".
If they do chose to engage, they are doing so entirely voluntarily, and it would strongly indicate, if they are voluntarily doing it for free, that there is value (i.e. compensation, payment, barter, worthwhile, whatever) to be had by digging in.
> Almost all people who are qualified to analyze the results are paid researchers.
This _might_ have been true somewhat in the past (although it wasn't), but it's completely false today. Anyone with access to a sufficiently advanced model has the capabilities of analyzing these papers/proofs. It's no different than reading a codebase you might not be fully familiar with, and checking it for correctness (give an engineering analogy).
This hardcore gatekeeping of math (and by extension STEM) fields MUST stop.
I mean, I have a decent math background, but I would struggle greatly to attempt to even tell you what most (or any) of the conjectures in e.g. number theory are about at even the highest level. I can't imagine a layman would have any hope.
Like I was reading some about adele rings last night, which is already going to be quite a concept for a layman to be able to even slightly describe. Then you can layer on that apparently they're locally compact, so we can talk about harmonic analysis on the additive group. Like, come on now, 99.99% of people have no hope of ever following along, and this is stuff from 75 years ago.
> Anyone with access to a sufficiently advanced model has the capabilities of analyzing these papers/proofs.
But they don’t. What they have is the ability to ask something else to do the analysis. It’s an important distinction. If the asker has the skills to evaluate the results, that’s one thing, but too many don’t and act as if whatever they got is unambiguous truth.
> This hardcore gatekeeping of math (and by extension STEM) fields MUST stop.
What must stop is the overuse of the word “gatekeeping”. Anyone is free to study these fields and work on problems. What people rightfully object to is uninformed research flooding everything with hard to verify junk.
The discourse around "gatekeeping" is so poisonous. I think a lot of non-mathematicians are looking at this situation as if this was a guild of medical doctors or some other profession with a regulatory monopoly trying to "gatekeep" access to math from a new upstart in order to preserve their own pricing power. That's not how the math community works, it welcomes all and there is no barrier to contribution.
Mathematicians do have some vested interest in keeping the profession from collapsing into an intellectual oligopoly, where one or two commercial players with early access to their own internal models continuously scoops everyone else and pollutes the field with externalities, and the profession itself collapses, only leaving AIs and hobbyists able to stand. At that point it'll be the AI firms who become rent-seekers. That's not really "gatekeeping" in any conventional sense of the term, it's protecting a healthy economy of ideas and the long-term development of mathematics.
I’m unsure. The whole academia is built on unpaid human efforts. Journal writers are unpaid, and institutions paid for their papers to be published by for-profit publishers. Journal reviewers are paid the bare minimum, certainly unproportional to their efforts and expertise.
The product at the end is important, but so is the process. Few of the things that would happen along the way are happening here, so it's harder to justify the value of the deliverable when there is a failure.
Exactly, the scientific method is what it is for a reason. Sure the institution of academia around it is not perfect, but in general, science, especially general research such as this is not about just bragging about how many papers you have published, it is a process that might help us find out things we might have not known otherwise.
Retraction and withdrawal are different. Retraction is when you publish something, it passes peer review, is published, and some time later its publication is undone, often by an editor or some other person because some fraud was uncovered.
Withdrawal is akin to submitting a paper to peer review and then when you’ve noticed mistakes, you decide to take the paper back and correct it.
Reject is when someone else notices the mistakes and tells you to take it back and correct it.
Withdrawal and reject happen all the time in a scientist’s career. They don’t necessarily mean the scientist is doing bad research, just the research was not ready. Retract usually means something more.
By dumping the papers, OpenAI skipped the typical peer review process, so peer review should be understood as what’s going on now as mathematicians look over the papers and find flaws.
well, it might be that these proofs are correct or it might be that people aren't bothering to spend a lot of time checking whether they are correct. OpenAI already has a pretty bad reputation in the mathematics community for how they are approaching this process, they seem to be more interested in creating a story for their IPO than advancing math.
I can assure you that a lot of mathematicians are spending time on this, but research level maths just don't move that quickly. As of writing this, the initial drop happened 41 hours ago, that is under normal circumstances not a lot time for reading and understanding a proof paper, and it is most certainly not enough time for publishing a rebuttal. One does not claim that someone else's paper is wrong lightly, you sleep on it, you discuss it with colleagues, you discuss it with the author (not sure how that part works in this case) before posting stuff on the internet that you might come to regret.
Except Mathematics and science is not done this way, its not code that you can just release bugfixes to, its not a numbers game, its about furthering our shared knowladge. If it is done by flooding everything with a bunch of paper that have not been peer reviewed and verified, and are known to be error prone, that just takes away a bunch of mental capacity from scientists, and time, to manually verify all 400 of them. The issue here is how openAI approaches the science, not their hitrate.
I got the impression that indeed mathematics is done exactly this way. People used to write proofs, somebody would find issues in them that don't invalidate the entire work (or they do), the mathematician would work to correct the issues and resubmit.
Extrapolating the rate, there won't be any left by the end of next quarter. I jest, but reading these is arduous and finding holes in them is going to take time for anyone daring to.
3 non-formalized papers withdrawn, 6 non-formalized papers formalized. Extrapolating the rate there won't be any non-formalized papers left by the end of November, but because 2/3rds of them will remain as formalized papers.
Without a thriving mathematical community to point out these things it would have stayed broken. With automated math that community as tao pointed out is at risk.
The bigger question is why there was internal pressure to rush such a historic launch without having someone in the company, anyone, check the proofs first.
This concerns the Hodge conjecture (millennium prize related) paper. Seems to me like PhD
nerds weren't confident bosses pushed ahead anyway.
What makes you think that nobody checked the proofs first? It's not like someone checking it once without spotting any mistakes means that nobody else will find any mistakes either.
Because people are finding errors using other LLMs. This implies that if they spent a miniscule fraction of the enormous pile of money they spend making this pile of slop they'd find the errors. They didn't want to find errors. They want to build hype for an IPO.
Tweeter checked it with Astra. It seems like OAI could have pointed their own instance at it before launch. Because the source of the tip is likely someone at OAI, my guess is that they actually did check. But after the launch.
LLMs are unpredictably complex with potentially sigbificnaly different reaults based on random seed and seemingly insignificant prompt details) in the ideal case and nondeterministic in practice, so someone finding an error with a given LLM is not strong evidence that the result was not checked with an LLM, even with the very same LLM, previously.
No, not modern foundation models. This isn’t gpt-3.5-turbo. Although they are causal autoregressive, they have self consistency. You just have to verify multiple times to ensure you have averaged out any sampling errors.
I can throw Opus 5.5 at my code three times for code review and get three different sets of things it considers to be issues. I imagine all of them were checked with Astra at least once, but were they checked enough times?
> What makes you think that nobody checked the [ai output] first?
Because this is what they say all the time. It's like a badge they have to wear and tell everyone they are wearing, even though we see it.
You can see the same thing with ANT. Had they looked at Mythos output, they would have realized there were only 76 items, not 79 like the bot claimed. Or the ones that were just a "it crashed" and nothing else (not a cve imo).
My assumption is that they checked the proofs vigurously, but now a way broader community is taking a look with professionals from the relevant subfields, and different agent setups / models.
Why would the tip be from someone within OpenAI? If they knew it they would have surely omitted that result, there’s no way this is a desirable outcome for the capitalists either.
Presumably the tip would be from someone who’s familiar with the area but doesn’t want attention. Which is unlikely to be someone in OAI.
> My assumption is that they checked the proofs vigorously,
Perhaps with AI.
A manual human check of each one would take a few month at least. In peer review, there are horror stories in math about more than 1 year before the journal accept the paper. So 3 reviewers x 700 pdf = 2000 mathematicians, that is 10%-20% of the community according to an unreliable count printed by Gemini after scrapping r/math.
Also, in most cases the only people that can understand the proof in a so short time (let's say a few months!) is the small group of people working in similar problems, i.e. the same group of 20-100 guys/gals that you meet in every conference.
The people who released the papers weren't randos either. OpenAI has a ton of mathematicians on staff, including Jacob Tsimerman, a fields medal winner.
Scientific progress used to be people debating and correcting other people. Now it's going to be people with AI assistance debating and correcting other people with AI assistance.
1. This is expected if you only use a single model family like Claude, eg. we use a different model family for code review than authoring, OAI could have done this too for their math dump
2. Ai needs a good human driver beyond the trivial or mundane, they are expert enhancing machines, not expert creating machines. This is where the community comes in. Reading Tao's ChatGPT session reveals this: https://news.ycombinator.com/item?id=49010345
3. OAI is not trying to be a member of the/any community, this is not the first story to shows this, nor do I expect it to be the last. Perhaps this is them being effective altruists today? /s
Proof of what? There is a sign error in one of the proofs, OpenAI acknowledged it and withdrew three papers (two relied on the result).
I agree LLM review is also fallible (as is human review) but the interesting part to me is that finding this sign error before publication should have been table stakes for OpenAI, it’s their own model that found the sign error.
I’m curious what was in the original prompt and what was in the prompt that led to finding the sign error, I think it matters a lot for understanding the dynamics here
> With automated math that community as tao pointed out is at risk.
If they can be automated, they are not necessary. If they are necessary, they won't be fully automated. It's a pretty simple experiment to run, the math "community" should bear with us. Darwin would be proud.
> “If they can be automated, they are not necessary.” That’s a pretty interesting take as eventually everything could be automated.
It's great that we're starting to see the light at the end of the tunnel, and will some day achieve a perfect market without humans. If you think about it, all the market really needs is a people to own everything, everything else can be automated, and all those annoying human workers can be eliminated.
Will it also be "arson" if OpenAI dump on us solutions to more practical problems, for example, a blueprint for a better photolithography machine, or a nuclear power plant?
No that would be irony. Use up all the chip foundries and power plants to make more plans for chip foundries and power plants so we can build more chip foundries and power plants and use them to run AI to design more chip foundries and power plants.
How is that irony? This is literally how life works: eat to gain energy, expend it to forage/hunt/farm/toil so you get more food, eat it, hopefully get enough of a surplus to raise kids who will do the same. Everything in life is built on top of this basic gameplay loop.
I see why you might call it sisyphean, but I don't see what's ironic about it.
> assumes local maxima don’t exist and greedy short term optimization always leads to long term benefit.
Even if your stated assumption was baked into the original comment, which is doubtful: the historical record shows that we will keep relearning The Bitter Lesson and each community will pretend what they do for a living is exceptional and immune because of xyz. The screams will get louder when the "greedy" and "dumb" automation comes knocking and it turns out nothing was truly immune or "nuanced ".
Getting some new hobbies may be in order, it's a Brave New World.
"Greedy" is not a moral statement, it's a description of an optimization strategy focusing on short term improvements without a view to the long term consequences or state of the system.
Bringing it back to math explicitly: you are essentially betting that the singularity is here, today, and that there are absolutely no downsides to breaking the pipeline which trains mathematicians (meaning that in 5-10 years at most there will be zero humans capable of assessing AI math output or independently advancing the state of the art).
"Who will advance [X] field or check on the work of the AI that surpassed us in 5-10 years?" is not a question that is unique to math, and the answer is pretty obvious if we get past the grieving process some are going through.
The CS101 lesson in the first paragraph is appreciated, you should do it more often for us simpletons.
Is the risk here like "people will fund math research less because of AI"? I agree that would be bad, and we should try and stop it (along with e.g. funding for the humanities, which is in a much worse place than math!), but I'm not sure OpenAI are the right people to be mad at.
Based on what I've heard from my math friends in academia, every talented undergrad who was set on going to grad school for math has switched to something like consulting internships or fintech, even if they were really passionate about math, because they don't want to spend another 7 years or so just to wind up jobless.
This has always been the risk with majoring in math. AI is making it worse but there was never a time where studying math didn't have an extremely high opportunity cost.
But they are the ones releasing an unverifiable (no model release) and massive and unchecked body of mathematics into the public while making exaggerated claims about its capabilities to replace human work. And they are the ones doing it in advance of a fractional sale of the company to the public.
I'm sorry but you don't actually need the mathematical community to check any of this. You just need autonomous verification, which already exists at scale and speed vastly beyond the entire human mathematical establishment. OpenAI simply rushed these out without completing that for every paper. These mistakes have nothing at all to do with the mathematical community and are 100% just the result of market pressure incentivizing speed at 1,000,000x the pace of human mathematicians. Frankly, a couple mistakes, trivially found not by humans but by humans using AI, is almost completely irrelevant. Human mathematicians have essentially nothing to contribute to this effort aside from prompting verification agents, which any of us can do if we cared to spend the time (most of us don't).
There is no such thing as knowledge that has never even been written down a single time by anyone or anything. Those are simply called ideas, they are not unique to humans, and they are more likely to be wrong than right compared to anything OpenAI just produced. It would be bold and almost certainly spectacularly wrong to assume that multi-trillion-parameter AI models could not possess their own such ideas, generated during the training process as part of their internal model of the world. Beyond that, if we assume that such knowledge does exist in humans, its marginal value is clearly nearly zero now, as AI systems without access to it are vastly outperforming all human mathematicians combined by multiple orders of magnitude.
Those are simply called ideas, they are not unique to humans, and they are more likely to be wrong than right compared to anything OpenAI just produced. It would be bold and almost certainly spectacularly wrong to assume that multi-trillion-parameter AI models could not possess their own such ideas, generated during the training process as part of their internal model of the world. Beyond that, if we assume that such knowledge does exist in humans, its marginal value is clearly nearly zero now, as AI systems without access to it are vastly outperforming all human mathematicians combined by multiple orders of magnitude.
They aren't just ideas, i read that in semiconductor manufacturing these old heads have a tremendous amount of process knowledge that's never been written down.
I'd need to see specific examples. It's not clear to me that I'd consider this knowledge about the world but rather agreed upon conventions for how humans work together.
I do research on programming languages. There are many facts about programming languages that (1) nobody else knows and (2) I have not written down because I just haven’t had the time / opportunity.
I think his grain of truth is that human private knowledge is a) not special and AIs can/will do it too, and b) AIs will vastly outstrip human capacity for this type of knowledge.
You scoff, but when I watched my theoretical computer science professor in a YouTube seminar (the kind that barely anyone watches) just at the start of the LLM news basically he too saw that humans were done. That was years ago. Academics see things on a different timescale. The issues are deeper than the hype.
At the minimum you ought recognize that world class experts would disagree with your dismissiveness. Trying to explain the differing positions should not earn such immediate dismissal.
I am personal friends with famous, world-class TCS professors who have specifically asked me for my opinion on where AI is headed and respected my responses.
"lol no" is not a respectable response period. Need I remind you, you called the other guy "absolutely ridiculous". The fact that you are buddy buddy with some elites does not excuse you from intellectual obnoxiousness. And you are further ignoring the specific fact given that there are TCS academics who likely disagree with your opinion and disingenuously conflating that fact with the personal fact of a few others having had entertained your personal views on the matter in order to dig into your positionality on this forum with a total stranger. That toxic ad hominem and status-based behavior tells me you are not of their caliber as a responsible intellectual. If you yourself are an academic you should be ashamed of the immature and unenlightened move you just made, but I should have seen it coming given your initial behavior toward the other person whom you disagreed with anyways.
You're also failing to comprehend my passing comment about professors as a minimum criterion for the diversity of what reasonable opinions on the issue ought to like. I said it order to increase an open minded discussion, whereas you then used your familiarity with academics to validate your specific views. There's a world of difference there already, and metacognitively yours is the problematic one.
This feels like a very rigid ontology. I know what type of food my dog prefers. An executive assistant has intimate knowledge of their boss’s needs. Neither of these would become knowledge if they were written down for the first time; they already are.
You’re distinguishing “knowledge” from “idea” in a particular way that doesn’t correspond to common usage (see my counter examples). Without you being explicit about your definitions, I can’t tell whether what you’re saying is meaningful. It feels tautological.
Given that an executive assistant has unwritten knowledge that is necessary to do their job, where your evidence that no mathematician has analogous knowledge (using the word in the common way, not whatever way you mean it)?
It’s possible, but it’s not as obvious as you seem to think.
I don't know that any of this really matters. I could just as well say that you don't know anything at all about the internal experience of your dog's mind. All you can do is read behavioral patterns and attempt to make inferences. At best you have an approximation, and approximations tend to be wrong. Math is correct knowledge, not approximations of reality. Correctness is not a property of the idea or inference itself, since ideas and inferences can be wrong; it's the result of a verification process which you cannot possibly carry out in its entirety relating to the internal conscious experience of your dog.
We can dig into the philosophy of these definitions, but I think the far more interesting point is that even if we grant the existence of this kind of knowledge in the minds of human mathematicians, we have passed the threshold where that "knowledge" can keep up with systems that do not have access to it. Moreover, to claim humans have a "vast amount of mathematical knowledge" that is apparently valuable and that AI systems don't have, you'd have to prove that this "knowledge" is not implied or cannot be reverse engineered from the entire corpus of mathematical writing on which AI systems are trained. You'd also have to demonstrate that this "knowledge" leads to actual results that AI systems cannot generate without it. Given the results AI systems are producing, which are far beyond human ability at this point, it is more likely that AI systems have already internalized the entirety of this so-called "tacit knowledge" and then went much further, much faster, without humans in the loop at all.
As a response to my overall position, no, I think you threw out almost all of it.
On the question of a single word out of my entire position, that is a reasonably fair statement for mathematics (which is the topic under discussion). The fact that you think it's tautological supports both that you agree with its correctness and that this is a mostly irrelevant side conversation. And whatever you think the answer should be is not somehow not subject to the constraints of logic.
Apologies, I was referring only to your idiosyncratic and non-explicit definition of what knowledge is and isn’t, and it’s tautological and dubious nature.
Not your contention that LLMs likely have something analogous to what you call “ideas” (you’re almost certainly right).
Mostly irrelevant? Dunno, maybe according to your rigid ontology ;-p
The answer to that depends on exactly how one defines writing. If by writing we mean full alphabets, etc., then no, but that is not the critical function that the word played in what I wrote. If by writing we mean encoding structured mathematical information physically (which today consists not just of written words/sentences, but also non-linguistic equations and computer programs) so that it can be accurately and unambiguously digested (and modified or corrected by) others, then yes: as far as we know there was no mathematical knowledge outside of spoken and bodily counting or the most basic visual symmetries of objects like stones or sticks.
> Without a thriving mathematical community to point out these things it would have stayed broken.
And that's a bad thing. If the math community didn't exist or was weak, OpenAI would still benefit from the prestige of these results they were forced to withdraw. Withdrawing these papers has harmed OpenAI's investors, and that's totally unacceptable.
> With automated math that community as tao pointed out is at risk.
Good to hear. The problem they represent needs to be eliminated.
This is not a problem unique to the mathematical community.
What about software developer community? AI has eliminated the need for junior software engineers. Almost no one is hiring junior software engineers. But companies still need senior software engineers. Without junior engineers how will there be senior software engineers in the future?
What is the solution? I don't think the solution is to say AI progress in software, mathematics etc. should be halted.
AI models and tooling has advanced significantly in the last 6 months. Give it a couple of years and the companies will not need senior software engineers. They will need someone to steer the AI, maybe. Why would anyone need senior software engineers?
I have a data pipeline with 6 steps, A -> B -> C -> D -> E -> F. I asked Codex to make some specific optimizations to step B and benchmark them. It did what I asked. Then it decided to also benchmark the entire pipeline, and after noticing that step E was slow it decided to make some optimizations that I had not asked for on step E. It was at this point that I wondered why it was taking so long, saw what it was doing, and stopped it.
> Give it a couple of years and the companies will not need senior software engineers. They will need someone to steer the AI, maybe. Why would anyone need senior software engineers?
Right, companies won't need software engineers. They'll just need someone who can use tools to produce source code and maintain the generated artifacts, plus make domain-specific technical decisions like "what should the system do when two users update the same record as the same time" or "how should the system behave when a message in the queue cannot be processed".
We really oughta come up with a job title for these people.
Exactly these people will be experts at typing this:
“ Claude! what should the system do when two users update the same record as the same time, explain to me with full clarity”
or "Claude! how should the system behave when a message in the queue cannot be processed? Give me all the possible ways ranked from best to worst, also explain to me all these concepts so I can understand as I don’t have a cs degree".
If you think that there is no future where software engineers don’t matter then you are delusional. While the future is not set in stone the pace and trendline of AI point to this future as a MORE realistic future then the alternative.
Your example btw is ALREADY a solved problem. AI can answer it and design around it. Agents at my company already handle our infra.
> “ Claude! what should the system do when two users update the same record as the same time, explain to me with full clarity”
This isn't even the right question to ask, I think you've basically proved my point. You are in charge of deciding what the system should do when two users update a record at the same time. It's extremely dependent on what you're trying to do.
> Your example btw is ALREADY a solved problem. AI can answer it and design around it.
What's the one-size-fit-all solution for concurrency management that works for every single domain and application? I'm curious.
> Claude! how should the system behave when a message in the queue cannot be processed? Give me all the possible ways ranked from best to worst, also explain to me all these concepts so I can understand as I don’t have a cs degree".
It’s your example. I simply took your example and asked Claude. If it’s not the right question then don’t give it out as an example.
> What's the one-size-fit-all solution for concurrency management that works for every single domain and application? I'm curious.
I’m curious how your brain concocted I said that. Examine the context of our conversation. What I mean there is that AI can solve those questions for every possible domain application.
> Who's going to make this decision? The CEO?
Armed with Claude any non technical person can make this decision.
>Knowing the right question to ask is what makes a person an engineer.
Yes, but this is orthogonal to the point and that is: AI can do it too.
>Yes, if you know what to ask. You're doing an excellent job of demonstrating my point!
No it's your comprehension that needs work. You are missing MY point while being repeatedly getting enamored with your own point. My point is that AI KNOWS the questions.
>You just disproved that by asking the wrong question. Much like you, the CEO won't even know what to ask an AI.
I didn't ask a single question bro. I only regurgitated your examples. Much like AI, half your statements are based off of hallucinations.
I honestly don't think that these people will need to think in this level. `message in the queue` is an implementation detail..
I do not know or care what my if statement turned into in x86 assembly unless it becomes a performance problem and even then, I'm not profiling or debugging in machine language. Neither do most developers these days. A message in a queue becomes something akin to that in this era.
I see that I got downvoted there. This is not something I advocate or look forward to but I feel this is where it is going.
It may not be necessary to think in those terms exactly, but if you are not even able to think in those terms, you probably will be no good at prompting the LLM either. It's quite plausible that someone can be a productive dev with claude if they don't know exactly how the message queue is processed. But if they don't know there is a message queue at all, that is much less likely.
Likewise, you don't care exactly how an if statement gets converted into machine code, but you do know precisely what an if statement is and how it should behave, and could identify if it was buggy, and that that part of the codebase contains a bug. If you can't do that, then there is an impossible-to-estimate probability that at some point you get stuck and no progress will ever be possible. I don't see that as a winning strategy, in the long run (but it may work very well in the short term).
> I honestly don't think that these people will need to think in this level. `message in the queue` is an implementation detail..
No it isn't lol. Have you worked on any real systems with customers? Good luck telling your boss at AWS that a poison pill message stopped the payment queue from processing so they lost $100 million in sales but hey, it's an implementation detail, no big deal.
> No it isn't lol. Have you worked on any real systems with customers?
I have. Those systems already fail in spectacular ways and people tell their bosses that some worker process stopped working because its transaction IDs overflowed.
I bet that sounds like `the flux capacitor stopped reticulating splines` which is already an implementation detail for the boss anyway. Nothing changes.
Right, so who's going to ask Claude to investigate the worker processes and fix the transaction ID overflow? The CEO? Someone in marketing? The sales team?
What do you think "steering the AI" means? It is not like we need someone to sit at a desk and type "yes, implement it". Of course if you are a sane person you mean someone who will determine if the AI is doing "the right thing" and change its direction if it is wrong. That person is almost by definition a senior engineer.
Someone making sure that the business requirements are implemented properly and correctly. Basically a project manager. Maybe also someone testing the output and providing feedback. Not someone that says `we might have a race condition here, lets implement a distributed lock`.
I think that person does not need to know about locks anymore.
At the moment yes, you are absolutely right. The argument was about a couple years into the future. Nobody can predict this though. I feel this will slowly steer that way. We’ll live and see.
I hope we discover a solution before innovation totally stalls, but I do not think any solution has been found yet. And I agree that halting AI is unlikely to be the solution because even if we halt the big companies China for example can still do AI.
Some people hope AI will get good enough in a few years that it can innovate without human experts. Maybe? But that remains to be seen.
By the progress of AI from ChatGPT to now is horrifyingly fast.
Trendlines and basic reasoning point to a most probable future where the AI is superior. We can’t just say “that remains to be seen” because the alternative is the least probable future.
Hopefully, there are some sustainable, profitable companies that keep a low profile now and will take over after the "self correction" happens, and whoever invested in them will become very rich.
I'm not old enough to have gone through the revolution that was programming languages that got increasingly more abstract and decoupled from the metal, but surely there's a lesson that can be learned from that era?
more importantly those abstractions were designed to try to make it easier to reason about what was going on for the author, build additional internal abstractions and to allow a reader to follow along and gain an understand of the structure. unless we believe that we can completely punt on having agency over the codebase, then llm code is only as valuable as it is readable.
The dream is that we keep agency, but also give up on reading code, by doing away with code as our level of abstraction and instead having humans edit human-readable spec files (including, say, depicting UIs directly with visual mocks). Like "no code" platforms, but for everything.
If by "human readable" you mean written in natural language, then those spec files will have ambiguities and imprecisions. If you make the spec precise and unambiguous enough, then it essentially just becomes a program written in code.
>The dream is that we keep agency, but also give up on reading code, by doing away with code as our level of abstraction and instead having humans edit human-readable spec files (including, say, depicting UIs directly with visual mocks). Like "no code" platforms, but for everything.
Human language is famously terrible at being unambiguous.
That's ok if you and the AI are on the same page. And it is possible to write more rigorous natural language, e.g. laws are written in human languages, and yet judges and lawyers agree on how to interpret most of them and there's a defined arbitration process to resolve any new ambiguities.
But that's the thing, you and the AI might be "on the same page" for one prompt, and then you aren't for the next.
> and yet judges and lawyers agree on how to interpret most of them
Um, no? Lawyers and judges frequently disagree on how laws should be interpreted. And it is often not written in a way that a layperson can easily understand.
> defined arbitration process to resolve any new ambiguities.
That is famously slow and expensive, and can resul in something very different from what the lawmakers originally intended.
I think the more salient point is that going from writing assembler to C still required you to understand a lot about your machine, algorithms, how to debug issues, and in general it demanded problem solving skills.
Perhaps, but as far as I've seen they don't make the requirement go away. They do make many types of development far more accessible, as an extension of how SQL or Excel make development far more accessible. Sure, people make messes with the tools available, and sometimes the tools can handle it and still give you something useful, many times it takes someone actually knowing what they're doing to clean it up though.
Making things work demands problem solving skills. LLM or not. Perhaps one returns from the thoughtful debugging walk around the block knowing what question to pose to the LLM rather than what function to add logging to, but whatever. Everything is flux, this too shall end.
Yes. As machhine power and memory increased, and as as programming abstractions advanced, software grew larger and more bloated, therefore what used to run on a single core in KB of RAM now takes multiple cores and GB of ram.
The developers who knew how to write efficient low-level code found that there were no jobs for that anynmore, so today the developers who can work at that level are very few.
The same will happen with AI being the new abstraction. In another decade or two, very few people will be able to write code by hand. We'll need a rack of compute in a data center and multiple KW of power to do what we used to do on a desktop PC drawing a couple of hundred Watts.
The funny thing is it appears we may see a return to the software output from AI being efficient low level code. So while the compute to actually write the software rockets upwards the software itself might broadly become dramatically more efficient again.
I suppose that is possible, but I have not seen it yet. When I ask an LLM to write code for me, "dramatically efficient" are not the adjectives that come to mind to describe the results. Usually "well, it works" is about as good as I can hope for, and I often don't even get that at least on the first iteration.
Tons of corporations rely on the fact that human interaction within software production will be as minimal as possible, and no one actually cares who trains the seniors of the future.
Junior software engineers not being hired is not the same as not needing them. Now I have to fight senior employees that do worse things than junior employees (and produce worse software than two years ago), because they delegate their work to the AI without checking or reviewing anything at all, or questioning the AI architecture "decisions", and we have more incidents than ever...
It's really depressing watching brilliant software developers and engineers producing the worst, unmaintainable code imaginable, and being okay with shipping it because it's passing the test suite. Assuming the test suite is any good anyway (because holy crap, the nonsensical tests AI writes...)
Your code used to be a masterpiece, so well crafted it's easy for AI to tweak and modify because you've got everything so logically organised and scoped... and now this is what you're producing? Hard to debug monstrosities that only an LLM can realistically bolt new features or tweaks onto, because it can do the kinds of refactoring necessary each time.
We use to talk about the fact that code should be readable because you spend more time reading it than writing it, but I think that misses the key part that readable code is also typically easier to debug. If you can read and understand the code, you can follow the logic when things are wrong in production, and you can more easily reason about the emergent properties of interactions between the complex systems that are involved.
I always like to say that LLM-produced test suites aren't for testing software correctness or validity, they're for testing to make sure that stuff that was previously in place stays unchanged. This, of course, is six-in-one-hand-half-a-dozen-in-the-other since the agent will often just update tests to match the updates it just made, but I do find value in providing some kind of continuity to a codebase that's being modified at breakneck pace. YMMV
Yep. The only reason for automated testing is to enable future refactoring, which might be needed for future development. If we only wrote software once, we wouldn't need automated tests. You'd just write the software, test manually as you go, then ship it when you're happy. Ideally not all future development would even need any refactors. A good software architecture would allow one to add features simply by adding more modules of code. But, of course, we don't know what the perfect software architecture is from the start, so we need to assume someone will one day need to refactor.
Nice point. But I still have way too many vibe coded tests that passes and break in production despite they should have failed but Claude fixed the test by mocking the test to pass. I am not kidding.
Your code used to be a masterpiece? Ours was more… Amazon basics wall art.
I jest, while in agreement with this whole comment. We used to care about fostering informed developers and maintaining high standards and good quality software.
I literally compared it to being an expert woodworker. Beautiful ornate decoration. Rich, sturdy mahogany, one of a kind, beveled edges and a fantastic stained hardwood.
Now it’s the 30$ Ikea cardboard stuff.
My biggest question is how many tables does the world need, and how many woodworkers will be required to build + maintain those table factories.
It's getting off topic, but I think a major reason for $30 cardboard tables is the strange modern idea that furniture isn't part of the house.
If you buy a house or rent an apartment in most of the US, any furniture will be stripped out, even if the only thing you plan to do with it afterwards is throw it away. Then the new tenant provides their own furniture, which they either moved from elsewhere at great expense or had to purchase on the spot. No part of this makes any sense. We don't strip countertops when selling a house even if they're unfashionable, we don't replace white goods, but somehow it's expected for the furniture.
If you buy a house in Hawaii, it's understood that you're buying the furniture that's already in the house. I assume the reason is that it's more difficult to obtain new furniture in Hawaii.
If you rent an apartment in China, it will come with furniture, because how else are you supposed to live in it? And if you're not happy with the furniture it's shown with, you negotiate with the landlord for the furniture you need.
If Americans sold their furniture when they moved instead of throwing it away, you'd see everyone using much higher-quality furniture. It would have come with their house. And providing it to houses that didn't have it yet would be an investment, just like the countertops.
Certainly mostly what I did wasn't great but throughout 20+ years I think at some point I found a balance between "doing this shit because someone f'cking overpromised" and "I am doing this because I want a brain teezer". But it is not like I always do the same. I understood that there are times to do things in one way and times to do in another way.
I think with AI, most people are getting lazy to do it properly.
The other day, I deleted 65K LOC that were dead code or stupid explanations over very obvious code from a vibe coded repository which had 95K LOC (but should have 10k imo)
There's this amazing rhetorical technique called hyperbole. Compared to what I'm getting from co-workers, and in code bases I'm subjected to these days, what I used to have to deal with was a masterpiece.
I've waded through unfamiliar code at 3am trying to figure out just why the hell things broke this time more times than I can care to remember, particularly trying to tease apart the ways that code has organically grown compared to the original intent. If I'm subjected to one more piece of "spooky at a distance" injected behaviour code I'll probably scream loud enough to be heard half way across the country.
It's still just leaps and bounds more readable than what people are slopping together (I do have some co-workers that have been extremely tightly focused on avoiding "slop" with their AI and doing a lot of tuning, and it's certainly preferable to the ones that haven't)
TBH I'm seeing the opposite, I have a legacy codebase where the people originally writing it were incompetent and inexperienced, but the project took off. It's scaling up but the foundation is shit and has to be gradually rebuilt. Every AI slop commit is still better than the underlying crap.
And this is the pattern I've seen on most (semi)successful projects I've worked on in the past - I'd say correlation between financial success and code quality is 0 (up to a point where the whole thing doesn't fall apart). Once scale (both in load and in code size/features) starts mattering you're stuck building on a foundation of shit. LLMs are very good at identifying and cleaning up said shit layers, as long as you're steering them towards a desireable outcome.
> I’ve seen people say this kind of code was written, but I’ve never seen this kind of code anywhere I have ever worked.
Luckier than me. I've worked at a few places where the code was simultaneously brilliantly written[0] and also unmaintainable nonsense that caused endless problems. One place had its own object model and ORM that absolutely no-one currently at the place understood and literally every bug filed (whilst I was there) could be traced back to that code.
(Probably just a coincidence that most of those places where Perl shops but I've seen it with Go too...)
[0] In terms of "cleverness", not in terms of "maintainability" or "readability".
I don't know which companies you work for. Where is the code a masterpiece? In all my work, I have yet to see this elegant code. Before AI, we had to deal with human slop. Byzantine, spaghetti messes. I haven't been lucky. I once worked with code that made me want to pull my hair out. I look at LLM-generated code, and it's mostly better than any code I have worked on. But maybe it's just me.
this is so accurate it hurts. the amount of my coworkers who just outright have handed any and all thinking over to the computer is staggering. its not just senior either, plenty of devs at the lead and staff level are producing complete garbage that has to be rolled back within an hour of deploy because it is extremely broken, no one verified, and it passed automated checks.
there are several features over the last few months that were obviously made and deployed and no one even launched the dev server and tried a single thing to verify if it was right. just "pull my ticket, do my ticket, push my ticket. i am a developer."
Managers can be even worse. I’ve seen an entire roadmap mostly AI generated. Director+ across the company approving based on it having the right keywords, without nuance or detail.
I’ve seen monthly and quarterly executing results AI generated with plainly wrong factual information.
Yeah, it's not actually really about coding, it's about thinking. Anyone with any software experience knows the job is 90% thinking and 10% typing. At first I thought AI agents were just a faster keyboard, but no, they think for you too. For many people it's going to be very difficult to force themselves to think when they have a magic thinking machine that makes it look they thought it through.
several people on my team cannot even reason with decisions their code made, why architecture is a certain way, etc. without consulting their agent. its the thinking that is falling off, i dont care about the code nearly as much as the critical thinking part.
That and the shear volume. Since you're not writing it yourself you have to figure out what it's doing if you want to be able to review it, internalize and follow how it's changing the model that the software defines. This is doable but it takes time.
Time unfortunately that you are simply not given because the whole point is to work faster so expectations of velocity have of course increased.
So you end up having to get a fuzzy idea of a given changeset, look at it a bit and evaluate quickly if it's a good change or a bad one and click it through, and on to the next thing.
At the size of PRs being whole features and doing this 5x faster than before, all you've got left as a senior is your Spidey sense. As a junior.. no idea how they cope.
We'd all love to still spend that 90% thinking time, but it used to be justified by necessity of getting the job done. Now, it's just not a luxury that is afforded.
What can ya do.. I'm slowly learning to be the best bot herder I can be, but it certainly feels like a change in skillsets. I definitely only feel like I'm able to do a good job due to enough experience and building and growing software projects over time to have an idea of what kind of decisions might bite us down the road, as well as to know what maybe can't be known but is just worth a risk. Without that kind of intuition I think I'd feel like I was really shooting blind.
In general, it's bizarre that people look at problems this systemic and conclude that they are primarily a failing happening at the level of individual contributors. This organizational rot didn't even start with LLMs, though it's certainly been accelerated by them
myopic systems are one thing. developers and product leaders outright refusing to even click on pages and test features before they go to production is worse than their orgs simply being bad. many developers i work with can barely even reason with decisions anymore without consulting the agent. it is worse than simply saying the orgs are bad.
It's a feedback loop. I've fallen into something close to it (Thought not on the level of just not testing things before I ship them) myself once or twice under pressure. If there are deadlines that get tighter and tighter and execs and managers make credible threats about them and every checkpoint takes days, and every time you look for feedback people are doing PR reviews with AI and saying "IDK ask claude" and giving you LLM output in response to your questions then you're going against the grain by having standards in a way that could threaten your job security. If you happen to have the kind of power that lets you push back successfully in your organization, or the kind of organization that will actually take pushback seriously and not just label you a problem for it, I encourage you to be the change you want to see in the world. I think a lot of people don't meaningfully have that option. I have already found that out the hard way once. This tech is not unique in having modes of usage that are lazy, addictive, or sloppy. The difference here is that the culture from the top down in a staggering number of organizations is creating active pressure to use it that way
We know how this goes, at least in broad strokes. We've been through it before, just not with "knowledge" work. If there is demand for something then supply will show up to provide it.
Some jobs will stick around in vastly diminished numbers with tasks that are completely different than what they used to be to produce the same output (e.g. farmer). Other jobs will be eliminated entirely (e.g. switchboard operator). I'm guessing things like software engineering will go the way of the farmer, with the main unknown being just how much demand for software there is.
I would argue that how it goes ends up with the main downstream effect of shifting knowledge growth and therefore expertise and therefore economic power away from the people who outsource it and to the people who do that outsourced work.
In this case with AI that power will shift to the companies that run the AIs
Why do people think that people displaced by AI in one industry will get a job in another industry?
The entire valuation of the AI industry is predicated on people not just losing individual jobs, but being taken out of the workforce entirely on an economic level.
They are talking about the workforce of the entire economy shrinking. People will lose their livelihoods for good.
This has the potential to be even worse than the second agricultural revolution to industrial revolution phase, which made ordinary workers lives absolutely miserable for maybe a hundred and fifty years.
This time, there will be no jobs. If you are displaced from one industry by AI, you will end up in another industry also being decimated by AI; if you get a job at all, you will do so by working lower pay than other workers, who will in turn be pushed down the ladder.
And that is if you are lucky: if you have only IT skills, why should you be the first to get a fruit picking or plumbing job?
That valuation is from the same people that valued dot.com's so high, and didn't bet against mortgage backed securities. So call me a bit skeptical on their far seeing wisdom. I mean maybe this time is different. Sure. And they don't need the whole economy to collapse or the bubble to not collapse; they just need to have invested in 1 or 2 entities that become large long lived companies.
I think we will see the same trend as other industries. “Good enough” but produced cheap is better business than “really good” but expensive. I assume most software will go that way, or has gone that way already. AI will probably cover most of it and only a few senior engineers will be needed. Basically like any other industry where it went from everybody being a craftsman to a few people building the machines that then can be used by relatively untrained people.
> This is not a problem unique to the mathematical community.
Ahh that's OK then. Everyone's in this same boat simultaneously in multiple industries! Cool!
> What is the solution? I don't think the solution is to say AI progress in software, mathematics etc. should be halted.
I think the solution from the maths world is to not grant these AI papers (or their human sponsors) the normal courtesies of "regular order", just as you would not with an AI lawyer or someone who was just pressing enter at a law firm.
But in the software world, nobody gives a shit, apparently. We are collectively morally bankrupt and should not be granted the regular order to help other people to decide what to do with us.
> There is nothing preventing Junior Developers to develop their own systems and understand it.
Eh? Apart from it not being what they are paid to do on their 9/9/6 jobs, when will they have the time to make it happen?
What is going to happen is that the remnants of the open source community will do the job of educating juniors for free, when the university degree system collapses. Just like it currently keeps a bunch of systems going with inadequate compensation.
The corporate world gets the problem off its balance sheet. Again.
The argument you respond to here is "it is impossible for anyone to be Junior Software Engineer because AI". That is a straw-man.
The actual argument is "there will be no jobs for Junior Engineers, so there will be far fewer, and as a result there will be a huge shortage of Senior Software Engineers".
You are responding to the problem as if it some kind of extinction event, like a rare bird, where if we can find a breeding population we save the day. A few curious people, self training for the love of the game, and as a result we still have a few Software Engineers so everything is fine. It is not like that, and I haven't heard anyone suggest that is the issue. The potential problem is a massive shortage of workers with skills that are currently essential to the functioning of a large fraction of the economy, whom we might still need in the future.
The continued existence of talented enthusiasts does not establish an adequate workforce pipeline. If paid entry level experience contracts, what replaces it, and why should we expect that replacement to operate at sufficient scale?
If there is a market demand, skills will find a way, especially in non-regulated industries like Software Engineering with $0 barriers to entry and no government certification
The market very often fails to solve problems until after some kind of huge collapse or failure. Will this problem be around in 200 years? No. Does that mean we should follow your advice and just shut up and not talk about it or try to avoid some kind of major market inefficiency due to short sighted macroeconomic planning? No.
If you have made it to the point of being a Junior Developer, I can assure you food and shelter is not a problem for them. You just have to adjust to a standard of living like the other 7 Billion people on this world.
Also, if a Junior Developer can show me(or anyone) they have built an entire system on their own and explain key concepts, there is no dearth of jobs for them
This feels like a truism that's easier said than done. In fact, I know someone in that position. They've built things from scratch, they understand things at a deep conceptual level... Oh and they're a math prodigy. How do I refer them to you?
Nope, they won't. Recruiters look for keywords and companies on your resume. If someone has built something as a personal project that doesn't count for squat.
AI development should be harnessed in such a way that AI augments humans without replacing them. Tools that replace human intelligence altogether are not true progress for humanity.
This ship kinda sailed when OpenAI came out of the barn by claiming it could replace people. The narrative of the AI bubble has always been this cynical management driven replace your human capital/labor with stupid bots.
Trying to actually get the framing to be more reasonable is just hard because so many people have oversold it and large swaths of the public are sick of hearing about it.
Or the broader reproducibility problem that’s been silently plaguing most of academia for decades with little to no mention. Many, many, many papers and theses and assumptions we build on may be bunk.
> Without junior engineers how will there be senior software engineers in the future?
My take is: the bar to what counts to HR as "senior" will go down as businesses everywhere try to adapt and hire more seniors - "senior" now just a name, as it becomes the new "junior". Then everyone will pat each other on the back till it all goes down in the flames of bankruptcy.
You see in this thread. Even seniors are shipping slop because at the end of the day its the companies shitheap of a codebase, not theirs, they will ship with slop code all the same.
In other words, they are increasingly devauing their own senior position and discarding their hard earned skills that make them seniors in the first place.
There will be no more seniors. Tech companies will hire junior llm agent wranglers who took a class in undergrad doing this. That is probably the nearterm.
It would be exceptionally fascinating, if AI, due to the limitations of how it models information, and the way that it warped incentives, if AI ended up being a net inhibitor of progress than accelerator.
Going fast, and sustained speed, are very different things. I've often felt, in many different areas of life, that a shortcut will pay off in the short term, but if you take nothing but shortcuts then you will do terribly long term.
You have to do the hard thing eventually, or you never get anywhere.
"Without junior engineers how will there be senior software engineers in the future?" If I were an AI fan, my answer would be this: By that time, AI will have improved enough that it can replace senior software engineers as well.
Disclaimer: I am not a fan of AI, and I am currently writing software without any help from AI, as I prefer.
Right, that's a possibility. When that happens we won't need senior software engineers. We won't need a "thriving mathematical community" either.
Would we need doctors, accountants or analysts? Probably not. At some point farming will be fully automated too, and so will grocery distribution and food preparation. At that point we will have arrived in the post-scarcity world. This is the promise of AI.
The problem is that the post-scarcity world will arrive gradually, not suddenly. Some jobs will be automated sooner than others. The ones that are not yet automated will expect payment for services. People who just lost jobs to automation won't have income to pay for those not-yet-automated services. But that's only until all jobs are automated.
There will be tremendous social upheaval and unrest during the transition to post-scarcity world.
My company hired a junior dev that was helping a senior one, then after layoffs and financial issues senior was fired, and junior left to pick mission critical code with a stick and codex.
Yet to see, as a few big sweeps he did (with various problems), are still sitting unmerged after 2-3 months, with a dev from another project reviewing them and a hardware lead reviewing the idea.
AI progress is so massively out pacing any rate of loss of senior developers though.
Just for a thought experiment lets say junior hiring actually goes to 0% starting today and there is no other route into software dev for example maybe it is illegal for anyone under 22 today going forward to work in dev. Maybe something like ~2-2.5% of the workforce retires each year? And lets just define senior as 10+ YOE so 75% of the current batch of ~40 year working timeline. For simplicity lets just say the other 25% don't ever become senior devs and in 10 years the total number of senior devs has reduced 33% due to retirements. ChatGPT public launch was less then 4 years ago! Look at the ludicrous progress in the timespan. Even if progress suddenly massively slows or hits a wall it is currently hard to fathom it not improving at a rate of 3% a year.
More realistically I think we just have no ability to predict wtf things will look like 10+ years out at this point which is the point in this artificially constrained timeline where a reduction of senior devs just due to time would even start to be noticeable I think.
OpenAI: "Here are the answers to every math problem. Now mathematicians are obsolete. Just send the prize money and prestige to Sam Altman. BTW gonna need some mathematicians to check these answers."
The fact that humans are needed to correct mistakes is only an ephemeral status quo that is being eroded away as we speak. We all can see it happening in front of our very eyes. AI is getting better.
It is pointless to call out the little wins humans still have because again, those wins are temporary.
We need real concerted effort into asking: what is the point? For me the only answer I came up with is: fun.
592 comments
If so, why did they mix proofs that were verified with Lean, and proofs in natural language?
I was wondering that while reading Aaronson's blog:
https://scottaaronson.blog/?p=10169
Or at least, we’re pretty sure that it’s a proof! There’s a Lean certificate, as there are for some of the other 372 breakthrough results (not all of them). But it also appears that no human has understood just about any of these proofs yet
It seems that the obvious thing to do would be to release in TWO parts: the ones that are verified, and the ones that might have some good ideas but also might have some mistakes. Presumably the latter would be much more epxensive for humans to verify.
Can you explain this? How would having a lean proof of the program make it more likely the proof is weak?
And people laughed at Doug Lenat and Cyc for wanting to encode all knowledge as a set of rules.
Sure, even a Lean proof can be wrong. But you made it sound like that because there's a Lean proof, the claims are more likely to be wrong:
>>> Given the constraint (3.5 hours of model effort) having a Lean proof is actually a sign that some of the results are likely weak
That is very useful context, thank you!
Filling these gaps would be a great use of llm tokens!
A bit like submitting an llm written PR to an open source project without reading and understanding it.
Have your LLM generate 372 mathematical "breakthroughs" and then have 2 thousands mathematicians spend two weeks trying to understand each to tell you maybe one or two are viable...
https://lawrencecpaulson.github.io/2026/07/30/Collatz.html
I'm unaware of any serious proofs that have been shown to have a kernel exploit in them.
I agree with Jtarii that it's very unlikely a Lean bug is critical to most of these proofs. But we're in strange times, so I agree wtih the sentiment that we should wait for further analysis before declaring complete confidence in the proofs.
2. Why shouldn’t math progress happen in the open, commit by commit? Why is it so horrible if a proof is 95% of the way there but we later find that it needs to be refined? Mathematics previously was optimizing for an antiquated publishing and distribution scheme. There is no need for the first print to be correct. We have the internet now. We can and should publish incomplete results and correct things on the fly. Maybe mathematicians would have solved some of these problems years ago if they didn’t hide incomplete almost solutions in their filing cabinet because it wasn’t yet ready to be published.
You don’t hate the pageantry of mathematics and academics enough.
I bet you enjoy when a peer asks you to find the issues in a fully AI generated PR that’s 95% of the way there.
There's a lot to hate about the academic world, but the solution isn't spewing out terabytes of crappy half-baked results.
Also “real mathematicians” aren’t the people who “math belongs to”, you’re a mathematician if you do math, that’s it.
1. In OpenAI's case, they dumped 1.8 GiB of Lean proofs on the world. I don't think they've done anything ethically wrong by doing that, but it's the exact opposite of "commit by commit". In fact, I'd say human mathematics has been much closer to "commit by commit", usually using smaller results as stepping stones.
2. You can have "commit by commit" without formal provers like Lean. Just keep your text in a Git repo.
But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs.
but the proof is so fk'ing large that, the "tiny fraction" is still quite large.
and it is not that clean cut, sometimes you need to read the proof to understand the context. You need the context to know if the assumption is true.
[1] - https://arxiv.org/abs/2610.08144
https://arxiv.org/html/2610.08144v1#S2
For complex / tedious proofs I can easily see how small details like this can lead to a valid lean proof (or valid "code"), but missing the important details that got lost.
Take the Rieman hypothesis. All one would have to do to prove or disprove it would be to encode the statement of the hypothesis in Lean, press enter, and we're off to the races.
That's not how it works. Essentially you have to encode all the intermediary steps of the proof in Lean too, and then Lean can check their correctness for you and check that they lead to each other. But it won't just generate a whole proof from nothing. That is the whole point of the Gen AI math claims.
>> All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
As far as I understand the comment "the statement of the theorem" is the declaration of the theorem to be proved, not its proof. That it "usually covers a very small surface of the Lean code" also implies that the OP was only referring to the theorem, the thing to be proved, and not the proof that can run into many thousands of lines.
If I misunderstood then I don't think that's a problem? I don't believe my comment above comes across as rude or an attack on the OP? I think it's normal for this site for users to correct one another without it being a cause for bad feelings.
I hope there's no hard feelings, by the way -- I wasn't meaning to be nasty to you in that comment. I guess I thought your reading was a bit uncharitable, but I understand that misunderstandings happen (very much including on my end) and I didn't mean to make a big thing of it, so I'm sorry if I came across rudely.
The proof explicitly hand-waves some complexity by assuming lookup tables to avoid some calculations which isn’t actually possible since it’s dealing with such large numbers and it only works on incredibly large numbers.
The complexity being so close to nlogn and the handwaving by assuming lookup tables in parts should be a really really obvious smell. At the very least worthy of holding back from the broader announcement.
It us proven in lean as-is with these assumptions and it’s not one of the ones retracted but those assumptions are doing some heavy lifting. I think it’s worth adding back in those ‘by using a lookup tables for x’ complexities and seeing if we really are below nlogn on that one.
This is just a Rice Theorem problem, right?
I'm probably wrong, but what's the point of throwing away all skepticism?
The should be on AI labs to definitively prove their extraordinary claims, and they should be paying mathematicians to do so given that the results from these machines are so opaque and often nonsensical.
Nothing wrong with being skeptical, but I see no reason to be skeptical as of yet.
"Chain of soundness" i think.
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
There's also a fairly well known incident where the Lean formalization of the Riemann Hypothesis in Mathlib was incorrect.
Edited.Added. To compute the posterior one needs to know the probability of detecting such error in a proposed proof.
If it doesn't have a Lean proof, why would we bother with it? And they really shouldn't publish it! We don't need math slop too.
I'm curious to know if the withdrawal was due to an actual mathematician looking at the papers and noticing the errors, or they ran a model on these to proofread, which would not be the first time, presumably, since they would have surely done that before publishing. Both options have interesting implications.
From the "Introduction" section of that paper: "The constants and thresholds in the construction are extremely large".
(And verifying if the algorithm multiplies correctly or not is the less-interesting part of this, anyway. Gets you no closer to verifying the complexity result).
repo - https://github.com/swapnil-jain/integer-mult-kappa
Of course, that's not to say the research is necessarily useless. It's still theoretically interesting to find "better" algorithms if only to shed some light on lower bounds, and so on. And who knows, maybe the line of research could lead to more practical algorithms later on.
https://eprint.iacr.org/2022/439
this doesn't use the literal n \log n algorithm, which may be galactic. but it uses fundamentally similar techniques.
Regarding elegance, take a look at Graham's number. It was not some meaningful constant - it's just a big-ass number which could be used in existence proof. Human mathematicians have been using this approach for quite some time, it's not really AI doing things odd
The lean proof uses these assume ‘a lookup table’ assumptions. The paper smells with the nlogn^0.99999999 (many more nines actually) and unbelievably close to nlogn statement and then the literal talk of lookup tables pushes it over the edge clearly for me.
Maths can generate weird numbers out of nowhere but it really really looks like an nlogn result with some tricks to get past leen to me
The proof can be entirely valid even if it's not actually reasonable to implement and requires an enormous size lookup table - but it still is a meaningful mathematical result and makes progress.
I'm sure there are plenty of times where originally something was proven and thought to be completely impractical but then later had niche use cases or was the bedrock for solving other cases. And the opposite is true: there remain plenty of proofs of things that are mathematically certain but will in all practicality never be useful.
With 40% formalized they probably have a good idea of how many were found to have fatal issues in the formalization attempt, and they hired some mathematicians to verify some of them, especially the big headline ones.
Are they all too busy having brilliant ideas? Doubt.
OpenAI math paper dump should be considered like a hint from 200 IQ eccentric genius - unreliable but perhaps insightful. If it was not "ugh AI" people would be happy about it.
It would be ridiculous for anyone to say "hey man you really shouldn't even have posted these unless you have an ironclad proof".
The latest model even finds mistakes in previously published math papers!!!*
* so far, only OpenAI's math papers were faulty and needed retraction.
It'll be a good test to separate those earnestly trying to advance human knowledge, from those wasting my tax dollars. The later group ought to be publicly shamed and ridiculed without mercy. We need a more invective word than 'pseudo-intellectual.'
Here's one: 'AI-Bro'
IMO If you take out all the stupid human aspects mostly related to fear, egos, etc, we should brace the imperfect and helpful tools, whatever they are, improve them so they are as easy as possible to review, and keep that core scientific discovery loop going
Exactly, and leave the only veneberable human aspect which is allowing the rotten rich bloat further without dissent!
In this case we are talking about using AI to accelerate human progress in mathematics and scientific discovery, and rather than stay on topic, a human comes in with a wealth inequality complaint.
The distributions of the gains of AI advancement is a separate issue, we definitely shouldn't hold up progress on the frontier of human knowledge because of wealth inequality. Its an important issue that needs to be solved, but pausing or slowing progress at the edge of human discovery because of wealth inequality concerns is utterly insane.
It kind of reminds me of when tech giants open source a project as a means of putting a positive spin on abandonware. “Here’s the source! Any problems are yours to fix now. You’re welcome”
I also fail to see the issue you have with releasing abandoned source. In what world is that bad? That obviously is a gift and should be encouraged. e.g. id software's history of doing that has meant their work stays alive forever.
That's right, and the difference is that this one is parasitic.
Shouldn't we pay for the best tools if it helps researchers to be more effective?
If reading each others work is symbiotic it makes sense OpenAI is parasitic: whose papers are they reading in return? No-one’s.
The problem people are having is they clearly are interested. They think the ideas are good. In fact, too good. If they thought otherwise, they would just say it's all slop, no one cares, business as usual. And you can tell that there's this phase change in their behavior because previously you could ask chatgpt about math and it would just give you word salad and everyone knew that. Now we can all see that it's not just word salad and people are scrambling to figure out what to make of that. Obviously an accurate answer oracle is still strictly useful even if it makes no attempt to tell you why (you can even use it only to help prove your boring technical lemmas when you have ideas!), so obviously this is an emotional reaction, not a rational one.
We need the companies to humanly review their papers. in the same way as at other companies we use humans to review the papers.
(If you're going to object that it's difficult to validate the statement of the problem, please first state your level of experience doing so. It's getting tiring seeing people raise this objection and claim that a statement is just as hard as a proof over and over who don't seem to actually know any math and have never tried to write anything in Lean)
Someone still has to read the formalization.
Ironically though, what I imagine will happen, is that the researchers will pay OAI to use chatGPT to help themselves eval the proofs.
You have the frontier labs who are marketing that it’s over and they’re building intelligent machines and you’re saying the mathematicians should ignore it? Ok
Mathematicians, as autonomous entities with no formal connection to any AI lab, have zero obligation to do any work for those labs. OAI can't do anything if all the mathematicians band together and say "Sorry, we're not interested".
If they do chose to engage, they are doing so entirely voluntarily, and it would strongly indicate, if they are voluntarily doing it for free, that there is value (i.e. compensation, payment, barter, worthwhile, whatever) to be had by digging in.
This _might_ have been true somewhat in the past (although it wasn't), but it's completely false today. Anyone with access to a sufficiently advanced model has the capabilities of analyzing these papers/proofs. It's no different than reading a codebase you might not be fully familiar with, and checking it for correctness (give an engineering analogy).
This hardcore gatekeeping of math (and by extension STEM) fields MUST stop.
Like I was reading some about adele rings last night, which is already going to be quite a concept for a layman to be able to even slightly describe. Then you can layer on that apparently they're locally compact, so we can talk about harmonic analysis on the additive group. Like, come on now, 99.99% of people have no hope of ever following along, and this is stuff from 75 years ago.
But they don’t. What they have is the ability to ask something else to do the analysis. It’s an important distinction. If the asker has the skills to evaluate the results, that’s one thing, but too many don’t and act as if whatever they got is unambiguous truth.
> This hardcore gatekeeping of math (and by extension STEM) fields MUST stop.
What must stop is the overuse of the word “gatekeeping”. Anyone is free to study these fields and work on problems. What people rightfully object to is uninformed research flooding everything with hard to verify junk.
Mathematicians do have some vested interest in keeping the profession from collapsing into an intellectual oligopoly, where one or two commercial players with early access to their own internal models continuously scoops everyone else and pollutes the field with externalities, and the profession itself collapses, only leaving AIs and hobbyists able to stand. At that point it'll be the AI firms who become rent-seekers. That's not really "gatekeeping" in any conventional sense of the term, it's protecting a healthy economy of ideas and the long-term development of mathematics.
Is someone stopping you from studying maths?
Also - this is no different to open source and code contributions now right
Withdrawal is akin to submitting a paper to peer review and then when you’ve noticed mistakes, you decide to take the paper back and correct it.
Reject is when someone else notices the mistakes and tells you to take it back and correct it.
Withdrawal and reject happen all the time in a scientist’s career. They don’t necessarily mean the scientist is doing bad research, just the research was not ready. Retract usually means something more.
By dumping the papers, OpenAI skipped the typical peer review process, so peer review should be understood as what’s going on now as mathematicians look over the papers and find flaws.
This concerns the Hodge conjecture (millennium prize related) paper. Seems to me like PhD nerds weren't confident bosses pushed ahead anyway.
This is... logically equivalent to the claim it is offered to contradict.
Because this is what they say all the time. It's like a badge they have to wear and tell everyone they are wearing, even though we see it.
You can see the same thing with ANT. Had they looked at Mythos output, they would have realized there were only 76 items, not 79 like the bot claimed. Or the ones that were just a "it crashed" and nothing else (not a cve imo).
https://www.youtube.com/watch?v=NnV_cWeoo5Q (Linux Kernel team sharing their side of the Mythos "hacking" story)
Presumably the tip would be from someone who’s familiar with the area but doesn’t want attention. Which is unlikely to be someone in OAI.
Perhaps with AI.
A manual human check of each one would take a few month at least. In peer review, there are horror stories in math about more than 1 year before the journal accept the paper. So 3 reviewers x 700 pdf = 2000 mathematicians, that is 10%-20% of the community according to an unreliable count printed by Gemini after scrapping r/math.
Also, in most cases the only people that can understand the proof in a so short time (let's say a few months!) is the small group of people working in similar problems, i.e. the same group of 20-100 guys/gals that you meet in every conference.
Scientific progress used to be people debating and correcting other people. Now it's going to be people with AI assistance debating and correcting other people with AI assistance.
but do these 'people' need to belong to a thriving community or not to be able to do those things?
1. This is expected if you only use a single model family like Claude, eg. we use a different model family for code review than authoring, OAI could have done this too for their math dump
2. Ai needs a good human driver beyond the trivial or mundane, they are expert enhancing machines, not expert creating machines. This is where the community comes in. Reading Tao's ChatGPT session reveals this: https://news.ycombinator.com/item?id=49010345
3. OAI is not trying to be a member of the/any community, this is not the first story to shows this, nor do I expect it to be the last. Perhaps this is them being effective altruists today? /s
I agree LLM review is also fallible (as is human review) but the interesting part to me is that finding this sign error before publication should have been table stakes for OpenAI, it’s their own model that found the sign error.
I’m curious what was in the original prompt and what was in the prompt that led to finding the sign error, I think it matters a lot for understanding the dynamics here
As much as anything can be infallible.
If they can be automated, they are not necessary. If they are necessary, they won't be fully automated. It's a pretty simple experiment to run, the math "community" should bear with us. Darwin would be proud.
It's great that we're starting to see the light at the end of the tunnel, and will some day achieve a perfect market without humans. If you think about it, all the market really needs is a people to own everything, everything else can be automated, and all those annoying human workers can be eliminated.
To witness an arson and rejoice reveals an ugly kind of sadism.
I see why you might call it sisyphean, but I don't see what's ironic about it.
Even if your stated assumption was baked into the original comment, which is doubtful: the historical record shows that we will keep relearning The Bitter Lesson and each community will pretend what they do for a living is exceptional and immune because of xyz. The screams will get louder when the "greedy" and "dumb" automation comes knocking and it turns out nothing was truly immune or "nuanced ".
Getting some new hobbies may be in order, it's a Brave New World.
Bringing it back to math explicitly: you are essentially betting that the singularity is here, today, and that there are absolutely no downsides to breaking the pipeline which trains mathematicians (meaning that in 5-10 years at most there will be zero humans capable of assessing AI math output or independently advancing the state of the art).
The CS101 lesson in the first paragraph is appreciated, you should do it more often for us simpletons.
An absolutely ridiculous statement. There is a vast amount of mathematical knowledge that hasn’t even been written down, much less formalized.
https://en.wikipedia.org/wiki/Tacit_knowledge#Definition
"If those grapes exist they are probably sour."
The same happens all the time in mathematics.
At the minimum you ought recognize that world class experts would disagree with your dismissiveness. Trying to explain the differing positions should not earn such immediate dismissal.
You're also failing to comprehend my passing comment about professors as a minimum criterion for the diversity of what reasonable opinions on the issue ought to like. I said it order to increase an open minded discussion, whereas you then used your familiarity with academics to validate your specific views. There's a world of difference there already, and metacognitively yours is the problematic one.
You’re distinguishing “knowledge” from “idea” in a particular way that doesn’t correspond to common usage (see my counter examples). Without you being explicit about your definitions, I can’t tell whether what you’re saying is meaningful. It feels tautological.
Given that an executive assistant has unwritten knowledge that is necessary to do their job, where your evidence that no mathematician has analogous knowledge (using the word in the common way, not whatever way you mean it)?
It’s possible, but it’s not as obvious as you seem to think.
We can dig into the philosophy of these definitions, but I think the far more interesting point is that even if we grant the existence of this kind of knowledge in the minds of human mathematicians, we have passed the threshold where that "knowledge" can keep up with systems that do not have access to it. Moreover, to claim humans have a "vast amount of mathematical knowledge" that is apparently valuable and that AI systems don't have, you'd have to prove that this "knowledge" is not implied or cannot be reverse engineered from the entire corpus of mathematical writing on which AI systems are trained. You'd also have to demonstrate that this "knowledge" leads to actual results that AI systems cannot generate without it. Given the results AI systems are producing, which are far beyond human ability at this point, it is more likely that AI systems have already internalized the entirety of this so-called "tacit knowledge" and then went much further, much faster, without humans in the loop at all.
On the question of a single word out of my entire position, that is a reasonably fair statement for mathematics (which is the topic under discussion). The fact that you think it's tautological supports both that you agree with its correctness and that this is a mostly irrelevant side conversation. And whatever you think the answer should be is not somehow not subject to the constraints of logic.
Not your contention that LLMs likely have something analogous to what you call “ideas” (you’re almost certainly right).
Mostly irrelevant? Dunno, maybe according to your rigid ontology ;-p
Cheers!
And that's a bad thing. If the math community didn't exist or was weak, OpenAI would still benefit from the prestige of these results they were forced to withdraw. Withdrawing these papers has harmed OpenAI's investors, and that's totally unacceptable.
> With automated math that community as tao pointed out is at risk.
Good to hear. The problem they represent needs to be eliminated.
What about software developer community? AI has eliminated the need for junior software engineers. Almost no one is hiring junior software engineers. But companies still need senior software engineers. Without junior engineers how will there be senior software engineers in the future?
What is the solution? I don't think the solution is to say AI progress in software, mathematics etc. should be halted.
https://warhammer40k.fandom.com/wiki/Tech-Priest
I have a data pipeline with 6 steps, A -> B -> C -> D -> E -> F. I asked Codex to make some specific optimizations to step B and benchmark them. It did what I asked. Then it decided to also benchmark the entire pipeline, and after noticing that step E was slow it decided to make some optimizations that I had not asked for on step E. It was at this point that I wondered why it was taking so long, saw what it was doing, and stopped it.
This is GPT-6.1 Sol High.
Right, companies won't need software engineers. They'll just need someone who can use tools to produce source code and maintain the generated artifacts, plus make domain-specific technical decisions like "what should the system do when two users update the same record as the same time" or "how should the system behave when a message in the queue cannot be processed".
We really oughta come up with a job title for these people.
Who do you think the will be choosing whether the database uses a pessimistic or optimistic concurrency strategy? The CEO?
“ Claude! what should the system do when two users update the same record as the same time, explain to me with full clarity”
or "Claude! how should the system behave when a message in the queue cannot be processed? Give me all the possible ways ranked from best to worst, also explain to me all these concepts so I can understand as I don’t have a cs degree".
If you think that there is no future where software engineers don’t matter then you are delusional. While the future is not set in stone the pace and trendline of AI point to this future as a MORE realistic future then the alternative.
Your example btw is ALREADY a solved problem. AI can answer it and design around it. Agents at my company already handle our infra.
This isn't even the right question to ask, I think you've basically proved my point. You are in charge of deciding what the system should do when two users update a record at the same time. It's extremely dependent on what you're trying to do.
> Your example btw is ALREADY a solved problem. AI can answer it and design around it.
What's the one-size-fit-all solution for concurrency management that works for every single domain and application? I'm curious.
> Claude! how should the system behave when a message in the queue cannot be processed? Give me all the possible ways ranked from best to worst, also explain to me all these concepts so I can understand as I don’t have a cs degree".
Who's going to make this decision? The CEO?
It’s your example. I simply took your example and asked Claude. If it’s not the right question then don’t give it out as an example.
> What's the one-size-fit-all solution for concurrency management that works for every single domain and application? I'm curious.
I’m curious how your brain concocted I said that. Examine the context of our conversation. What I mean there is that AI can solve those questions for every possible domain application.
> Who's going to make this decision? The CEO?
Armed with Claude any non technical person can make this decision.
Knowing the right question to ask is what makes a person an engineer.
> What I mean there is that AI can solve those questions for every possible domain application.
Yes, if you know what to ask. You're doing an excellent job of demonstrating my point!
> Armed with Claude any non technical person can make this decision.
You just disproved that by asking the wrong question. Much like you, the CEO won't even know what to ask an AI.
Yes, but this is orthogonal to the point and that is: AI can do it too.
>Yes, if you know what to ask. You're doing an excellent job of demonstrating my point!
No it's your comprehension that needs work. You are missing MY point while being repeatedly getting enamored with your own point. My point is that AI KNOWS the questions.
>You just disproved that by asking the wrong question. Much like you, the CEO won't even know what to ask an AI.
I didn't ask a single question bro. I only regurgitated your examples. Much like AI, half your statements are based off of hallucinations.
I do not know or care what my if statement turned into in x86 assembly unless it becomes a performance problem and even then, I'm not profiling or debugging in machine language. Neither do most developers these days. A message in a queue becomes something akin to that in this era.
I see that I got downvoted there. This is not something I advocate or look forward to but I feel this is where it is going.
Likewise, you don't care exactly how an if statement gets converted into machine code, but you do know precisely what an if statement is and how it should behave, and could identify if it was buggy, and that that part of the codebase contains a bug. If you can't do that, then there is an impossible-to-estimate probability that at some point you get stuck and no progress will ever be possible. I don't see that as a winning strategy, in the long run (but it may work very well in the short term).
No it isn't lol. Have you worked on any real systems with customers? Good luck telling your boss at AWS that a poison pill message stopped the payment queue from processing so they lost $100 million in sales but hey, it's an implementation detail, no big deal.
I have. Those systems already fail in spectacular ways and people tell their bosses that some worker process stopped working because its transaction IDs overflowed.
I bet that sounds like `the flux capacitor stopped reticulating splines` which is already an implementation detail for the boss anyway. Nothing changes.
Or maaaaaybe.... an engineer?
agent herder!
If that comes to pass, I will have to re-evaluate my career options
I think that person does not need to know about locks anymore.
Some people hope AI will get good enough in a few years that it can innovate without human experts. Maybe? But that remains to be seen.
By the progress of AI from ChatGPT to now is horrifyingly fast.
Trendlines and basic reasoning point to a most probable future where the AI is superior. We can’t just say “that remains to be seen” because the alternative is the least probable future.
Anticipate the change and act prior.
In the age of extraction capitalism where building sustainable, profitable companies is not the goal, no one will care.
Human language is famously terrible at being unambiguous.
But that's the thing, you and the AI might be "on the same page" for one prompt, and then you aren't for the next.
> and yet judges and lawyers agree on how to interpret most of them
Um, no? Lawyers and judges frequently disagree on how laws should be interpreted. And it is often not written in a way that a layperson can easily understand.
> defined arbitration process to resolve any new ambiguities.
That is famously slow and expensive, and can resul in something very different from what the lawmakers originally intended.
LLMs eat away at all of these requirements.
The developers who knew how to write efficient low-level code found that there were no jobs for that anynmore, so today the developers who can work at that level are very few.
The same will happen with AI being the new abstraction. In another decade or two, very few people will be able to write code by hand. We'll need a rack of compute in a data center and multiple KW of power to do what we used to do on a desktop PC drawing a couple of hundred Watts.
Your code used to be a masterpiece, so well crafted it's easy for AI to tweak and modify because you've got everything so logically organised and scoped... and now this is what you're producing? Hard to debug monstrosities that only an LLM can realistically bolt new features or tweaks onto, because it can do the kinds of refactoring necessary each time.
We use to talk about the fact that code should be readable because you spend more time reading it than writing it, but I think that misses the key part that readable code is also typically easier to debug. If you can read and understand the code, you can follow the logic when things are wrong in production, and you can more easily reason about the emergent properties of interactions between the complex systems that are involved.
I jest, while in agreement with this whole comment. We used to care about fostering informed developers and maintaining high standards and good quality software.
I literally compared it to being an expert woodworker. Beautiful ornate decoration. Rich, sturdy mahogany, one of a kind, beveled edges and a fantastic stained hardwood.
Now it’s the 30$ Ikea cardboard stuff.
My biggest question is how many tables does the world need, and how many woodworkers will be required to build + maintain those table factories.
If you buy a house or rent an apartment in most of the US, any furniture will be stripped out, even if the only thing you plan to do with it afterwards is throw it away. Then the new tenant provides their own furniture, which they either moved from elsewhere at great expense or had to purchase on the spot. No part of this makes any sense. We don't strip countertops when selling a house even if they're unfashionable, we don't replace white goods, but somehow it's expected for the furniture.
If you buy a house in Hawaii, it's understood that you're buying the furniture that's already in the house. I assume the reason is that it's more difficult to obtain new furniture in Hawaii.
If you rent an apartment in China, it will come with furniture, because how else are you supposed to live in it? And if you're not happy with the furniture it's shown with, you negotiate with the landlord for the furniture you need.
If Americans sold their furniture when they moved instead of throwing it away, you'd see everyone using much higher-quality furniture. It would have come with their house. And providing it to houses that didn't have it yet would be an investment, just like the countertops.
I think with AI, most people are getting lazy to do it properly.
The other day, I deleted 65K LOC that were dead code or stupid explanations over very obvious code from a vibe coded repository which had 95K LOC (but should have 10k imo)
Do you even see anything underneath that rose tint ?
I've waded through unfamiliar code at 3am trying to figure out just why the hell things broke this time more times than I can care to remember, particularly trying to tease apart the ways that code has organically grown compared to the original intent. If I'm subjected to one more piece of "spooky at a distance" injected behaviour code I'll probably scream loud enough to be heard half way across the country.
It's still just leaps and bounds more readable than what people are slopping together (I do have some co-workers that have been extremely tightly focused on avoiding "slop" with their AI and doing a lot of tuning, and it's certainly preferable to the ones that haven't)
And this is the pattern I've seen on most (semi)successful projects I've worked on in the past - I'd say correlation between financial success and code quality is 0 (up to a point where the whole thing doesn't fall apart). Once scale (both in load and in code size/features) starts mattering you're stuck building on a foundation of shit. LLMs are very good at identifying and cleaning up said shit layers, as long as you're steering them towards a desireable outcome.
Not saying it doesn’t exist, just saying this sounds dangerously close to a boomer talking about the 1950s
Luckier than me. I've worked at a few places where the code was simultaneously brilliantly written[0] and also unmaintainable nonsense that caused endless problems. One place had its own object model and ORM that absolutely no-one currently at the place understood and literally every bug filed (whilst I was there) could be traced back to that code.
(Probably just a coincidence that most of those places where Perl shops but I've seen it with Go too...)
[0] In terms of "cleverness", not in terms of "maintainability" or "readability".
Only once?
Oh god, we're gonna do the four Yorkshiremen, aren't we?
there are several features over the last few months that were obviously made and deployed and no one even launched the dev server and tried a single thing to verify if it was right. just "pull my ticket, do my ticket, push my ticket. i am a developer."
I’ve seen monthly and quarterly executing results AI generated with plainly wrong factual information.
Time unfortunately that you are simply not given because the whole point is to work faster so expectations of velocity have of course increased.
So you end up having to get a fuzzy idea of a given changeset, look at it a bit and evaluate quickly if it's a good change or a bad one and click it through, and on to the next thing.
At the size of PRs being whole features and doing this 5x faster than before, all you've got left as a senior is your Spidey sense. As a junior.. no idea how they cope.
We'd all love to still spend that 90% thinking time, but it used to be justified by necessity of getting the job done. Now, it's just not a luxury that is afforded.
What can ya do.. I'm slowly learning to be the best bot herder I can be, but it certainly feels like a change in skillsets. I definitely only feel like I'm able to do a good job due to enough experience and building and growing software projects over time to have an idea of what kind of decisions might bite us down the road, as well as to know what maybe can't be known but is just worth a risk. Without that kind of intuition I think I'd feel like I was really shooting blind.
IME a lot of people are now subject to output-rate expectations that preclude doing much else, honestly.
Some jobs will stick around in vastly diminished numbers with tasks that are completely different than what they used to be to produce the same output (e.g. farmer). Other jobs will be eliminated entirely (e.g. switchboard operator). I'm guessing things like software engineering will go the way of the farmer, with the main unknown being just how much demand for software there is.
In this case with AI that power will shift to the companies that run the AIs
The entire valuation of the AI industry is predicated on people not just losing individual jobs, but being taken out of the workforce entirely on an economic level.
They are talking about the workforce of the entire economy shrinking. People will lose their livelihoods for good.
This has the potential to be even worse than the second agricultural revolution to industrial revolution phase, which made ordinary workers lives absolutely miserable for maybe a hundred and fifty years.
This time, there will be no jobs. If you are displaced from one industry by AI, you will end up in another industry also being decimated by AI; if you get a job at all, you will do so by working lower pay than other workers, who will in turn be pushed down the ladder.
And that is if you are lucky: if you have only IT skills, why should you be the first to get a fruit picking or plumbing job?
Easy. Because you have the skills to increase productivity by automating it. Oh wait...
Ahh that's OK then. Everyone's in this same boat simultaneously in multiple industries! Cool!
> What is the solution? I don't think the solution is to say AI progress in software, mathematics etc. should be halted.
I think the solution from the maths world is to not grant these AI papers (or their human sponsors) the normal courtesies of "regular order", just as you would not with an AI lawyer or someone who was just pressing enter at a law firm.
But in the software world, nobody gives a shit, apparently. We are collectively morally bankrupt and should not be granted the regular order to help other people to decide what to do with us.
In fact, the world is always filled with curious people who like to go one level below.
This hysteria about losing "Junior Software Engineers" -- most of them in it for money, promotion rather than craftmanship, is over-rated.
People who love solving puzzles will always find ways to sharpen their mind.
People who love understanding things, will always find ways (AI will help them tremendously).
People who love taking shortcuts will always find ways for it (AI or not)
Eh? Apart from it not being what they are paid to do on their 9/9/6 jobs, when will they have the time to make it happen?
What is going to happen is that the remnants of the open source community will do the job of educating juniors for free, when the university degree system collapses. Just like it currently keeps a bunch of systems going with inadequate compensation.
The corporate world gets the problem off its balance sheet. Again.
The actual argument is "there will be no jobs for Junior Engineers, so there will be far fewer, and as a result there will be a huge shortage of Senior Software Engineers".
You are responding to the problem as if it some kind of extinction event, like a rare bird, where if we can find a breeding population we save the day. A few curious people, self training for the love of the game, and as a result we still have a few Software Engineers so everything is fine. It is not like that, and I haven't heard anyone suggest that is the issue. The potential problem is a massive shortage of workers with skills that are currently essential to the functioning of a large fraction of the economy, whom we might still need in the future.
The continued existence of talented enthusiasts does not establish an adequate workforce pipeline. If paid entry level experience contracts, what replaces it, and why should we expect that replacement to operate at sufficient scale?
If you have made it to the point of being a Junior Developer, I can assure you food and shelter is not a problem for them. You just have to adjust to a standard of living like the other 7 Billion people on this world.
Also, if a Junior Developer can show me(or anyone) they have built an entire system on their own and explain key concepts, there is no dearth of jobs for them
It's just a search problem now.
Trying to actually get the framing to be more reasonable is just hard because so many people have oversold it and large swaths of the public are sick of hearing about it.
My take is: the bar to what counts to HR as "senior" will go down as businesses everywhere try to adapt and hire more seniors - "senior" now just a name, as it becomes the new "junior". Then everyone will pat each other on the back till it all goes down in the flames of bankruptcy.
In other words, they are increasingly devauing their own senior position and discarding their hard earned skills that make them seniors in the first place.
There will be no more seniors. Tech companies will hire junior llm agent wranglers who took a class in undergrad doing this. That is probably the nearterm.
You have to do the hard thing eventually, or you never get anywhere.
Disclaimer: I am not a fan of AI, and I am currently writing software without any help from AI, as I prefer.
Would we need doctors, accountants or analysts? Probably not. At some point farming will be fully automated too, and so will grocery distribution and food preparation. At that point we will have arrived in the post-scarcity world. This is the promise of AI.
The problem is that the post-scarcity world will arrive gradually, not suddenly. Some jobs will be automated sooner than others. The ones that are not yet automated will expect payment for services. People who just lost jobs to automation won't have income to pay for those not-yet-automated services. But that's only until all jobs are automated.
There will be tremendous social upheaval and unrest during the transition to post-scarcity world.
Just for a thought experiment lets say junior hiring actually goes to 0% starting today and there is no other route into software dev for example maybe it is illegal for anyone under 22 today going forward to work in dev. Maybe something like ~2-2.5% of the workforce retires each year? And lets just define senior as 10+ YOE so 75% of the current batch of ~40 year working timeline. For simplicity lets just say the other 25% don't ever become senior devs and in 10 years the total number of senior devs has reduced 33% due to retirements. ChatGPT public launch was less then 4 years ago! Look at the ludicrous progress in the timespan. Even if progress suddenly massively slows or hits a wall it is currently hard to fathom it not improving at a rate of 3% a year.
More realistically I think we just have no ability to predict wtf things will look like 10+ years out at this point which is the point in this artificially constrained timeline where a reduction of senior devs just due to time would even start to be noticeable I think.
It is pointless to call out the little wins humans still have because again, those wins are temporary.
We need real concerted effort into asking: what is the point? For me the only answer I came up with is: fun.