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.
> 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 for 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).
> Without a thriving mathematical community to point out these things it would have stayed broken.
And that's a bad thing. If that 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.
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.
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."
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
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.
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.
> 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 the normal courtesies of "regular order", just as you would not with an AI lawyer.
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 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.
I'll add that as a retired person myself, I have found things to do with my time that seem (reasonably) useful. At the moment that includes writing a computer program, substitute teaching at the high school level, and occasionally writing a sci-fi novel. How much of that the average person could or would do if they had no employment in the post-scarcity world, I don't know---and for that matter, most (maybe all) of these would be replaced by AI. The point: what are people going to do to make their lives seem worthwhile? Which will add to the social upheaval and unrest you rightly predict.
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.
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.
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.
> 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.
> Anyone with access to a sufficiently advanced model has the capabilities of analyzing these papers/proofs.
No, no 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 commercial players who become rent-seekers. That's not really "gatekeeping" in any conventional sense of the term, it's protecting a healthy economy of ideas.
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 happens 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 that 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.
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.
This company is just irresponsible. We (at least, Americans that vote and can therefore decide indirectly what’s legal) should not allow them to continue.
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.
This is pretty standard. Important to note that these "errors" (* not really errors) themselves were caught by an LLM, further proving their usefulness.
* The reason you shouldn't consider the withdrawals to be caused by errors is because this is pretty standard in math and development. "Errors" like this are a core aspect of science and it happens _all the time_. And from my research LLMs have a far lower error rate than even the best human scientists.
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.
It's so funny to see people on Hacker News talk about academic communities that they clearly are not part of. To be clear to anyone reading, no, retracting papers is _not_ standard in math. In math, people submit papers after they have checked with colleagues, they give seminars, they submit it for peer review, etc. It is not shotgunning papers and retracting incorrect ones on the regular. Retracting papers is rare and embarrassing.
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.
What do you mean by "the social aspects of math" here? Even some of the earliest known mathematical texts (like the Rhind Papyrus) contain evidence of a social aspect of math. And certainly mathematical discussions occurred among the ancient Greeks. People have been exchanging mathematical ideas for millennia. If you mean to say that the current academic organization of mathematics is a recent phenomenon, that's certainly true. But pretty much all the math history we know has been people communicating with each other, evaluating each other's ideas and developing them further. Given this, I understand why people are worried if the field should suddenly take a non-social form.
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.
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.
I guess I feel two ways about this. It does could be a "working with the garage open" sort of thing where these are known to be unverified and they're just letting people see the sausage being made.
But that also means marketing and PR should shut the fuck up until things are verified. And they should more clearly annotate lack-of-verification status on their repo.
I believe this is nice marketing trick. Don't have human names have following effects
- AI can work alone and produce value
- There no person whose career on the line, and who is responsible.
- You can skip lot of time on verification of papers, and just show as it is.
Goals of marketing people obviously don't aligned with science goals.
Sure, unverified claims are unverified so there's a real risk of reputational tarnish. Why is it anyone else's job to verify a papermill? Would any journal accept an article that doesn't name people who are accountable? It should correctly be viewed as abuse of peer review. Let them rot.
Those results were not dumped to advance math. Those results were dumped to generate positive press for OpenAI.
Now it's on actual mathematicians to figure out whether the proofs are bogus or not. But the mistakes will never reach the same level of public attention as the original positive press, so for OpenAI this is good anyway, consequences be damned.
In a sense this is a microcosm of AI usage in the wild, ignorance is laundered through LLMs, and it is left for those that still have knowledge to figure out what makes sense.
OpenAI is a horribly negligent company. The threat it poses to humanity is not that their models will be a superintelligent singularity that will take over the world, is that their negligence and greed has real world consequences that they really don't give a fuck about. Like right now, their shitty math bruteforce is just keeping actual specialists occupied trying to figure out what is bullshit from what is not. For free, mind you.
People keep calling this "a PR stunt", but from a PR perspective, it seems they went about it in the least PR way possible.
No announcement, no press blast (big orgs have press contacts that they feed big story tips to), they just quietly dropped a blog post and a link to the repo on a tuesday evening.
I get we really want to have some kind of negative framing here, but lets at least not lose track of the ground truth around it. In a parallel universe this was easily headline news that made it to water cooler chat the next day.
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".
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.
Picture a remake of Good Will Hunting, where Will is an AI and, instead of getting the mathematical formulas correct, he just mass dumps a bunch of nonsense and the professors have to go through it all, pointing out where it is wrong. The professors know that AI Will isn’t as smart as people say, but their funding depends on it, and if they prove it, which they can do easily, it may just tank the whole economy, causing a depression, all because they have history’s dumbest President in office.
Tao and most anti/critical ai math folks remind me a bit of the brhamins in the hindu caste hirarchy system... whilst others fought (kshatriyas), farmed/traded (vaishyas), built things, cleaned roads etc (shudras), the brahmins were the high priest doing science, stronomy, religion ...
AI is this strange modernist machinary that kind of threatens that brhaminic role... its almost like the vatican vs post industrialization world .. where they still have to keep making the case for why religion/priesthood/god is important... even as the tech/science world starts operating on totally different terms...
flooding the system with parts that may be incorrect hurts the whole process and will get people to tune out (like politics). Can't see the International Mathematical Union making a similar mistake because it would do reputational harm. But the models don't care about their reputation. Bad for the layman - like me - to know what to make of all this.
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.
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 proving giant theorems 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.
My point is that if a proof is wrong or incompletely stated, we can just revise it and fix it. This differs completely from the way that mathematicians have historically operated.
It’s better to just publish something that you think is correct and if you find out it’s incorrect, try to fix it later.
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.
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.
I'm sorry but this is _obviously_ not what I think. I _obviously_ don't think that merely typing a statement into Lean gives us a magic Lean proof. I am even aware that such a SuperLean is not even theoretically possible because of undecidability/halting problem/etc.
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.
LLMs are very good now - meaning you do actually need to check the proof to make sure a misaligned agent didn't reward hack by exploiting some issue in lean or adversarially incorrectly formalize the statement in a way that's subtly wrong and easy to miss when you're trying to dump 75 trillion proofs on the Internet to drive hype that also makes the proof easier to solve. Probably also something you can use ai to help with though - I'm sure the other lab is having a bunch of llms adversarially review all these proofs since finding issues hypes _their_ IPO cycle. As the software world is learning - don't review ai code until a different ai has reviewed it lol.
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.
It should be noted that it wasn't a legitimate attempt at the collatz conjecture. Someone found a lean bug and created the proof to show it off. It wasn't an llm reward hacking (but this still is a concerning risk). Lean probably isn't the best kernel for adversarial proofs, but it probably has too much momentum at this point for anything else to take over.
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.
The huggingface hack is a reason to be skeptical. Thats a pretty clear instance of a misaligned model and the models are undeniably very good at this point. Meaning also good enough to reward hack by finding and exploiting holes in lean or adversarially formalizing the problem in ways that are deliberately subtly wrong in ways that are hard to check but result in formalizing a problem that's easier to solve. There are pretty strong incentives (hype for IPO) for creating conditions that drive that kind of misalignment
If it's anything like programming, then LLMs are still worse than the best developers. If you give them any freedom then they choose worse solutions than what's possible by any metric about 50% of the time. If they don't need to invent anything at all, they are great, otherwise they are bad. The only metric in which they are better is speed. For example the other day I used Claude for an anti accidental double clicking mechanism on Android Compose. I even listed, and give examples what it should do, what shouldn't, and I give the freedom to choose an exact solution (it's a very simple problem). About half of the code wasn't needed. And some of them caused real problems. Also its solution was far from good. It was error prone as hell. For some reasons it didn't handle at the point where clickability is defined, but one layer up with more boilerplate than it needs... which is not great at all. They also cannot handle flows well at all. It works for PoC, and for quick tests, and nothing for any complexity even a little bit, like having the same screen twice on the stack. But of course, if it has an example, how it should be done, then it copies the logic well.. Also we vibe coded a website recently. There were a ton of bugs on the happy path, which were considered finished by its creator. I don't even want to imagine what's with error cases, which I'm quite sure nobody tested.
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".
I think this is now an interesting part about LLM based automation. The scientific community is quite strict on references. Even with its most advanced model ChatGPT isn't reliably able to tell me if an online shop has an item in stock. Then the other part is peer review which isn't optional either.
Yes, the whole point of captchas is to capture automated systems. I used captcha as an example. There are a whole host of other anti-bot countermeasures.
That's crazy. You mean to tell me that the system which is supposed to replace my job as an attorney can't figure out if it's a motorcycle or a car?? I'm not so sure that's true.
When You See One Cockroach, There's Probably More.
This can and should erode our trust in every single proof OpenAI published. The model is clearly faliable despite the lean proof, and clearly the output was't actually checked properly before release. Once these proofs are peer reviewed and published in a journal we might be able to trust them again but until then they are just slop, sadly.
I think OpenAI actually did the right thing by sharing everything with the whole community right now but I also hope that some significant credit will now go to the reviewers who confirm these 'proofs" actually work.
Fantastic. Let’s also apply this reasoning to math papers written by humans too?
Humans produce flawed Lean proofs. Indeed LLMs were successful at finding and fixing many issues in the “core” standard library if I recall correctly. Humans regularly produce flawed papers and have minor issues require fixing. And when it happens it often isn’t as prompt and clear as this.
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.
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.
Undermining your point is that math papers don’t get published in nature and most math papers just go up on arxiv not journals. Are you sure you’re familiar with how academic mathematics works?
I picked Nature because it's the best known academic Journal. I'm aware it's not a mathematical journal. I don't think that undermines my point since mathematical journals obviously exist although they lack name recognition with a general audience.
I am pretty sure that journal publication is the norm. I do know mathematics although I am not one myself. The mathematicans I know want/need journal publications as unpublished research isn't counted in their research output. I know Arxiv is typically used for preprints while awaiting review but publication is always the aim.
> The mathematicans I know want/need journal publications as unpublished research isn't counted in their research output
If they’re untenured sure. Tenured mathematicians care a significantly deal less.
> Don't take it from me though. zbMath did a study finding 60-70 percent of arxiv papers on math end up in peer reviewed journals.
Elite journal capacity didn’t expand. There’s just a bunch of mid-tier journals helping to absorb the increased publishing to help these ~indentured~ untenured professors.
Tenured mathematicians care about publication. My impression is that this is because they believe in the process of peer review. However they also have other incentives as their publication record affects their ability to attract research grants. They also publish because they share as authorship with untenured students and postdocs who need publications for their own Tenure tracks.
You are right that most work gets published in mid tier journals. These are still peer reviewed. The difference is that they have a lower bar for impact. The bar for correctness is still very very high however.
The papers were all in a 'preprint' directory in GitHub. Academic mathematicians seem to think all research should happen in secret until it's completely proven.
But how much more progress would have been made in the last 100 years if they collaborated in real time? Watching the work someone is doing and spotting errors, or making suggestions would be a good thing. Unless the goal is simply to claim credit for a discovery vs the discovery itself.
What are you on about. The papers are held to scrutiny, this is how it works. If you put something out there, you should have done the due diligence of checking it (which is how these errors were found, with their own weaker model!). Being a smug prick about checking results that were announced as progress is less than worthless.
It's a little strange to write a comment attacking strawman "academics" with the structure of a partisan political attack ad in response to OpenAI making a mistake.
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.
324 comments
[ 2.0 ms ] story [ 55.4 ms ] threadIf 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.
And that's a bad thing. If that 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.
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.
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."
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.
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 the normal courtesies of "regular order", just as you would not with an AI lawyer.
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)
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.
I'll add that as a retired person myself, I have found things to do with my time that seem (reasonably) useful. At the moment that includes writing a computer program, substitute teaching at the high school level, and occasionally writing a sci-fi novel. How much of that the average person could or would do if they had no employment in the post-scarcity world, I don't know---and for that matter, most (maybe all) of these would be replaced by AI. The point: what are people going to do to make their lives seem worthwhile? Which will add to the social upheaval and unrest you rightly predict.
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.
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.
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.
No, no 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 commercial players who become rent-seekers. That's not really "gatekeeping" in any conventional sense of the term, it's protecting a healthy economy of ideas.
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 happens 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 that should be understood as what’s going on now as mathematicians look over the papers and find flaws.
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 reason you shouldn't consider the withdrawals to be caused by errors is because this is pretty standard in math and development. "Errors" like this are a core aspect of science and it happens _all the time_. And from my research LLMs have a far lower error rate than even the best human scientists.
Or is it the kind of research you'd prefer to keep shrouded in mystery?
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.
Source: Ass, My
But that also means marketing and PR should shut the fuck up until things are verified. And they should more clearly annotate lack-of-verification status on their repo.
Goals of marketing people obviously don't aligned with science goals.
Just had to get that PR stunt out to bump their valuation.
Vibe coding math research is just next-level AI slop.
Mind you, this is a competent AI company that's making these mistakes.
I can only imagine what non-technical people are putting out in production via vibe-coded AI slop.
Those results were not dumped to advance math. Those results were dumped to generate positive press for OpenAI.
Now it's on actual mathematicians to figure out whether the proofs are bogus or not. But the mistakes will never reach the same level of public attention as the original positive press, so for OpenAI this is good anyway, consequences be damned.
In a sense this is a microcosm of AI usage in the wild, ignorance is laundered through LLMs, and it is left for those that still have knowledge to figure out what makes sense.
OpenAI is a horribly negligent company. The threat it poses to humanity is not that their models will be a superintelligent singularity that will take over the world, is that their negligence and greed has real world consequences that they really don't give a fuck about. Like right now, their shitty math bruteforce is just keeping actual specialists occupied trying to figure out what is bullshit from what is not. For free, mind you.
No announcement, no press blast (big orgs have press contacts that they feed big story tips to), they just quietly dropped a blog post and a link to the repo on a tuesday evening.
I get we really want to have some kind of negative framing here, but lets at least not lose track of the ground truth around it. In a parallel universe this was easily headline news that made it to water cooler chat the next day.
From the "Introduction" section of that paper: "The constants and thresholds in the construction are extremely large".
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.
https://www.smbc-comics.com/comic/equations
AI is this strange modernist machinary that kind of threatens that brhaminic role... its almost like the vatican vs post industrialization world .. where they still have to keep making the case for why religion/priesthood/god is important... even as the tech/science world starts operating on totally different terms...
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 proving giant theorems 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.
It’s better to just publish something that you think is correct and if you find out it’s incorrect, try to fix it later.
[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.
Good question whether Lean is enough.
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.
That’s almost certainly due to things like captcha or something. What’s the actual shop you are referring to?
This can and should erode our trust in every single proof OpenAI published. The model is clearly faliable despite the lean proof, and clearly the output was't actually checked properly before release. Once these proofs are peer reviewed and published in a journal we might be able to trust them again but until then they are just slop, sadly.
I think OpenAI actually did the right thing by sharing everything with the whole community right now but I also hope that some significant credit will now go to the reviewers who confirm these 'proofs" actually work.
Humans produce flawed Lean proofs. Indeed LLMs were successful at finding and fixing many issues in the “core” standard library if I recall correctly. Humans regularly produce flawed papers and have minor issues require fixing. And when it happens it often isn’t as prompt and clear as this.
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.
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.
I am pretty sure that journal publication is the norm. I do know mathematics although I am not one myself. The mathematicans I know want/need journal publications as unpublished research isn't counted in their research output. I know Arxiv is typically used for preprints while awaiting review but publication is always the aim.
Don't take it from me though. zbMath did a study finding 60-70 percent of arxiv papers on math end up in peer reviewed journals. https://ems.press/content/serial-article-files/47210.
If they’re untenured sure. Tenured mathematicians care a significantly deal less.
> Don't take it from me though. zbMath did a study finding 60-70 percent of arxiv papers on math end up in peer reviewed journals.
Elite journal capacity didn’t expand. There’s just a bunch of mid-tier journals helping to absorb the increased publishing to help these ~indentured~ untenured professors.
You are right that most work gets published in mid tier journals. These are still peer reviewed. The difference is that they have a lower bar for impact. The bar for correctness is still very very high however.
But how much more progress would have been made in the last 100 years if they collaborated in real time? Watching the work someone is doing and spotting errors, or making suggestions would be a good thing. Unless the goal is simply to claim credit for a discovery vs the discovery itself.
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.