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

> the mathlib has many gaps and lacks many basic theories. So many problems can not even be stated yet not to mention proved.

That is very useful context, thank you!

> the mathlib has many gaps and lacks many basic theories.

Filling these gaps would be a great use of llm tokens!

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

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.

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.

Link or it didn't happen

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

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

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.

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.

[dead]

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.

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

the autoformalization could be proving a subtly distinct result; if the area is not in mathlib already there's likely not a good reference theorem specification to use for a comparator check. or it could be exploiting kernel bugs. just using a second checker kernel is not enough; there has been an example of a model interpolating bugs across multiple checkers in a single bogus proof.

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.

Why is it all unpaid - shouldn’t some of these have applications of which it would be in companies with paid employees best interest to verify?

Also - this is no different to open source and code contributions now right

We are all reverse centaurs now.

It’s fairly common to have errors in preprints.

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

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?

> IMO If you take out all the stupid human aspects mostly related to fear, egos, etc

Exactly, and leave the only veneberable human aspect which is allowing the rotten rich bloat further without dissent!

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.

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

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

How many mathematicians write 100 papers?

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.

Humans are not being sold as the panacea to all the world problems currently.

> We need a more invective word than 'pseudo-intellectual.'

Here's one: 'AI-Bro'

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

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

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)

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

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?

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.

  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?

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.

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.

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.

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.

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.

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

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.

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.

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

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.

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

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

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.

Darwin, possibly the most misunderstood scientist in history, would not be proud

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.

> automathician

I vote for "automathon"

> I assume progress there is kept under wraps until they can capture the economic benefits. If they can do that, then the insane valuations may actually be valid.

Or progress is not as straight forward in those fields as in math.

*Algebraic geometry

So a fair headline would be "OpenAI tried formalizing more of their proofs, and found 33% of them had a mistake".

But like with all slop, why should I have to spend my time dealing with your worthless slop? If I wanted slop I could just make it myself.

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

Even if that's the case, they aren't even mentioned. I'm guessing Lean failed on the 3 that got withdrawn. And it makes even less sense in that light, because there are 6 verified new things to be explored and built upon, yet the many are putting all that energy into the failures, as if seeking out some hidden truth or something.

Yes, that was my understanding too.

First of all, people retract papers all the time. I can't give you the exact figures, but surely at least half of all academic researchers have retracted a paper at least once in their lives... Second, is it so hard to believe we are going through a complete paradigm shift in academia? People can now produce hundreds of high quality papers in a matter of weeks/days (with enough compute). Even if the error rate goes up (which it likely won't) we're still being exposed to a monstrous amount of novel information.

Even Einstein retracted one of his earlier papers re the cosmological constant... And he is one of the greats. Although not purely math related, it still counts.

It is wild to me how much stock mathematicians put into the social aspects of math. The whole social framework you are describing _did not exist_ for almost the entire history of math. It might very well be seen as a historical anomaly, like renaissance mathematicians challenging each other to solve cubic equations.

Wait, what? Well, yes, you're correct, AND flipping a sign in a draft paper that your buddy catches in a pre-read is SUPER common. People don't do math in a vacuum. Well, many do not. Some do.

Thanks for the question. It's difficult to quantify but it basically comes down to how many obvious errors LLMs produce amortized by the processing time.

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.

Oh, because captcha's are really hard to solve?

Not a great sign when nobody wants to attach their own name to words thrown into the world.

I agree. I don't even think their Navier-Stokes proof is correct & more errors will be found in that one as well.

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.

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

> No it’s not. In fact, much of it is formally verified, which makes it far more reliable than most human-written proofs.

its formal verification on top of formalization by LLM, which could have errors.

I wonder why the heck were they provided / uploaded then. Perhaps just a fast and loose play-out on their part. What I don't understand is how come engineers / scientists working on these are okay with this kind of attitude.

But that's the argument that was used when people here were skeptical about the results.

Irresponsible is an adjective that means lacking a proper sense of responsibility, or acting without thinking about or caring about the potential consequences of one's actions.

They do not care if they waste everyone’s time or flood the common with slop. They did not spend their own time to verify that the Lean proofs correspond to the natural language proofs. They did not even spend their own time to verify that all of these proofs are well written.

They instead are mining the unrenewable resource of open math problems.

However, seeing it another way is easy if you are financially motivated by their upcoming IPO (see how easy it is to invent motivations for comments?).

It is irresponsible when nobody checked it for correctness first. They just copy pasted what the slop machine spit out.

it's like if you vibe coded something and the onus is now on the reviewer and the reviewer tells you your work contains bugs and is messy - that is not acceptable from the reviewers pov - why should the reviewer spend all his human effort, a scarce resource, reviewing your code while you've spent barely a fraction of his effort generating this. OpenAI is a trillion dollar company, surely they can verify stuff before pushing it out? The problem is not that they are solving the problems, they don't care at all about the actual process of doing mathematics. Using compute to mine problems and throwing results in github and letting human reviewers spend effort to correct these is not going to win them any favor. If OpenAI really cared about math, they would have someone on their side who actually understood the results they produced and was able to verify their correctness and educate others.

They only withdrew it after someone pointed out that it was a flawed paper.

In one case by asking Astra to review it.

Not exactly encouraging that they did their homework before publishing results.

Withdrawing it, in itself, might not be, but it kind of skips over the part where they have a paper that warrants it in the first place.

Withdrawing it isn't irresponsible. I don't even think releasing it is, because that is often the best way to find problems with it; expose it to the wider research community. Doing PR victory laps based on unverified, unfinished work, on the other hand, is. It is well known, even scientifically demonstrated, that retractions or refutations get much less attention than the initial exuberant PR announcement. And thus this practice contributes to misinformation.

And just to preempt the kneejerk whataboutism: Yes, all of academia does this to varying extents, and the mainstream media are also complicit. And that is also irresponsible. And no, that is not an excuse for OpenAI. Especially when you consider that OpenAI actively portray themselves as some kind of moral arbiter on AI and "doing good for humanity". They should be held to the extraordinarily high moral standards they purport to hold themselves to.

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.

> It seems to be getting invalidated as people dig through the wall of meaningless text surrounding the actual results.

3 results out of 400 is nothing.

Wrong.