Hacker News Reader

Comment by ComplexSystems | Hacker News Reader

I can't relate to this at all. AI models will surely get better at writing "enjoyable proofs," but for now the situation is what it is. You're passionate about this problem, right? But you don't want to do the work to understand the result? Fine. There's a new generation of younger, hungry mathematicians that are highly interested in figuring out why the result is true and I am sure they'd be happy to wade through it and spoon-feed you the answer instead. Maybe they should be running things.

View on HN

Knowing a few PhD candidates and non-tenure track postdocs, the “younger, hungry mathematicians” are more worried about finding a damn job in the poorest job market - both academic and in industry - in a decade.

They don’t have any more patience for this.

Seems like an excellent opportunity to learn how these new proofs work and be at the frontier.

Checking someone else's work carries a lot of opportunity cost, and is only fruitful if one can learn new methods which apply to the own work. This is pretty risky, especially without tenure!

I realize that, but when you’re out of a job, you may as well chew on something like this.

When you are out of a job that's probably the last thing on someone's mind. Will I be able to pay rent for next month is probably their first thought

There are plenty of mathematicians who think the results are interesting. Not only do they have the "patience" you speak of, some even seem to be enjoying exploring the new results.

Your point would be stronger with links to such discussion.

No idea why you're downvoted, my intial thought was that I would like to see some of this supposedly widespread sentiment as well.

I even think it's plausible a lot of mathematicians are excited by it, but the sweeping confidence of the comment you replied to without anything to back it up leaves some to be desired

The problem here is that while you can call what OpenAI does "mathematics", I would hesitate to call it science. Science as a process of acquiring and developing knowledge within a domain involves a lot more than just dumping unfinished work on the scientific community. Among other things, it involves developing frameworks and understanding of the domain, formulating questions, creating results in a fashion suitable for verification/testing/replication, and relating these results to and integrating them with that edifice.

Have you looked around recently? Because there are plenty of mathematicians that are excited to read and learn about all of the new results. They've improved on the sub-n log n result and have even made a web site to track progress on it: https://beyond-n-log-n.netlify.app/

It looks like people are enjoying themselves, having fun with the new results, and generally doing all of the things you say "science" is supposed to be about. So what's the problem?

I didn't say it is useless. Consider Ramanujan, whose work gave rise to a lot of interesting math, even (and sometimes, especially) the parts that lacked proofs or had other gaps (probably because it was obvious to him unlike us mere mortals). But a singular genius, whether a person or a machine, does not science make.

why are AI sites so hard to read... is it the terrible contrast? or something? any designers here?

There’s so much information, but it has no idea where to put the focus. Why is the number of PRs the same size as the actual best result?

Kinda sounds like computer science vs developing - in the sense that people with a master's in CS and are dedicated to the craft will write wonderfully artistic software, while it doesn't actually take a love for the process to write code and get hired at some tech company (even less so now with agentic development).

Not what I am getting at. In fact, the problem I am getting at is the abolition of existing scientific and engineering principles and processes without a replacement and applies to programming with agents as well. This is not about artistry, but about building durable things.

Except for the fact that academia today is bs:

https://www.youtube.com/watch?v=LKiBlGDfRU8 https://www.youtube.com/watch?v=shFUDPqVmTg

"AI models will surely get better at writing "enjoyable proofs,"" why? Why is that surely true? they've increased in all other capacities at shocking rates while still writing awful, slippery, turgid prose. Very silly to assume that this will just go away.

I think it’s silly to ignore the sheer rate of progress that’s occurred in the last 5 years. Compare gpt 2 output to latest foundation models and then re-read your comment. You’ll realise just how out of touch you sound.

The tech industry is chock full of straight up magical thinking, and nobody shows it more than AI boosters.

Every single day now, for close to 4 years, ever since ChatGPT 3.5 was released - there's been people dismissing AI progress. Every step of the way.

It is entirely possible that one day progress just stops or slows down, but with current evidence, I don't find that too likely - at least not in the near future. The sheer amount of resources being put into this (AI) race is mind-boggling.

