"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.

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...

TECH! PRIESTS!

https://warhammer40k.fandom.com/wiki/Tech-Priest

> 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.

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)

  AI progress in software

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?

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.

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.

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?

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.

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.

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.

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.

I think this will be a self-correcting problem once the damage is done, and the only cure is more cowbell, I mean - TIME.

In the age of extraction capitalism where building sustainable, profitable companies is not the goal, no one will care.

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.

AI slop is basically the grey goo scenario but happening on the level of information and thought.

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.

There's plenty to be concerned about without making up problems like OpenAI claiming any prize money.

How else do you get free world class training data?

Yes: https://x.com/ElliotGlazer/status/2108026240582246600

This statement assumes local maxima don’t exist and greedy short term optimization always leads to long term benefit.

“If they can be automated, they are not necessary.” That’s a pretty interesting take as eventually everything could be automated.

You've abandoned every part of yourself to the siren's song of efficiency and automation, huh?

To witness an arson and rejoice reveals an ugly kind of sadism.

> You just need autonomous verification, which already exists at scale and speed vastly beyond the entire human mathematical establishment.

An absolutely ridiculous statement. There is a vast amount of mathematical knowledge that hasn’t even been written down, much less formalized.

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.

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.

> 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

Can you explain this? How would having a lean proof of the program make it more likely the proof is weak?

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?

Here's a recent example of an AI exploiting a soundness hole in Lean in a paper purporting to have solved the Collatz Conjecture.

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.

(integer multiplication, not matrix multiplication, right?)

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.

  > 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.

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.

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?

[1] - https://arxiv.org/abs/2610.08144

How much lean code do you need to read to check if NAvier-Stokes was correctly formalized?

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.

About your second point.

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.

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.

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.

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).

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).

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".

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.

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.

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.

Right. Imagine if some human mathmetician released what OpenAI did with all the caveats and warnings about possible mistakes.

It would be ridiculous for anyone to say "hey man you really shouldn't even have posted these unless you have an ironclad proof".

Link or it didn't happen

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.

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.

We are all reverse centaurs now.

It’s fairly common to have errors in preprints.

But is it equivalent to withdrawing post-publication or is it more akin to not passing peer review with major revisions requested?

But have you formalized every single one of your results? And if you haven't what odds would you put on one of them not working out, if formalized?

Most mathematicians don't produce 400 papers in a 48 hour window either so I'm not sure comparisons are helpful

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.

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.

The typical human math paper does not have multiple unfixable errors, no.

The onus is on formal verification when it comes to computer generated results. So far only 22% of the papers have it.

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.

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.

I think you are implying that my suggestion is unreasonable and exceeds the standards applied to science produced by "normal" human processes.

In fact we already follow exactly this process for human papers and have done for a very long time. Publications without peer review are treated with great suspicion. This is how we end up with journals of varying levels of prestige and rigour.

The process isn't flawless and there are huge problems with retractions, as well as weird financial incentives and rent extraction but there is definitely an increased level of trust in a paper published in Nature.

Super-intelligence that’s going to end mathematics as we know it surely must be held to a higher standard than puny humans?

More seriously the problem is the complete utter lack of care OpenAI has shown in their desperation to demoralize mathematicians with their new LLM. In their words, it took 3 hours of ChatGPT pro per result, why not spend a hundred hours per result formalizing it, checking if the formalization matches the natural language proof, and whether the argument could be made more simpler and readable. Any human paper has hundreds of hours of work put into it, but OpenAI who is absolutely adamant in demoralizing the mathematical community and demonstrating their superior “intelligence” will only spend 3 hours, write unreadable, inscrutable proofs, not formalize all of them, and then dump it on the mathematical community for some reason.

This is extremely disappointing. It means they are sharing unproven work for PR, forcing the mathematicians community to do the verification job for them, while so-called "accelerationists" surf on the hype and help with the pro-AI propaganda.

If your AI tool can help advance mathematical research, share the tool with mathematicians. Using it like this is irresponsible.

"AI will kill us all": no. Greedy humans will kill us all. With AI.

Generating Lean proof is much harder and time consuming so these errors made were probably discovered during Lean proof stage.

Well, fine - but my understanding is, if a fuzz-generated Lean proof is correct, that’s end of story. It can’t be “incorrect” if it “passes”.

You might think this is not very useful, maybe - but that’s not a reason to retract..?

Well I do assume lab automation in all the hard sciences. Social science already doesn’t reproduce so no difference there.

My intention wasn't to attack academics. I was just trying to point out that being wrong is something that happens all the time, especially when something is in-progress (pre-print). How many papers written by people are withdrawn during peer-review, or while in the preprint state?

If someone had a blog about their research on a math problem, and they figure out one day that what they wrote a week before was wrong (retracting it), would that be a bad thing? I don't think it would be bad, but that's not how academics approach things.

This is almost certainly the case. I very much doubt that anyone there of any importance in the decision-making process around this actually cares about the math, just the headlines they can get from pushing it out.

I am certainly experiencing what seems like some mania or computer addiction from these technologies. I’ve never been able to produce such results as I can today. I lose sleep staying up late working on it (though to be fair this has always been an issue). But the volume of work is so hard to audit. It makes it difficult to make flawless results. That doesn’t excuse the mode of publication. They could have had humility in their announcement. “We are seeing some interesting results and seeking community validation.” Maybe they did, I did not read their full announcement. But that would have been the right move if they can’t verify something fully.

I've tried reading one of these, it was an unreadable mess with some strong smells. It might have something to it, but it'd take a decent amount of labor to validate it, especially with how many references to other papers it had.

Yeah imagine being in a company where everyone is suffering from AI psychosis and fully bought in. They give you unlimited tokens and tell you that you are a genius and can solve anything. You’d publish all sorts of made up slop papers.