So while past performance does not guarantee future results, I'm just going to kick back, and assume that many of the current issues will be fixed with future models.

The progress is clearly not uniform though, it’s shaped by how amenable things are to collecting data and verifying computation. I think writing clear and cogent prose is harder to quantify than formally verifiable logic, and this is why progress in coherent communication has been slower than raw problem solving ability

Maybe this is just a matter of what model developers choose to invest training resources in, but I don’t think it’s inevitable unless clarity is made a higher priority

OP is not dismissing AI progress, they're saying there's been no progress in writing better.

Which is false. Any of the sota models write far better than chstgpt that was released 3 years ago.

I think that would be very difficult to say. Good or bad writing is subjective.

Compare gpt-2 to todays foundation models. If you think writing hasn't objectively improved, you are willfully ignorant or a moron.

Doesn't address my point at all and I did not dismiss AI progress.

Yes it does address your point. Maybe actually read what he wrote.

> There's a new generation of younger, hungry mathematicians that are highly interested in figuring out why the result is true

The problem is that right now mathematicians don't have the economical incentive to read these AI generated results. Even if you love mathematics and all that, it's always more important to get a job, and for that it doesn't seem like a good idea to invest time around problems that AI touches because you can't compete with it and you don't know if tomorrow they'll improve by x10 the sota.

I am a mathematician, and I do have the incentive to read the results. Two results in the drop were two major life goals of mine, and all I got was three lousy citations. :) But a third question I've spent a lot of time on is a not-so-hard consequence of one of the lemmas in there. So, yeah, I do have the incentive.

Of course, it's not clear at this point whether reporting such a result even matters, but still. In its own right, it's a very cool result.

Thanks for your perspective, genuinely.

What do you do if those results suck like in the article?

I think quite a few mathematicians would be interested in using AI to figure out the answer.

But providing the answer in gibberish along with a certificate is not that, it's at best a cruel way to do it, but I'm leaning towards the idea that it's a fundamental misunderstanding of what it means to do math and what it means to communicate a result.

If you think sending an answer in gibberish is acceptable just because it's true then SSdtIG5vdCBzdXJlIHdoYXQgdG8gdGVsbCB5b3UsIGJ1dCB3ZSBkaXNhZ3JlZSBvbiB0aGF0.

Like all the junior devs getting opportunities left and right.

The question is why the situation is what it is. Did OpenAI publish a large volume of unreadable proofs because that was their best attempt to contribute to the field of mathematics? Or does OpenAI feel that it’s more profitable for them if people come to see mathematics as something that’s less focused on understanding and more focused on using AI to generate proofs?

Even with humans, the first publication is rarely the best expression of the lesson. Getting published does more than establish priority; it also frees up the community to build on the result. Nobody expects a human to wait until the proof is comprehensible to anyone except themselves and the referees.

I don’t think that’s true? I never did research math myself, but the people I’ve known who do would definitely invest time in making a proof clearer and better even if they had the idea basically correct. There’ve been multiple recent stories of researchers saying “we’re going to publish this lame proof that isn’t up to our standards because the AI companies let us know they’re going to scoop us if we don’t”.

Mathematicians care a lot about the exposition of their ideas, invest a lot of time in giving talks, writing, and don't publish too frequently, compared to other sciences.

They normally don't feel like they are in some kind of race to publish the results ASAP and claim priority. Cases like that are very rare (but they get media coverage because they are so unusual).

OpenAI did a publicity stunt, their motivation is not to make a good contribution to the field, which has very different standards and culture, compared to the AI labs.

Yes, I guess it matters a lot whether this was quite close to the best they could do or the best they could do given specific resource constraints or whether they just didn’t bother to try doing better (eg to invest more tokens into readable papers)?

> I guess it matters a lot whether this was quite close to the best they could do

As the author of the post points out, there is no way this is “the best they could do”. It’s a write up that didn’t involve someone with the math + communication skills required to clearly explain the result.

How about the scenario where they are already better if you give them more time/tokens/…? Would it be a more relatable concern in that case?

So OpenAI should be able to flood the world with AI pollution and ask scientists and mathematicians to wade through it all and tell us if there is any sense in it, then sit back and wait for them to report in?

Nice idea.

OpenAI in fact didn't know what to do with results and didn't want to flood the world, so they asked mathematicians. Mathematicians recommended OpenAI to release them. My guess is it would have been better for OpenAI if they didn't release them. OpenAI is basically doing this as a goodwill.

(See https://agmai.org/general-sep29/ for the recommendation in question.)

People seem to have very misguided ideas about why OpenAI is doing this at all. It is not to brag or to torture mathematicians. It is an eval. OpenAI is known to be willing to pay large amount of money to get a good eval, think FrontierMath. FrontierMath is now saturated, so they need a replacement eval for math. Open math problems are actually a fairly good eval, although a proper eval is better (eg FrontierMath has known difficulty and have tiers from 1 to 4).

Mathematicians would prefer if OpenAI didn't use open math problems as an eval, but OpenAI is not obliged. I actually think OpenAI wouldn't point AI to open math problems if unsaturated FrontierMath Super Duper is available, as it just angers mathematicians, but such eval is not in fact available. Given OpenAI used open math problems as an eval, they could just throw out the result (this is in fact better as an eval since it will keep problems useful longer), but mathematicians preferred to see the result. So OpenAI released them.

How is solving unsolved problems a good eval? Once a problem is solved and released, you can’t evaluate a future model’s ability to solve it.

As I said, a proper eval is better, but it measures something real that gives a good training signal, and there is lack of good alternatives for math eval. Since the result is 372/4000, it is also unsaturated.

I think this is right - it can be seen as trying to get free feedback from the community. In that way it’s reasonably described as exploitative, since it’s not a good faith effort. The problem of ai slop being submitted to conferences to get publication counts is similar.

"Mathematicians recommended OpenAI to release them."

This is a misleading characterisation of the mathematicians' position.

The very first paragraph of the AGMAI recommendations explicitly states:

"we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models." You appear to have acknowledged this by saying “Mathematicians would prefer if OpenAI didn't use open math problems as an eval…”.

The mathematicians did not ask OpenAI to produce these results. They explicitly asked AI labs to stop producing them in this manner. Their subsequent recommendations concern what labs should do if they have already produced significant results, not an endorsement of the practice.

Furthermore, the recommendation was not simply to release the results, but to responsibly release already existing results. Section 2.B, Step I, explicitly recommends "...labs that have AI mathematical output that is not understood by the people who prompted the AI systems", to search the literature for relevant prior work, provide appropriate attribution, and improve the exposition of AI-generated proofs before releasing them, rather than leaving this work to mathematicians afterwards.

OpenAI published the results on GitHub while still exploring repositories that meet the committee's guidelines. So they followed some of the recommendations, but not all of them and hence, did not release the results as requested by the mathematicians.

I do not think it is a settled matter whether this was done out of goodwill. This is because releasing these results as they were can benefit OpenAI more than releasing them according to the AGMAI recommendations. AGMAI recommended in section 2.B, Step 1.5 that "Each time a solution to a problem is released, it should be clearly documented how exactly AI came to be used on that particular problem. If many results are released at once, then in addition to the results themselves a further document should be written and made public that references all of the released results and explains how many other problems of comparable difficulty the models tried and failed to solve, as well as how the problems were chosen." If the results are released, it is easy to expect that the media will discuss the capabilities of the AI used in the work, as indeed happened. If this AGMAI recommendation was followed, the media would plausibly have also discussed the number of failed attempts and then the overall attitude would not be as favourable to OpenAI as it is now when it comes to the capabilities of the AI that was used. OpenAI did release on GitHub that approximately 4,000 problems were attempted and resulted in 719 manuscripts (after 3 containing suspected errors were removed by OpenAI) across 372 families of problems, but this does not give a calculable number of problems it failed to solve. I do not claim to know OpenAI's intentions or reasoning when these results were released and am not arguing that it was done with improper intentions, only that whether it was done out of goodwill is not a settled matter.

AGMAI's October 6 statement explicitly clarified that its advisory role should not be interpreted as an endorsement of OpenAI's process, and that it was up to the mathematical community to assess how successfully its recommendations had been followed.

Recommending how to responsibly handle the outcomes of something you oppose is not the same as asking for it to happen.

It is also worth adding that the Association for Human Mathematics published a statement (which Tao reposted on his blog) in which they explicitly say the following:

> Mathematicians did not ask for this work to be done. The Advisory Group on Mathematics and Artificial Intelligence, from whom OpenAI has claimed to derive its legitimacy, opened their initial advisory statement by saying that frontier AI corporations should not test advanced mathematical problems on internal models. In ignoring the central premise of the Advisory Group’s position, OpenAI has indicated total disregard for the norms of scientific research — norms that guarantee that mathematics remains trustworthy, ethically researched, and in the public interest.

https://www.ahmath.org/

>> I do not claim to know OpenAI's intentions or reasoning when these results were released and am not arguing that it was done with improper intentions, only that whether it was done out of goodwill is not a settled matter.

That's right honourable of you but for me it is very clear that the only incentive in AI companies' effort to produce mathematical results is to advertise their technology. There is no reason at all to assume they have any other motive; certainly not any kind of interest in mathematics as such.

Any idea what sort of percentage the sentence

> supported by a clear plurality of respondents

was referring to?

Yes, they should. They have invented a magic button that can tell you the long-awaited answers to the burning mathematical questions that you've spent your life researching. The caveat is that the technology is still new, so the explanations "are not fun to read" like set theory papers usually are (lol). If you don't think that's a worthwhile tradeoff, that's your call, but it sure as hell isn't everyone's.

I don't think the claim is "they definitely have an oracle that solves the problem, and I reject it because it's hard to read". The claim is "OpenAI claims to have used an oracle to solve the problem. The proof is very difficult to read, and to even know if it does or not, we have to go through it with a fine-toothed comb, but they're going around claiming they definitely solved the problem (or at least getting press that claims that which they aren't pushing back against) and this might convince the people who sign grants even if it isn't true"

People who are invested in the idea that we've invented a general intelligence, now, which includes all these companies that are literally financially invested in this claim they are making, will tend to believe that its results can already be trusted in domains like this. Some mathematicians seem to believe some of the proofs written by their models, and some, like this one, don't. I do think it's valid for an expert to push back against the claim that the best use of their time right now is to verify the poorly written work of everyone who's claimed to solve the problem

Over the year, nothing they've released with a lean proof attached has turned out false (That's sort of the entire point. It's not impossible but it's really difficult). There's a reason most mathematicians, including the ones vehemently against OpenAI's dumping are not arguing the results are secretly false or have a high potential to be. And indeed, if that were the case, it would quickly become apparent and all this worry about grant signers would vanish into the wind. It's very easy to ignore nonsense. The problem is that it isn't nonsense.

> Over the year, nothing they've released with a lean proof attached has turned out false

That's not true. [0]

> On July 25, Ramana Kumar published a repository containing a sorry-free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types.

Even in this dump we're talking about, it hasn't been true. [1]

> In “Algebraicity of Weil classes on split abelian eightfolds” a sign error invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers.

[0] https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...

[1] https://github.com/openai/math/blob/main/history.md

1. That wasn't from Open AI or any major lab. I don't know what random people are getting to. It's curious also that it had no natural language proof attached. Usually these labs have a NL proof then translate to lean. Lot less possibility of lean maxxing.

2. None of the results Open AI retracted had an attached lean proof

I really don't know enough about it to know whether you're right or not, nor do I know whether or not you know enough to make the claim you're making, so I won't make an argument one way or another because it's non-sequitur to what I said anyway. The fact that you or I or Sam Altman or Terrence Tao believe the claim is irrelevant to whether this obligates the person who wrote the blog post to believe the claim, and it sounds like he's willing to consider the possibility that it is right, and would read the paper if it reached a threshold of comprehensibility expected of people making that kind of claim.

I's not a non sequitor because it cuts right to the point. He's under no obligation to read it sure, but that doesn't mean Open AI isn't justified in claiming to have proved it. The justification isn't Sam Altman's belief or Tao's or anyone else's authority. Results accompanied with lean-verified proofs whose formal statements match the problem at hand have arguably stronger justification than the vast majority of human math publications.

I don't understand. Why is this the onus of scientists and PhDs to review whatever results OpenAI had dumped out? If OpenAI had produced incomprehensible papers, surely any journals would just reject it, or demand the author to do a complete rewrite? Unless we are talking about a race to solve problems, which PhDs are afraid that they had been scooped up on?

The problem isn't just that the papers aren't fun to read. The problem is that a lot of the research that goes into solving these issues leads to other discovers, new fields to explore and people have to develop new approaches to solve them. The other part of it is, the quality and the enjoyment of working on these problems leads people to find new and other interest problems to work on.

If you just strip mine the answers and Sam Altmans magic button solves 100/100 problems, what's next? Who is left to come up with a new interesting question for the magic button to solve?

Lastly, life and the present moment is all there is, if there is no enjoyment in anything we do, then what's the point of all the "living for ever" Altman et al want to achieve.

We will live forever to read boring papers generated by LLMs? Literally sounds like an eternal hell.

People are already finding stuff in the release to get excited about, and as the models get better at distilling proofs to make them more coherent, this will only amplify. Of all the things to worry about, human curiosity and the ability to run with new ideas probably aren't at stake.

In fact, I can't remember a time when I was more excited about the future of science. This could herald an end to the replication crisis, and kill off bullshit science completely. The danger of course is that we end up with two companies effectively dominating cutting edge research in every field, but it remains to be seen if that's even possible given the pace of improvement in open weight models.

Nuclear fusion is already proven by the universe to be a viable energy source by the fact that the sun exists but people still work on understanding and taking it and developing new approaches to accomplish it. People didn't stop experimenting with and developing programming languages because technically they're all turning complete and the first one was "enough." Y'all will be fine - every JavaScript framework that exists is someone looking at a theoretically correct and complete solution and deciding actually it sucks and they could do better. "I want to understand xyz but the proof is trash and I think it's ugly" will be plenty motivation for a lot of people to work on it.

How is the journey to understand fusion related to not wanting to spent your limited time on earth wading through AI slop?

You don't have to wade through the slop. The point is a giant star in the sky figured it out and that doesn't demotivate you from figuring it out yourself

Here's a guy who's made a "beyond n log n" tracker: https://x.com/aurel_pr/status/2108214135179944096

He's tracking the community progress on sub-n log n multiplication. OpenAI started with 1 - 1.63e-55. The result has been now improved on 115 times, and the current record is "rohanarun"'s 1 - 9.87e-5. I'm sure by tomorrow it'll have improved again.

Does this look like people aren't having fun? Does it look like they aren't discovering stuff? It looks like it's spurred a cascade of interesting community activity. It doesn't really seem much different from what happened with the twin primes conjecture. Isn't that supposed to be the point of all this?

Some people are having fun doesn't negate the rest of the issues with this sort of thing.

then the rest of them can pound sand.

They should certainly be allowed to share their findings. No one is forcing scientists and mathematicians to review the findings in general. It’s just the case that the findings are of such such a quality that it would not make sense to ignore them wholesale

> No one is forcing scientists and mathematicians to review the findings in general.

This is like "no one is forcing software engineers to use AI tooling" or "no one is forcing you to show your ID in the airport" or "no one is forcing you to own a car in your small midwestern city" - there can be no law requiring something and the practical consequences of not doing so can be so painful that you're effectively forced anyway.

That is exactly what I’m trying to say. The findings are of such such a quality that it would not make sense to ignore them wholesale.

That’s why it doesn’t make sense to present AI companies as dumping or burdening the scientific community into doing labor for them; the scientific community is self motivated to do so.

It's not self motivated. The motivation is not "this is doing amazing things for us", it's "if we don't review this, the bullshit headline complex and the bullshit-spewing (sorry, marketing) departments of tech giants are going to misinterpret/misrepresent everything and our grant money will be taken away".

add "no one is forcing you to own a smartphone"

The best part is that when the academics fix OAI’s issues, the model gets better and OAI shareholders get richer and more powerful!

As someone who uses LLM tech occasionally, this is why I prefer using open local models. If I’m making myself obsolete, at least I’m not making some asshole richer and their closed model better.

No, they don't have to ask. Those interested enough will jump at the opportunity, even if it's just to be "one of the first to get it".

You know, I kinda relate to the feeling of not wanting look at those outputs if I think of it from a layman's perspective.

I just imagined that instead of math papers, they released 700+ feature length films, and the only way to tell if one of them is any good is to watch it in its entirety.

That feels pretty unappealing to me.

I know it's the same for human made films, so what's the difference right? But those are good enough most of the time that it's a decent bet, and the people that made them had real skin in the game.

Contrast that with something made by a nondeterministic slop machine with no skin in the game where small details can be off in a way that's jarring. Right out the gate I have an aversion to committing that much time to something that very well may waste it.

That's actually a really interesting thought. Given Sora, and the amount of funding they have, they could have created started their own film festival and dropped 700+ feature length films, had they wanted to go in that direction. But they didn't. Hmm.

From the perspective of "is this just a garbage dump to impress the market?", it's way too easy for investors to figure out 700 films are garbage.

What else should they do? See these models get smarter and smarter, somewhat-solve things but only to the tune of 90% what mathematicians (or experts in any other field) would deem acceptable, and then gate keep the findings for the next few years going through peer review and paywalled journals? I for one welcome the flood, bring on more in every possible industry and see where all that progress lands up. Sure it will upset a lot. A lot of things also upset the luddites.

Exactly.. this is an opportunity for people to pick up where the model left off and run with it. Like you don't have to, nobody is forcing you to.

However, there are always smarter, hungrier people out there and this is a buffet.

Some output is going to be wrong or incomplete. I am willing to bet even those have nuggets that can be used elsewhere.

> this is an opportunity for people to pick up where the model left off and run with it

Like people enjoy racing in front of a stopped train? As soon as they turn on the engine again, they will run you over. The questions that remain will be only the low value ones, not worth the effort to vacuum up.

So no, the smarter, hungrier people are not the ones that are going to swoop in. It will be the most desperate.

> Some output is going to be wrong or incomplete

This is a very human take on the situation. No, the Lean proof is not going to be wrong, and it will be incomplete only in the sense that OpenAI didn’t try to push the results further.

Are you going to be doing the work to verify the results ? Will you just expecting other people to wade through the flood and reap the benefits later on?

Nobody is forced to verify the results. I am honestly not expecting anything other than AI to get smarter and smarter and people who are motivated and interested enough to pick up after it; and potentially reap all the long term benefits ahead of those who aren’t (seeing this happening with software development in my own field). But in the end; if you don’t like it, you’re not forced to do anything.

Wondering if you read the article?

I think this might feel about the same as getting a PR from Claude that purports to solve some issue that it deems exists, but it doesn’t conform to the contribution guide, isn’t clear in its objectives and looks quite likely to be utter bullshit. I close them without comment and lock the issue.

You don't know what you're talking about. Just because it was created by an LLM, and verified in Lean, does not make it true. The whole point of writing a proof is for it to be understandable.

Suppose I directed some llm agents to factor the primes from network logs of your machine. I then publish the private and public key in full. You would not change your keys of course because its not true right?

My argument is that LLM generation and a correlated Lean verification are not sufficient conditions. Both are falliable.

"true" != "understandable"

It's a necessary condition

You're passionate about this problem, right?

There's a "Silicon Valley-ism" for you. We offer a thing in whatever form we want and people "who are passionate" will gobble it up, should gobble it up, 'cause they're "passionate".

Reply on news.ycombinator.com