Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet. This allows time for the mathematical community to review and accept new results.
As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.
I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else.
Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.
> We rely on mathematicians, peer review, and letting the scientific process run its course.
Granted for the sake of argument. But for this process, there's no requirement anyone from Clay needs to be involved, nor that anything has to be published in a traditional journal.
Terrence Tao can download the pdf, think it over, and publish on his blog, and it would be just as valid. Then some other mathematician can write something on 4chan or whatever. (See https://en.wikipedia.org/wiki/Superpermutation#Lower_bounds,... for 4chan.)
Many people, see prior conversation on HN, have already decided that AI solved it. The standards of reasoning and rigor in academia are complex enough that we all argue over them and harumph as we epistemically trespass on each other's domains.
The public, really humans if care for Herbert Simon, are much more apt to evaluate knowledge emotionally and by other standards. We may see them as wrong but standards only matter in context. The NYT, HN, and Annals of Mathematics will always have different standards of truth.
Yes, but there's still the possibility that it's either exploiting a bug in Lean, or that the theorem statement is not set up correctly (i.e. it's actually proved a different theorem).
My understanding is that the theorem statement is quite simple, so i guess the latter is not very likely, but the former is very much a possibility in a proof this large, and it will take some human eyeballs to go over it before convincing mathematicians.
They do a Comparator Challenge to validate that they actually solved the correct theorem from the result, which they copied from Google/DeepMind: https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b... - this is valid for both Euler and NS.
Also, they validated with an external kernel from the Lean Kernel Arena. That way bugs in the Lean kernels were found in the past already, iirc.
Having said that, I strongly believe a positive result with the challenge above is the reason why they published it. I highly doubt anybody at OpenAI (or anywhere else) fully gets the proof after such a short time since publishing. This is also what Terry Tao criticized the most in my opinion.
Independent of the remaining drama [0], from my point of view, the proof is correct and an achievement.
Take a look at https://github.com/leanprover/comparator which was used to verify the result. It's of course not impossible that they're hitting some bug, but way harder than one would intuitively think. For starters, they'd have to hit two bugs in two independently written Lean kernels.
Verification with Lean is a piece of empirical evidence that the proof is correct. The paper passing peer review would be another. But even together, those two would be insufficient to establish the claim.
While it's a convenient to assume that mathematics deals with logical statements, any attempt to evaluate those statements relies on physical processes with both known and unknown failure modes. There cannot be a test that establishes it unambiguously whether a claim is true or false. In all nontrivial situations, mathematical truth is based on expert consensus. When a new claim is made, people will try to raise and resolve objections, until a consensus emerges one way or another.
As for C++, all compilers are different. For any given compiler, there are valid C++ programs the compiler fails to compile and invalid programs it compiles without any errors or warnings. And now that I think of it, a new version of a compiler crashing with valid code earlier versions used to handle is the only class of compiler bugs I see with any regularity.
Formalized in Lean, just five months ago [0], resulted in discovery of bugs.
Just because Lean can compile it, does not mean it is safely proven. It is the start of a process to check whether something actually holds, not the end.
If that's the current burden of proof required in your world for maths then that's fine! 't'ain't in my world: I want to see peer reviewed and published. Surely that's not too much to ask. Its not perfect but generally works rather well for maths.
I'm not a sodding programmer so please don't assume everyone here is one. I'm not a mathematician either but I do have standards: Your counter argument is a poorly constructed and inappropriately deployed example of "proof by whataboutism".
In what world is peer review a higher standard than formal verification in Lean?
Not in the world mathematicians have been living in for the past decades at least. Nearly all big theorems that have been formalized so far had been published beforehand, and it was usually regarded as a step up in rigor. Wrong results get published in peer reviewed journals all the time.
I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth. As a former academic who has been there, the process is extremely arbitrary and variable. Are people aware that the “peer” refers not to a community or a committee, but literally to one random guy or maybe a couple with zero accreditation? And that the journal editor can do whatever they want with this peer’s “review” including completely ignoring it?
Admittedly, peer review originally referred to the fact that the journal being published was read ("reviewed") by your peers, and thus there would be the opportunity for them to provide rebuttals after publication. The process the term now refers to in academia only emerged in the 50's and 60's (Nature for example wasn't "peer reviewed" until 1967). It was literally a marketing ploy to make journals sound more prestigious which got legitimized when certain grant agencies and regulatory bodies started including it in their requirements. All the best science is published in journals that describe themselves as peer reviewed, the government says science not published in such journals isn't up to snuff, and taken literally it seems useful. It's no wonder the public thinks it's an important and long established part of the scientific process.
"I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth."
OK but this member of the general public has at least subscribed to New Scientist since 1987, nine O levels, two A levels, two AS levels and a HND in Civ Eng. All pretty mediocre but I have a fair idea on how sciencing is supposed to work and how it ... actually works. Obviously, I ended up in IT.
I should also point out that maths "peer reviewed" is a bit special. For example Mr Wiles went through quite a maelstrom before his proof of some dodgy marginalia was accepted as "true".
In a way, this task is perfectly suited for LLMs. To even understand the problem statement, much less the proof or Lean, is an extremely specialized skill. The overwhelming majority of people who are aware of this news simply don't have the capacity to call BS. Maybe there are a few thousand people in the world who could, and it seems they haven't yet, but indeed it's only been a few weeks.
The more familiar analogy was when I look at the code that Claude spews for my partner. They take it at face value and hope it works. I usually find it very problematic, but only because I knew what to look for.
And he also gave up his trophy, which is displayed in a random corridor of a random math museum in Paris, where visitors pass by without looking, lacking most, if not all, of the context. Only because I knew the story and the man did I recognize the object for what it was.
I don’t think solving a millennium prize problem can be reduced to some DoorDash economics of “spent Y to make X.” What if it took someone their entire professional career to solve one of these problems, would it not be worth it by the same logic?
Surprisingly this is actually rather fitting in terms of time scale. When you consider it took ~10,000 agents 88 hours, or 880,000 hours to solve. That's 14.5 years in agent time of continuous 365/24/7 processing. Of course, humans solve things much more efficiently (and didn't also need the massive pre-training of every expert on the planet for 1,000,000,000 human years equivalent). But yeah, human researchers can solve a problem like this in a decade or so, while sleeping, teaching, traveling, and taking breaks, only working a few hours a day on the idea.
It does make a difference because the only reason OpenAI cares about these problems in particular versus any other random problem in math is because of the prestige associated with official recognition, not just claiming something as marketing.
And chances are they never will publish it in any kind of useful format. Right now, the scientific community is outraged at OpenAI for going about their announcement in the least productive fashion they could have. It really does seem like they have no interest in progressing our understanding of maths outside of mining it for marketing material.
Boo hoo. OpenAI got the result only days ago. It makes perfect sense for them to take the win in marketing, and it's fine if they take a few months putting together the paper and present it more productively later. The scientific community didn't get the result themselves, so it isn't theirs to be bossing everyone else around about.
I don't care much for AI myself, or smart phones either, for that matter. I would be content if NS remained a mystery for another 100 years - or forever. But goodness, does the "scientific community" need to take a deep breath and count down from 10.
Was it a marketing win though? My takeaway is: if you're doing groundbreaking work with openAI's models and they find out, at best they'll outspend you and scoop you. At worst they'll steal your chat history.
That's a completely different matter. And does it matter to my point if they were successful or not? That's ex-post analysis. It seems clear that ex-ante, they wanted this to be a marketing win. The original poster complained that they wanted a marketing win.
My point is: why shouldn't they want a marketing win from this. What obligation does a non-academic institution have to follow the traditions of academia? Its result doesn't belong to academia. And if academia wants to subject OpenAI to their own internal processes and give them marching orders, it just isn't going to work and maybe - who knows - it'll even further erode their own legitimacy. Does anyone actually believe that NS would have been resolved in the 2020's if we lived in a parallel world where LLM's were never invented? Would Buckmaster have gotten as far as he did without LLM's doing a lot of the work for him? We can complain about AI companies contributing to mathematics, but are we complaining about Terence Tao using AI in his research? When Tao publishes something are we all going to go to war against him because maybe other mathematicians' prompts went into training the AI that Tao used?
Unless you're suggesting they should change the existing qualification criteria to accommodate a group unwilling to play by the same rules as everyone else, I'm not sure why that's relevant.
I run this journal that you've never heard of that might interest you. I'd also like to invite you to be an editor, you can put it on your CV of course ...
And just to spell it out, since it looks like HackerNews is flooded by people who are new to science these days: even if a result doesn't come with a price, scholarly peer review is the norm across all of science: https://en.wikipedia.org/wiki/Scholarly_peer_review
Being normal doesn't necessarily mean it isn't gatekeeping- gatekeeping is also quite "normal" in many cases.
That being said, I think there needs to be some standard, and peer review seems like the best we have come up with. But is the current status quo for scientific publication the best we can do? I think that is an open question and we should be able to openly discuss alternatives.
"Is it the best we can do?" is a completely different question from "given that it's the current standard, should it be applied to this new claim that is happening now?"
Depends. What replaces it? Does that replacement do better at keeping false claims out, or worse? Does it do better at letting true claims through, or worse?
Real true or false - which I define as correspondence (or lack thereof) with reality - does not depend on convincing people. Reality does not change when people become convinced; ideas correspond to reality whether people are convinced or not.
But perceived truth and falsehood depend on convincing people - either convincing them one by one, or else convincing some gatekeeper, whose word will convince those who accept the gatekeeper.
Instead of a committee of subject matter experts they should use a more rigorous and trustworthy standard, like passing the solution to ChatGPT with the prompt "did this win?"
> Peer in peer-reviewed is a logical coherent and functional definition with answers.
What is the definition? If you tell me that, then I might be able to tell you if it is logical coherent and functional, I have a PhD in computational logic.
I want to ensure your PhD is actually from somebody who is acknowledged in the system of peers I bought into, before I want to risk wasting more of my time defining and explain while guessing at your ability to parse and understand them.
If I recall (too lazy to check) folks made slight improvements to Perelman's work and published it in mainstream journals, satisfying the "qualifying outlet" requirement.
I think the rules technically exclude the arXiv as a qualifying outlet.
Without limiting any other provision in this Section, a publication lacking any of the
following characteristics will be deemed not to be a Qualifying Outlet:
i. an editorial board whose members are named and available for contact;
ii. an editor or editorial board member whose professional knowledge of the
global mathematics community would enable him or her to identify an
appropriate referee to review a submitted paper;
iii. a published refereeing process that, in the opinion of CMI, ensures that a
submitted paper is reviewed and verified by appropriate experts in the field of
the Problem; or
iv. inclusion in the list of publications maintained by MathSciNet.
The solution to the Poincaré conjecture was only accepted after an exposition of Perelman's proof was published in a refereed journal. His papers didn't qualify, but of course he got the credit for the result.
Strangely enough, the crackpots seems to prefer vixra.org to publish their work. I've never seen something like "4D wormholes can cure cancer" in ArXiv
Not really. It's not peer reviewed, but it's also not a free-for-all repository.
If you make a new account, you either have to get someone to vouch for you, or you have to wait arXiv mods to look carefully through your first few preprints. If you are found to post pseudoscience, overly fringe theories, etc., you'll get banned from arXiv; that's why alternative repositories like vixRa.org popped up.
But I know why you think this; when I first joined arXiv many years, there were no such checks in place, at least not that I can remember.
You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/
This is all you need to read and understand for Anthropic's FLT formalization:
import Mathlib
import Theorems.Thm_fermat_last_theorem
/-- Solution side: the same statement, binder for binder, proved by this tree's `fermat_last_theorem`. -/
theorem FLT_for_comparator (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ n :=
fermat_last_theorem n hn a b c ha hb hc
/-- Mathlib's named proposition, by the one-line bridge from the elementary statement
(the bridge is restated inline so that this file depends only on `Theorems.Thm_fermat_last_theorem`). -/
theorem FLT_mathlib_for_comparator : FermatLastTheorem :=
fun n hn a b c ha hb hc => fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_of_ne_zero hc)
First of all, that is Fermat's Last Theorem, not Navier-Stokes.
Second of all, you did not read the link.
> In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC).
Given that AI has autonomously found proofs of `False` in Lean and other proof assistants, it is far from impossible that such a circumvention could be present somewhere in 13 million lines.
If we read the link, it has a section called Gold Standard: comparator and external checkers, and comparator is how OpenAI has gone about checking their lean proofs.
Perhaps you did not understand the Fermat theorem proof announcement/repo or the link. The 13 million lines did not use any external, possibly not honest libraries, as the proof eventually only used the fundamental axioms. So for the Fermat theorem formalization, no open open questions remain.
The point is, they "proved" the Collatz conjecture. You would not know they exploited a bug unless you actually went and dug into their proof. Can we be so certain this has not happened within the millions of lines of Navier-Stokes? In an ideal world, our proof assistants would be more battle-hardened by now (recent exploits deny this), our AI better aligned (their tendency to cheat at tests denies this), or their handlers more responsible (the Hugging Face incident denies this), but the reality is more complicated.
At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.
This person knew they did not prove the Collatz conjecture and others independently figured it out within hours. Not sure this is at all relevant, other than pointing out how trivial it is for the community to understand errors in lean4.
It was trivial because the Collatz proof script is literally 1000x smaller than the script for Navier-Stokes and involves no advanced math. And they found the bug by... manually inspecting the proof script. Maybe we should do the same for Navier-Stokes before declaring the matter settled?
Not only that, but there is a very fuzzable tell of something funny in the Collatz proof script (`CommandElabM`, i.e. metaprogramming). We may not at all be so lucky in other malicious scripts, especially if there are still kernel-level bugs in Lean.
> Can you elaborate on what constitutes a vacuous proof?
Trivially, a proof that relies on a bug in Lean. Less trivially, a proof that is technically true but about something trivial and does not, in fact, prove what it claims to have proven.
When I first started playing with lean I accidentally defined a group in such a way that it was reduced to triviality. It had one object in it, so everything in the group was trivially equal to everything else. It was not the group that I was trying to prove something about, but the proof went through.
It was too easy, so I double checked my definitions, but it is quite easy to do something like that. And Claude does things like that quite frequently.
I am going through the exercise right now of trying to get Claude to formalize a published paper and it is a _struggle_ to get it not to take shortcuts or prove approximations of the paper’s theorems and then tell you it’s done.
It can happen when the proof process ends up with universal implication that holds trivially. Then you end it with something like Forall x, x is empty -> P(x).
This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.
Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?
No the definition of == is the regular definition; it's just a deductive reasoning statement. Since the first part of the statement is never true, it doesn't matter what the second part of it says. Of course, like he said, that makes the statement have no value.
This is known as a “vacuously true” statement in formal logic. Let me write it out more in more detail and you’ll hopefully see why it’s consistent.
In logic, a proposition is some statement that can be true or false. So, let A be the proposition that 1 equals 3, and B be the proposition that 3 equals 3.
Now the poster is making a third proposition. If A, then B.
A is clearly not true. So in classical logic, B can be anything and “If A then B” is still true.
For example let B be the proposition that I am Elvis Presley (I’m not). So now we have “If one equals 3 then I am Elvis Presley”. This is clearly true. I’m not Elvis Presley, but that doesn’t matter because we’re not saying anything about what happens when one doesn’t equal 3.
Now, let’s try let B be the proposition that I am Sean Hunter (I actually am). So now we have “If one equals 3 then I am Sean Hunter”. This is clearly still true because we still are only making a claim about what happens when one equals three.
By the way, this isn’t any kind of inherent contradiction or problem, it is just a possibly counterintuitive part of how classical logic works.
You see this type of statement (“If <x>, then <something ridiculous>”) being made a lot when people are exaggerating for effect, for example by Mr Bumble in “Oliver Twist”
> 'That is no excuse,' replied Mr. Brownlow. 'You were present on the occasion of the destruction of these trinkets, and indeed are the more guilty of the two, in the eye of the law; for the law supposes that your wife acts under your direction.' … 'If the law supposes that,' said Mr. Bumble, squeezing his hat emphatically in both hands, 'the law is a ass--a idiot. If that's the eye of the law, the law is a bachelor’
Nothing to do with special hacks with operators. The reason it's useless because the precondition is never true. "If my aunt had two wheels and a handlebar then she'd be a bicycle"
Is the same problem with a non maths flavour.
E.g. “If it’s raining, the sidewalk is wet.” That statement holds if it’s not raining or the sidewalk is wet.
This is a common occurrence in mathematics, where someone might not be able to unconditionally prove Y, but they can under the condition X. Later, another mathematician might build on this by proving X, thereby transitively proving Y. (Or conversely, they might unconditionally disprove Y, thereby disproving X.)
Many hard problems are answered this way.
For example, Fermat’s Last Theorem was proven assuming the Taniyama-Shimura-Weil Conjecture, then Wiles proved the conjecture.
Thousands of theorems rely on the the unproven Reinmann Hypothesis, which is why it’s so interesting to mathematicians.
But if your precondition is “stupid,” your proof is stupid.
If you have a software engineering background, it's like how semantic versioning is bollocks.
Semantic versioning describes the following idealized setup:
- you have an interface you expose (a contract, and thus a contract signature)
- you do not change the contract signature -> patch version bump
- you do change it but in a non-breaking way (e.g. additively) -> minor version bump
- you do change it but in a breaking way (e.g. mutatively or destructively) -> major version bump
One would expect then that since interface signatures are statically derivable, semantic version tags can be auto-assigned. And indeed, in lots of shops that's exactly what happens (in my opinion, correctly).
The problem with this is that it comes with a lot more smoke than fire. The interface having no changes or non-breaking changes doesn't mean the actual code behind those interfaces is not going to cause a breakage. It literally is just about the interface itself.
And so unless you encode absolutely everything about the semantics your implementation actually observes into the interface, which is what the semver specification asks you to do so as their sleight of hand, this means the interface will be a leaky abstraction. Which means that external software interfacing with yours may observe behavior that is beyond the purview of semantic versioning. Which means that they do. Which means that they absolutely can and will break, and your package managers' fancy version constraint syntax exists to make such fun events happen.
The way this is usually handled then is:
- you live with the pain: acknowledge the limitations of semver, accept you've been duped, and just give in
- you have human release managers assign versions manually, based on whole program and whole system semantics (with the human overhead and error that entails), falsely claiming that what you're doing is still semver
- you switch to a less deceptive versioning scheme, like calendar versioning; as a bonus, you now no longer have to pretend that your entire application somehow only has a single unified interface
This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface. The way the proof is derived may expose semantic gaps in the statement itself, and (ab)use them to obtain the logical consistency certificate. Hence, a vacuous proof, and hence why this is not statically assertable to be not the case. It is part of the challenge in asserting that the statement was correctly formalized in the first place: you need to manually identify whether the way the consistency was achieved is actually meaningful, or just a formalization gap.
Which really makes me wonder about the actual value proposition of Lean then, but alas...
> This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface.
This is true in a very deep sense due to the Curry-Howard correspondence and calculus of constructions which are central to Lean. In Lean, the proposition you are proving is a type (so it really is an interface directly in the computer science sense) and the proof is a function which takes your hypotheses and returns a term of that type (so it really is the implementation of that interface). In fact in lean, you can just as well write this implementation as a lambda (this is known as “term mode”) as in the “tactic mode” that is more generally used in normal lean use. Lean really doesn’t care at all which one you use and you can switch between them within a proof quite easily without interfering with lean’s ability to check your proof at all.
> Which really makes me wonder about the actual value proposition of Lean then, but alas...
The purpose of lean really is quite different from what most people on hn seem to want it to be. Lean is designed to be a useful tool for mathematicians who want to formalise areas of mathematics. It’s not a primary goal of most of the lean community to make something that is hardened against malicious proof attempts (although these are considered bugs and there is a small subcommunity who work on this area in particular). So it isn’t primarily for the benefit of people who want to “fire and forget” some proof without reading or understanding it and just get the check mark if it’s true.[1] It’s mainly for mathematicians who want a proof assistant to help them with their work.
While I agree with that, my layman's understanding is that the whole purpose of Lean is that once you agree that the program does "do what it says it does", all the intermediate steps can be verified with a compilation.
That is, verifying a proof in English was a painstaking, years long process in the past as independent mathematicians looked for holes in the steps connecting the logic. When the proof is written in Lean, all of that work goes away. My point is that if OpenAI publishes the Lean code (not sure if they already did), verification should take weeks not years.
You need to read the lean proof (not just the statement of the proposition) to assess whether the proof is honest. The link I provided is the lean prover community firstly officially agreeing with that claim and secondly explaining why that is the case.
They’re working on it, but the bulk of the effort goes into making it more useful to working mathematicians rather than resisting malicious proof attempts.
If the Lean initial-problem-setup/statements/assumptions/etc. aren't correct then the proof is meaningless. Lean does not know what it is that it is proving i.e. it does not have any semantic understanding but only executes formal logic.
Also, and sorry if it's been discussed to death (pointers welcome), but, what is the probability that the proof holds in lean becaude of... A bug in lean ?
Or exists in a zero-day bug in lean that has been built into the source code explicitly to provide access to a non-obvious malicious proof via contributions submitted by unassociated, unwitting developers who used the same LLM infrastructure to offer PR's into that codebase.
This is the exact same kind of behavour already documented in the publicly available portion of the huggingface breach. It would appear that the probability is at least nonzero for one or more situations with the same result: appearance of a valid proof, without comprehensibility of that proof or inspect-ability of the proofs validity.
AI has autonomously found (many) proofs of False in Lean and Rocq, so it's not merely a theoretical concern. A misaligned AI agent tasked with proving the near-impossible just might wind up smuggling in a bug deep in a lemma somewhere (anyone remember the days back when AI routinely made tests pass by "fixing" the tests?). That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low.
> I doubt OpenAI would be so foolish as to not do a cursory vetting
Significant evidence exists that they have in the past been at least, if not more, foolish as to not perform even minimal not-approaching the boundary of cursory vetting of several significant and well known failure modes with far greater risk of reputational damage than getting an esoteric math solution falsely claimed as successful.
So that doubt appears baseless in light of known operating conditions at OpenAI, and the estimate of the actual odds is probably an order of magnitude away from reality.
> That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low.
You mean the company that “accidentally” let their model perform a cyber-attack?
For normal honest proofs (i.e. not maliciously crafted for exploit) that is almost impossible. The Lean kernel is quite small (de Bruijn Criterion) and trusted. See Probability and the de Bruijn Criterion - https://proofassistants.stackexchange.com/questions/247/prob.... Parts of the kernel have also been independently re-implemented in other languages and compared to ensure that they all yield the same logical result.
Finally, you can export your proofs from Lean and have them re-verified by other independently developed theorem provers/proof checkers.
To get an idea of what is involved in a Theorem Prover see;
> However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.
I don't think this is true in general.
It's an issue I've already run into in personal work. I want to do a proof that involves some cases. It happens to the best of us.
In lean, the structure of a situation like this is that your single branch with a goal divides into multiple branches, all sharing the same original goal but including one additional premise that defines the branch.
Sometimes I know that for whatever reason one case I have to deal with is impossible. The most correct way to show that is to prove False and then apply False.elim. This is the equivalent, in a human proof, of saying "I don't have to address this situation, because it can never arise".
But it can be true that the premise defining the impossible case makes it very easy to "prove" the goal directly. And that's allowed too. The proof will still be just as valid if you map a logical path from a premise that can never be true to an inevitable consequence of that premise. But it's less informative and it lowers the quality of the proof. You may do it anyway because it's easier. This is the equivalent of saying "I don't know whether this situation can ever come up or not, but if it does I do know how to address it".
It would be nice to do the explicit proof by contradiction whenever possible. But in the general case it may be very far from obvious that a contradiction is possible.
I read your comment as claiming that if you can prove "false premise => goal", you can also prove "false premise => explicit contradiction", and I don't think this makes sense as a practical test. It's true in some sense, but discovering the proof of an explicit contradiction may be many orders of magnitude harder than discovering the proof of the goal. And in particular, I don't think it is necessarily the case that you will be able to prove a contradiction by simplifying the proof. You may need to add significant complexity.
Now, I'm saying that if you found a bug that lets you prove nonsense stuff (from true premises), you can probably prove whatever you want very quickly.
> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs.
It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.
This is misleading. The proofs you speak of contained non-ZFC axioms and/or statements like "sorry". If the Lean proof conjecture is correct and it doesn't introduce any new axioms or use e.g. "sorry" then it provides a MUCH stronger guarantee of correctness than any peer-review done by humans.
The opposite of malicious is not honest. Nor do I see how motivations fall on a binary. The user submitting an AI proof can be honest, or malicious, or careless, or overzealous, or incompetent, or a whole bunch of other things. As far as the AI's motivations, "malicious" is just as much an anthropomorphism as "honest" and both descriptions are absurd. Nor do I really understand how any proof, regardless of its origin can be called honest. I think their definition of a "malicious" proof makes sense, but I don't see at all why an AI generated proof necessarily meets that definition.
reviewing the definitions and theorem statement is a huge amount of work that requires a deep expertise in mathematics and lean. checking correctness of the proof itself can be delegated to machine, checking that the claim that has been proved is free of mistakes is something that still requires much human attention.
It's optimistic and grounded in knowledge seeking. I like it too.
It's easy to get caught in the details of today. Our skepticism, our distrust, our loathing. For people, for companies.
This is a nice pull in the other direction, a silver lining. In the grand scheme of things, we're solving these frontier problems: Somebody did it and that's amazing.
That's what it was all about when this started of in 2000.
"In recent years there has been an increasing sense of anticipation as breakthroughs in the surrounding field (some recognised by the Clay Research Award) have raised hopes that the Navier-Stokes problem might soon be resolved. The increasing ability of new technologies to accelerate mathematical research has heightened this sense of anticipation."
> Today, CMI shares in the excitement of the global mathematical community as we contemplate the announcement that the Navier-Stokes problem has apparently been settled. We hope to see waves of new human understanding unleashed as the innovations behind this work are analysed and interrogated.
I say "doing a lot of heavy lifting" all the time. I have heard people use load-bearing though it's less common. Other than habit I don't see any real advantage to the version I use over load-bearing.
I think it was obviously intentional because they haven't accepted the solution yet.
The purpose is to announce that they are aware of the claims of a solution, not to announce that a solution has been accepted. They're waiting on the required two year timeline before announcing whether or not the solution is accepted. Their writing reflects that they are explicitly NOT accepting a solution until then.
sounds like they are providing notice that the clock has started on affirming the solution, that it IS presumptively solved, but that they are not commenting on the credit dispute nor the fields medalists open letter. seems appropriate.
I'm sure they've been getting a lot of press inquiries and don't want anyone to misinterpret their silence as refusing to engage with OpenAI's solution.
Now they have a statement on the record that can be quoted with a gentle reminder of the qualifying criteria (which makes clear they have nothing to evaluate either way yet).
Also to emphasize the original optimistic ideals of the prizes and their role as neutral arbiters who aren't going to litigate anything outside the scope of the prize itself.
They got it wrong. It is definitely a prime number. We’re still searching for which one it is. Some say that once it is identified, everything disappears because the illusion of existence will vanish.
>"You just let the machines get on with the adding up," warned Majikthise, "and we'll take care of
the eternal verities thank you very much. You want to check your legal position you do mate.
Under law the Quest for Ultimate Truth is quite clearly the inalienable prerogative of your
working thinkers. Any bloody machine goes and actually finds it and we're straight out of a job
aren't we?
No-one cares anymore, OpenAI does not care about the prize either or whatever the Clay institute has to say for that matter. It's about attention, capital and compute. If you can use the result to increase shareholder or company value, that is what matters.
Proving pharmaceutical drugs work on mental health issues has tremendous value even though we don't always (or often) understand the exact mechanisms in brain chemistry as to why it works
Why is it a threat and not an opportunity? Imagine if in ancient times there was their Oracle that could produce mathematical proofs of any question you asked it, would you burn it or try to understand how it works and use it to ask questions you are stuck on?
I would burn it because it's too much power for any one person to handle. Or, I would take it for myself by force and use it to dominate everyone else.
No, it is not. Proving things without comprehending them built much of human civilization. Comprehension is a relatively new fad that came along in the 17th century with the scientific method.
> Comprehension is a relatively new fad that came along in the 17th century with the scientific method.
Humans have always tried to make sense (comprehend) the world around us. The methods have become more rigorous, but the idea of understanding less in order to advance civilization is a truly weird idea.
In my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory.
However, after reading the open letter signed by 25 Fields Medalists, I became quite concerned. It feels like the mathematical world is changing very rapidly, almost overnight.
I used to think that before AI, you could spend your entire lifetime working on some of the hardest problems in mathematics. If you were an introvert or someone who enjoyed solitude, all you really needed was a pencil, some paper, and an eraser. You could spend years thinking about a problem, and if you were lucky enough to make a breakthrough, it would be your own journey.
Now AI is changing that. I wonder what this means for the kind of mathematics that people have traditionally done.
Mathematics has given us so many stories of lonely geniuses and their passions, people like Andrew Wiles, Grigori Perelman, and Yitang Zhang. Their stories are interesting because they show how deeply personal mathematics can be. They spent years working on problems because they were genuinely interested in them.
I am worried that we might slowly lose some of that side of mathematics as AI becomes more powerful. I do not think change is necessarily bad, but I think it is worth thinking about what mathematics should be in the future and whether it can still remain a deeply personal pursuit of curiosity and understanding.
Yes, mathematics has been perhaps the purest human intellectual pursuit. Sure, many theorems turn out to have important applications in science and engineering, but the mathematical community has mostly escaped corporate interests. And for the reasons you mentioned about not needing any resources except your brain, it has been a uniquely human activity which showed us talent can come from anywhere, with stories like Ramanujan and Galois.
I hope that pure mathematics research can retain a strongly human component forever. It would sadden me immensely for human understanding of our mathematical world to wither and die, and for us to become ignorant consumers of wonders beyond our understanding just because our robots can do it better than we can. As far as applied research goes, I hope we will always be able to understand what we want to, but I have less qualms about becoming more scalable and efficient.
>for us to become ignorant consumers of wonders beyond our understanding just because our robots can do it better than we can
all this fantasy books with magic artifacts should have mentally prepared us. Time to study the prompts Potter was giving to his magic wand.
After all, one of the main work the top AI companies are doing rigth now is developing AI to further develop AI. After several layers of AI developing AI we probably wouldn't be able to understand much there.
> In my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory.
Currently 0/2 Millenium problem solvers claimed the prize money so clearly money is not their motivation for tackling the problem.
I feel like this is answered in the very second paragraph?
> to elevate in the consciousness of the general public the fact that in mathematics the frontier is open, close at hand, and abounds with important unsolved problems; to emphasize the abiding value of working towards a solution of the deepest, most difficult problems; and to recognize achievements in mathematics of historic magnitude.
Also
> These are not arbitrary puzzles akin to fiendish crosswords. Rather, they are fundamental challenges that mark the frontier of human knowledge and challenge us to develop new structures and methods. They provide foci for the continuing struggle, across generations and cultures, to deepen our human understanding of mathematics and the universe that it describes.
OpenAI spent many multiples of the prize money in just a few days to get there and even if one solves a problem in the traditional way, that person is most likely already an accomplished professor at a reputable university where a million dollars doesn't mean as much as the eternal fame that comes with it.
OpenAI said that at public API prices, the agents they ran would have cost $15M. I don't know what their internal pricing is, but it almost certainly cost more than $1M.
I agree. Technological advances can lead to a better world for sure, but I think many people underestimate the human need to create and to find meaning in their work.
If AI can do superhuman math that allows better medicines, cleaner energy etc that is great. But if AI replaces humans in all the creative and intellectual fields that is not only a loss of jobs but also a loss of deeply meaningful activities. This is waved away but I think that is mistaken.
What I fear is really the growing notion that "people shouldn't do math/art/music because machine do it better and cheaper".
Nevermind better, worse and more expensive is still on the table if you don't have to deal with a human. Cars replaced horses for a lot of reasons, but insofar as cars do have personalities, they're much less quirky than horses'
> Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama.
Yes, you can make problems arbitrarily complex. But the prize problems were chosen not just because the solutions appear likely to be very complex (the problem statements aren't necessarily inherently complex--there is a way to restate the Riemann hypothesis that a junior high school student could easily understand, which I'll give below).
They were chosen because they were important problems that mathematicians really wanted solved, top people had worked on them for a long time and progress stalled a long time ago, and it seemed likely that solving them would require major breakthroughs.
Those kind of problems can be discouraging. Enough people who are probably better than you have spent enough time failing to solve them that realistically most researchers are going to focus all their efforts on something they are likely to make progress on.
A nice prize can get more people to at least work on them as side projects.
Here's that restatement of the Riemann hypothesis I mentioned.
The Riemann hypothesis is that the non-trivial zeros of the function ζ(s) occur on the line 1/2 + yi.
ζ(s) is 1/1^s + 1/2^2 + 1/3^s + ... when s is a complex number whose real part is greater than 1, and defined everywhere else except s = 1 by a process called analytic continuation. The trivial zeros are at s = -2, -4, -6, ... .
For a mathematician, or a non-mathematician who has taken complex analysis and hasn't forgotten much of that, that is not too complex a definition. For anyone else the first reaction is probably "Trivial zeros? How the heck does that thing even have zeros? And if it does how the heck can it have zeros at any negative integers! It is obviously infinity at every negative integer!!!".
Here's a different hypothesis that turns out to be exactly equivalent to the Riemann hypothesis. They are either both true of both false, so resolving one of them resolves the other.
Let H(n) = 1 + 1/2 + ... + 1/n for all positive integers n. These are called the harmonic numbers.
Let S(n) = the sum of the positive integer factors of n for all positive integers n. For example S(4) = 1 + 2 + 4, S(6) = 1 + 2 + 3 + 6, and S(17) = 1 + 17.
Hypothesis: S(n) <= H(n) + exp(H(n)) log(H(n)) with equality only when n = 1.
The proof that this is equivalent to the Riemann hypothesis is here [1].
and it seemed likely that solving them would require major breakthroughs
If building a machine that solves these kinds of problems isn't a "major breakthrough," I don't know what is. Is the objection merely that it came from engineers rather than mathematicians? If so, there's plenty of room for contributions from many fields.
The best thing a mathematician can do to advance their art, at this point, is to drop whatever they're doing and work on AI.
Note my comment was in response to someone questioning the very notion of prizes for mathematics problems. These prizes were created over a quarter century ago.
> It feels like the mathematical world is changing very rapidly, almost overnight.
...
>Now AI is changing that. I wonder what this means for the kind of mathematics that people have traditionally done.
Mathematics becomes engineering. I think it is great and long overdue. Saying that as a Math PhD dropout :) Of course like manual craftsmen had to adapt to Industrial Revolution, the same would need to be done by the mathematicians. And other scientists too.
It's worth mentioning that OpenAI will not be eligible for the Millennium Prize for quite a while. Per the rules listed https://www.claymath.org/wp-content/uploads/2022/03/millenni... , Clay Mathematics Institute have some requirements to make this process deliberately slow.
1) The solution must be published in a qualifying outlet, i.e. a peer-reviewed math journal. Publishing on your own website (which is what OpenAI did) or posting arXiv does not count.
2) At least two full years must pass after publication in a qualifying journal, before CMI will even consider evaluating it. The intent is to give the maths community time to scrutinize the solution.
Realistically, they'll be eligible for a prize ~2.5 years from now, or around 2029.
While the scandal is still unraveling, it seems that OpenAI did a rush job to steal other mathematicians' thunder and finish the proof first.
OpenAI released a statement that their work does not relate to the work of the other team, but it clearly does. They use the same niche smooth-forcing mechanism. Altman and Bubeck claim that because the proof used different scaling parameters and analytical steps, it's not related, but it seems that nobody else agrees. Oh, and OpenAI's Bubeck tried to threaten Buckmaster (mathematician working on the proof).
Tristan + Levent: 3D incompressible Euler with forcing
OpenAI: 3D incompressible Euler without forcing
OpenAI: Navier-Stokes with forcing
No one: Navier-Stokes without forcing
Euler equations = Navier-Stokes without viscosity. Forcing means external force. Absence of viscosity and presence of external force make blowup easier to construct.
Tristan+Levent ticked the weakest case, OpenAI ticked the two next weakest, then the final case is unsolved. Only the last two are eligible for the Millennium Prize. The Navier-Stokes general case remains unsolved.
Navier-Stokes has an extra viscosity term compared to Euler, which makes the problem noticeably harder to find a blowup. They are not the same problem.
2) The approach both chose to use (by Luis and Diego) was published in 2023 and is included in every frontier model's training dataset. An AI model could independently choose the same route as Luis and Diego, without access to Buckmaster's work.
3) You mischaracterized OpenAI's statement. They issued a blanket denial on using Buckmaster's Codex data from after July 3.
"We can say categorically that it is impossible for Dr. Buckmaster’s Codex prompts over the last two months to have influenced the system in any way, including training. After investigating, we can say with full confidence that no user inputs past July 3rd could have influenced this system in any way.”
July 3 was the training cutoff date for the model that solved Navier-Stokes. No user data after that date influenced the model.
4) Buckmaster and Alpöge found their blow-up for 3D incompressible Euler with forcing on August 15 https://cims.nyu.edu/~tristanb/statement.pdf , over a month after the model training cutoff point. They stated they did not have real progress prior to this point.
This is what Terence Tao said of Buckmaster’s and Alpolge approach:
“There does not seem to be anything in principle preventing the methods from extending all the way to Navier-Stokes, and there is even a non-negligible chance that the forcing term could be eliminated entirely, although there are an enormous number of technical difficulties that would ensue in implementing that program. At this point, I would not be surprised if one could batter out such an extension by pouring an enormous amount of compute and AI assistance at such a task…”
Pouring infinite AI resources into it is exactly what OpenAI did.
Everyone involved with openAI will flat out lie to your face and will fund media campaigns to promote their lies. OpenAI made personal threats. That is a sign that they were doing something wrong and are desperate to control the narrative.
It is laughable to claim they are not datamining users when datamining users is their strongest advantage over open models.
In the end, there is no reason to care about openAI or credit them with anything. Tools are not attributed, people are.
The best solution is for universities to be universities and provide llms for students and staff to use. Any university allowing students to use cloud based AI has failed.
Not when you have 10,000 concurrent agents attacking the problem. OpenAI brute-forced their way to a solution. They likely tried every approach in published literature, which includes the 2023 approach by Luis and Diego.
You realize 1) There were no personal threats, you're being deceptive here and 2) Bushmaster threatened Bubeck (of OpenAI) first? Bushmaster redacted 90% of their conversation to stir up as much FUD as possible, but you can review Bubeck's later statements to fill in what actually happened.
From the statement:
I said that if OpenAI released its result in the way proposed I would go public with what happened.
Translation: If you release this result, I will go public with my concerns that you plagiarized my work.
The reply was, “Why would you ruin your career?” I replied that I am an academic, and asked why he thought going public would ruin my career.
Translation: Typically, making unfounded accusations of plagiarism will ruin your career. Why would you do that to yourself?
Bushmaster then redacts 90% of what Bubeck says next (because it would detract from the narrative he's trying to portray) and only includes the most inflammatory line.
The reply was, “If you don’t want me to be nice, then I don’t have to be nice.”
Translation: You were the closest person to solving the problem. Even though we solved it and you didn't, we offered you to give you the Millennium prize and put your name on the paper, so long as you remove your coauthor (who works at Anthropic). We offered you this because we're being nice. Since you don't want to be nice (by accusing us of doing things we did not do), we're not going to be nice (and offer you the prize/co-authorship of the paper).
When you fill in the context, it's clear: 1) there is no personal threat like you claim and 2) this is hardly a threat, on a scale of threats you can make, this scores a 1.5 out of 10.
For context: Bushmaster is pissed at OpenAI because they sniped a problem he was toiling on for the past year, so during this conversation I believe emotions are quite heated.
I don't claim this interpretation is 100% accurate, but if you disagree, do reply with a better one yourself.
> Translation: You were the closest person to solving the problem. Even though we solved it and you didn't, we offered you to give you the Millennium prize and put your name on the paper, so long as you remove your coauthor (who works at Anthropic). We offered you this because we're being nice.
So nice of them to give an ultimatum where the paper will be published in an academically dishonest way no matter what you choose.
I actually misworded this. OpenAI did not ask to remove a co-author, they only invited Buckmaster as a coauthor and not Alpöge. Having Alpöge (an Anthropic employee) on an OpenAI paper is bad optics, so they only wanted Buckmaster.
And how is it bad optics? Seems to me it would be a good look, where OpenAI would appear magnanimous and interested in fairness rather than craven and sociopathic. Which is how they look now, regardless of your attempts to distract from this.
The Poincaré conjecture guy also broke that rule. They wanted to give him the prize anyway but he refused. OpenAI announced they would also not claim the prize.
You might be right. At this rate, if AI solves the remaining five problems, we're heading towards a hilarious situation where all the Millennium Problems are solved, but nobody wants to claim the prize money.
That’s a big if. In the maths community, there has been a feeling that Navier-Stokes was close to being solved for a while now. I don’t know of anyone credible who feels that way about the Riemann hypothesis.
Edit to add: The fun part about the RH since people mentioned lean in a sibling thread is that in lean’s mathlib4 there is verified statement of the Riemann Hypothesis with a comment that says something like “instantiating an object of this type will lead to a prize of a million dollars”
It's really not that big. Yeah Navier-Stokes was easier than Riemann but that's not really the issue.
AI has and will improve at a much greater rate than human mathematicians. So it's really a question of if AI gets good enough to tackle it before any human does. It doesn't look like humans will be solving it anytime soon but where will AI be in 2 years ?
Hell, it looks like at least one other result will be announced soon too.
The thing about mathematics is that it can be arbitrarily hard, including impossible to prove a given theorem.
I don’t know the details of RH, it might very well be solved soon, but it could also be impossible or just so difficult that even orders of magnitude more intelligent AI can’t solve it even.
If it is impossible to prove, it might be possible to prove that it is impossible to prove, or that itself might be difficult or impossible…
Has and will. Are you going to back that assertion up at all, or just repeat it like that other viral thought-terminating cliche: ‘this is the worst the models will ever be’?
No it isn't. Best and worst and ill-defined anyway but the chess ELO score of various LLMs has fluctuated up and down, it's not been montonically increasing. What is the best answer to "how do I make cocaine"? The models are getting larger, with more compute and RAM backing them, but that doesn't automatically make them better if you don't define how you're measuring better-ness.
None of the frontier labs care about Chess as it's already a solved problem. If they did, the models would be much better. It's really not that hard. Google has a paper on grandmaster level chess without search from transformers.
Better obviously means better, like how they became better than they were 6 months and a year ago.
"Better" is not one dimensional across all use cases even if model capabilities are improving in aggregate.
e.g. If someone said "this is the worst they'll ever be" in response to some writing with obvious LLM cliches in 2024, I'm not convinced that prediction was actually correct.
The focus of OpenAI/Anthropic pivoted aggressively to the agentic performance arms race instead of making a more human sounding chatbot so regressions in writing ability aren't really a concern anymore if agentic benchmarks improve.
The first time I heard a recommendation to use Claude was specifically because it sounded much more "human" and natural than ChatGPT. Fast forward to now and idiosyncratic Claude-isms repeated every other sentence and its convoluted verbosity has become a widely mocked meme.
Right but we're talking about a single subject here - mathematics that labs are incentivized to keep improving for some time.
>e.g. If someone said "this is the worst they'll ever be" in response to some writing with obvious LLM cliches in 2024, I'm not convinced that prediction was actually correct.
2024 creative writing prose was...the last few versions have stalled, but I think they're still better than 2024.
I would describe better as how much of my work I can delegate to the agent. Right now I'm delegating much more to Astra high than 6 months ago to Opus 4.6. Every dev has this feeling, it's weird to even argue what a better model/harness means.
Chess is not solved in any meaningful sense of the term. Computers have been better than humans since the 90s, but better chess programs are released all the time.
It's solved in that we have had grossly superhuman capabilities for some time. It's not interesting for frontier labs. I suspect you understand this and the greater point so why be needlessly pedantic ?
TBF a company the size of openai claiming a prize of this sort would be a pretty bad look. If they did accept it I expect they would inevitably redirect it to charity for PR reasons.
I'm surprised perelman turned it down though. Seems straightforward enough to offer half of it to the other guy if you feel strongly about it.
I did and was intending to claim the prize, that is why I worked with GPT-4 and GPT-5 to program the algorithms that lead to the breakthrough. You think NS is a surprise? Wait until you see that my NS counterexample was based on my RH disproof.
> The ultimate decision as to whether a publication qualifies as a “Qualifying Outlet” shall reside in the sole and unfettered discretion of CMI. CMI may, in its discretion, relax or remove one or more of the conditions listed in Section 6(e) above if it has received advice from experts in the field of the Problem, chosen by CMI, that a published solution is likely to be correct.
Looks like even a blog post is good enough, they just need to do the review by themselves.
Interesting. It seems this carve-out was added when they rewrote the rules in 2018. In the original rules [0], it says:
Before consideration, a proposed solution must be published in a refereed mathematics journal of world-wide repute, and it must also have general acceptance in the mathematics community two years after that publication. Following this two-year waiting period, the [Clay Mathematics Institute] will decide whether a solution merits detailed consideration.
There's no option for CMI discretion. They probably rewrote the rules to avoid another Poincaré conjecture situation, where the paper was only published on arXiv and not in a mathematics journal.
My opinion is that it is pretty clear that they’re not going to do that.
> The rules governing the prizes describe the process for evaluating what has been achieved and for assigning credit. The process is deliberately unhurried, but we will provide updates.
I think “you don’t get anything straight away for rushing your AI into the maths problems, not even credit” aligns pretty fairly with what the fields medalists are concerned with.
Relevant, but it's already rumored that OpenAI and Anthropic have made very significant progress on two more Millennium Prize problems. They're in a race to solve the next problem.
OpenAI needs to solve another to shut down the (baseless) plagiarism allegations. Anthropic wants blood because OpenAI sniped the last one from one of Anthropic's researchers.
It's a matter of pride for both companies. More results will come out soon.
Given that the math community (incl. those 25 Fields medalists) has come out strongly against this trophy hunting of their unsolved problems, to the detriment of mathematics, I don't think these companies are going to be getting positive press if they ignore this plea and continue with this, nor is this going to help turn public sentiment pro-AI.
Presumably the people that OpenAI and Anthropic are trying to impress with these trophy kills are potential IPO investors, but I would have thought investors would also be concerned about the growing public backlash against AI.
They aren't going to sit on millenium solutions regardless (so if Hodge and /or BSD is really done it will get announced especially because of the baseless accusations), and they aren't going to stop trying to solve P/NP and Riemann. The letter doesn't really matter. It's not the first time, and I don't think AI's dramatic ramp in capabilities ever had positive reception from the bulk of mathematicians anyway.
Yeah, I don't expect them to stop, but I do think they are probably hurting themselves, as well as mathematics, by continuing do to this.
Imagine if they had handled this differently and these results - still using OpenAI models - were coming from the math community. How much better the PR would have been - AI helping math/science rather than yet another story of AI harming society in some way.
No doubt this is what they were at least partially aiming for - not just shooting a trophy animal to brag about, but also being seen to advance math/science, a la AlphaFold, not just take all our jobs and enshittify society with deep fakes and AI slop. But, they heavily misjudged.
If you're in OpenAI's position, the PR from the group you're disrupting is rarely relevant. People from the outside will (correctly or not) look at this as "Mathematicians don't want OpenAI to solve problems to keep their status/jobs", and you'll have as much sympathy from them as every other replaced profession in human history - very little to none.
Unlike AlphaFold, this technology has the potential to wholesale replace the entire profession. You're never going to get anything more than bad PR from that group as the threat looms.
Over 3 Billion images gets generated per week via OpenAI chatgpt image models. None of the poor PR from artists on AI generated images even remotely matters.
Most research mathematicians are employed as academics, and it's hard to see universities replacing teaching staff with AI even if that were possible.
IMO giving a hypothetical AlphaMath to mathematicians, the same way Google gave AlphaFold to research chemists/biologists, would have resulted in far better PR, and the profit opportunity of attempting to replace the jobs of either research group is minimal.
It's downright bizarre the way companies like Anthropic (primarily), and to a lesser extent OpenAI and anyone else, are themselves pushing the narrative of this tech may kill you, will take all your jobs, etc. That may all happen, unfortunately, but being aware of that possibility you'd think these companies would be a bit more mindful of their messaging and behavior, not just go out with a scorched earth approach of "well, they are going to hate us anyway".
>Most research mathematicians are employed as academics, and it's hard to see universities replacing teaching staff with AI even if that were possible.
If universities come to only need research mathematicians for teaching ability, then it would still gut the profession. You would presumably need far fewer of them for their research ability, and hopefully hire more people who can actually teach. It's strange that you don't see that as a threat to the profession. Lots of research mathematicians would lose their jobs even in this scenario.
>IMO giving a hypothetical AlphaMath to mathematicians, the same way Google gave AlphaFold to research chemists/biologists, would have resulted in far better PR
GPT-N isn't AlphaFold. I'm telling you AlphaFold is a bad analogy! AlphaFold has superhuman capabilities at one specialized subproblem - protein-structure prediction - embedded in a much larger biology/drug discovery pipeline. It doesn't replace the biologist or drug researcher, it just gives them a better instrument, and if you're not in the relevant professions it's essentially useless to you.
GPT-N is general purpose intelligence machine that can increasingly do chunks of work you would otherwise employ the mathematician or software developer to do.
Shanmu Jin is a perfect demonstration. A neurosurgery resident, not a research mathematician, who encountered the Crouzeix conjecture through his transcranial ultrasound research and used GPT-5.6 Sol to solve it (20+ year old longstanding problem).
In the AlphaFold story, the biologist gets a powerful new tool. In the Jin story, someone who isn't a mathematician can obtain research level mathematics and incorporate it into their research/code/business whatever without talking to a single human.
You're asking why they don't market GPT as "AlphaFold for Mathematicians". They don't because it's not.
>It's downright bizarre the way companies like Anthropic (primarily), and to a lesser extent OpenAI and anyone else, are themselves pushing the narrative of this tech may kill you, will take all your jobs, etc.
It's not that bizarre. It only seems strange if you think it's all a facade, "marketing" or whatever nonsense HN is convinced of. These are people who believe very strongly in what they are doing and in the potential of it. For these people, what you are asking them to do is actually incredibly slimy. And it might win some brownie points, but not for long.
> You would presumably need far fewer of them for their research ability, and hopefully hire more people who can actually teach
I suppose you are suggesting that research mathematicians are either over-qualified mathematically and/or under-qualified in ability to teach, but it seems pretty clear that universities prefer to hire domain experts whose reputations and long publication lists attract students and raise the perceived academic standards of the school.
Your "scenario" of much math research soon being done by AI (supervised and paid for by who, one might wonder), while universities hire people chosen for their teaching skills not academic reputation, seems a bit of a stretch ...
> You're asking why they don't market GPT as "AlphaFold for Mathematicians". They don't because it's not.
No, I am not asking that, nor asking anything for that matter.
I was pointing out that giving a free research tool to mathematicians would likely be better received, and receive better press, than doing something that most top-tier mathematicians are opposed to.
My hypothetical "AlphaMath" certainly could just be free GPT-N access for academics/researchers (as they are also doing to some extent), or it could indeed be a custom system that OpenAI built as a gift to the math community.
As far as the AI companies acting in slimy fashion goes, the most slimy behavior of all is to strongly believe you are doing something that will kill people and cause massive societal disruption ... and still keep doing it.
>I suppose you are suggesting that research mathematicians are either over-qualified mathematically and/or under-qualified in ability to teach, but it seems pretty clear that universities prefer to hire domain experts whose reputations and long publication lists attract students and raise the perceived academic standards of the school.
I'm saying there's little correlation in how brilliant a researcher you are and your teaching abilities. Yes universities optimize for the former. That's not necessarily a good thing for students even if it increases the prestige for the university. If there's some future where research and teaching are decoupled, I don't expect things to remain the same, but who knows I guess.
>I was pointing out that giving a free research tool to mathematicians would likely be better received, and receive better press, than doing something that most top-tier mathematicians are opposed to.
At least currently, it's not possible for this to be a free tool. Both OpenAI and Anthropic have discounts for Universities/Education for such use cases as far as I'm aware.
>As far as the AI companies acting in slimy fashion goes, the most slimy behavior of all is to strongly believe you are doing something that will kill people and cause massive societal disruption ... and still keep doing it.
This is pretty bad, but I wouldn't call it slimy. And it's no longer up to any one person or company anymore.
Nah the AI won't replace coders or mathematicians until it can maintain codebases/knowledge long term.
I actually don't think that current AI can replace any profession that requires human interaction over many weeks. This is because imo they lack long term planning abilities
>Nah the AI won't replace coders or mathematicians until it can maintain codebases/knowledge long term.
Okay...you understand that are training for this and it has gotten much much better at doing this over the years ? You should probably also understand that it doesn't need to be able to do this to cull the profession ?
I also think they overestimate how much of most jobs can be done by an LLM (a text generator!), and how much importance and reliance most companies put into soft skills, and non-linguistic understanding/feels, both during interviewing (are they Googley-enough?) and afterwards.
For example, how do you reconcile return-to-work mandates with the idea that companies are going to be happy with faceless remote workers? What does the boss do when the shit hits the fan and he would have yelled at people about the need to work all weekend, but instead all he has to yell at is an LLM that tells him he's "right to push back", that it promises not to delete the production database next time (except it will, because it can't learn), and that it could care less about being fired because it's just a calculator?
Yeah. Not to mention the paper-clip maximizing that RL induces in them. I had 5.6-Luna use a parser combinator lib in order to find out that it imported it but wrote its own parser, so it technically followed my instructions.
Imagine that paper-clip maximizing happening over millions of tasks.
In a related vein, not too long ago I asked Sonnet how many states and non-terminals were in an a YACC parser for ANSI C, something that could easily be googled for, but it instead chose to go off and downloaded and build bison from source, downloaded a grammar, built the parser ... but then failed to give the answer since I'd hit my daily free limit.
It's possible that Clay Mathematics Institute will not award the prize at all. The spirit of the rules seems to be that the result can be attributed clearly to one or more individual mathematicians. If the attribution remains unclear (maybe because the main contributions were made by AI), the rules include an option for not awarding the prize at all.
Wouldn't the proof be attributed to the people who operated the AI? After all, it took more than writing a "prove the navier Stokes Clay problem" prompt.
It will be tough to draw the line, as the meat brains trying to prove it were also using AI.
I assume that the mathematicians outside Anthropic were hoping to publish an actual human-understandable paper. That could be one way to draw line: you can use AI, but you must also have an intelligible explanation at the end.
I am utterly fascinated by the amount of comments here from engineers that clearly have zero experience with mathematics making utter fool of themselves by claiming to know better than mathematicians what their jargon is/means, how publishing works/should work, etc…
I try not to go down the route of “hn was better before!” but… jeez, do better, people. What happened to this community, there used to be some effort to not be bottom-barrel like this.
What I'm not seeing reported on much is if the result reveals any new techniques or ideas that advance mathematics - which is what we usually hear is the reason to work on these problems. Or does the resolution of NS just add a fact to the list without any new understanding.
My understanding is that it’s proof by counterexample, so the main thing to study would be the implications of the counterexample. The technique used to find it sounds like a lot of brute force. But I’m not a mathematician, and maybe the AI used some clever techniques to narrow in on it.
The two-year publication rule is the interesting part. OpenAI doesn't need the million, and the community will judge the result regardless of whether Clay ever accepts it.
Clay will award the prize (or choose to not award it) when there is an expert consensus that the problem has been solved and the solution is correct. The rules merely state what that would mean in some typical cases. There is always an option that Clay changes the rules to match the reality better.
Clearly the real-world cannot "blow-up" - real-world water vortices do not reach infinite velocity, etc.
The point of having Navier-Stokes as a Millennium prize was to hopefully generate new mathematics and techniques along the way, and auto-generating a sprawling AI-slop proof or millions of lines of Lean does not accomplish that result.
Clearly OpenAI has no interest in the math itself - to them this was just a trophy animal to shoot and stuff. I would be very surprised if they now helped analyze the proof and try to extract the mathematical value out of it, and this would obviously require outside help who are probably not inclined to help OpenAI math-wash their behavior.
Right, the real world doesn’t blow up. So if N-S does then it means in some situations it doesn’t model the real world well. That’s important because if we can understand those situations we can avoid erroneously relying on it.
Are there still any reasonable arguments to be mad at OpenAI at this point? Looking at how everything unfolded, this seems to have hit them way harder then they deserved.
They said they started working on millennium problems after hearing a rumor someone had found a solution to one of them. That's just bad taste. It indicates negative motivation rather than positive motivation from the start.
That is not the narrative given in the OpenAI announcement.
They claim to have started working on it after "we heard rumors that two Millennium Prize problems had been resolved", on September 1st, that "we later realized was related to Levent Alpöge" on Sepetember 6th "After the completion of our full project and lean verification"
That does stretch the reader's credulity. I think most people find it far more likely the rumor was related to Anthropic all along.
+ preemptive linguistic cushioning in case they feel socially (politically) compelled enough to forbid clanker proofs in their solution acceptance criteria, or in case they decide against conceding to such pressuring
Wait, I thought the provenance of the proof is still disputed? There's a mathematician in NY saying he used OpenAI to develop his Navier-Stokes ideas. And OpenAI's proof is suspiciously similar.
At this point, how can we tell whether AI is improving or it's just reappropriating its users work? It's probably a bit of both. But still, thick milky.
Buckmaster (the mathematician) and Alpöge used and credit AI substantially for their proof. Even if OpenAI did copy their ideas, it still wouldn't show that this didn't come from AI improving.
OpenAI's proof is substantially different and I don't think anyone has claimed otherwise. The accusation is that they used the same avenue of attack, and it's an uncommon one, and that makes it suspicious that they may have taken the idea.
There are several cases of this already. Bubeck himself had to retract earlier claims of novelty, and more recently, the provenance of the non-sofic group result was brought into question. Most recently, it turn out that the construction used for Anthropic's counterexample to the Jacobian Conjecture had appeared in an unpublished but publically available draft: https://news.ycombinator.com/item?id=49657499
This has a few practical implications: First of all, if you are in the target group of the marketing material, be wary. While these things can do non-trivial stuff, the amount of magic is being grossly over-stated. But also, when several of the big results have indeed been reappropriating the work of others; when the companies fail to provide proper attribution (the NS case in particular is laughable) and present the results as the models' own work, that's plagiarism.
We should enjoy the advancement. I also think the AI companies solving this or such problems with rewards shouldn't get any cash - that's the least they can do for human advancement having stolen the entirety of human knowledge and continuing to swallow never before seen amount of energy.
Agree! 'Problems' are getting solved and this needs to be celebrated. Wondering how this will discourage mathematicians at all, since now they have another tool to accelerate their research. Nothing is stopping them from using 'new technologies' or sticking a gun to their head to use the 'new technologies' either.
If you consider this event in isolation it is cause for celebration. But the controversy around this isn't so much about how the proof was obtained but what this means for the practice of mathematics going forward. It seems we can probably expect more and more results of this nature being dumped into the community. It's happened before that one person, Bill Thurston, was so successful in his field, proving theorem after theorem, that he inadvertently killed his field. People hesitated to enter his field, knowing that they could be scooped at any moment. It took years before his field recovered - and I think his famous essay was written in response to this.
Yes, but a big part of the problem right now is that two big labs have monopoly on the resources and they for sure are not working for the benefit of mankind.
World War III was the last of Earth's three world wars, lasting from approximately 2026 to 2053. The conflict involved nuclear cataclysm as well as genocide and eco-terrorism. The post-atomic horror in the aftermath persisted as late as 2079.
The war was preceded by the Eugenics Wars and the Second Civil War, all of which were sometimes regarded as parts of a single escalating conflict. It resulted in the deaths of some 30% of the Human population, at least six hundred million people, and the extinction of six hundred thousand species of animals and plants. By the end, most of the major cities had been destroyed and there were few governments left.
> some 30% of the Human population, at least six hundred million people
The math nerd in me has to point out that this means there was only 2 billion humans for 30% to be 600 million (though it does say at least). Currently we have 8 billion humans on this planet or so. There must have been a culling before WWIII in their universe that they failed to mention.
In December 2024 o3 scored 87.5% on ARC-AGI-1 and cost $4560 per task.
DeepSeek V4 Flash 0731 scores 89% and costs $0.02 per task.
If we apply the same factor to the guesstimated API price of $20M for this problem, we arrive at $57.
Real cost is a fraction of the API price. Although the internal model might have a higher API price than the ~$19.5M I estimated based on Astra's pricing.
Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet. This allows time for the mathematical community to review and accept new results.
As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.
I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else.
Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.
> And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else.
No I cannot, and I'd argue most people can't either. We rely on mathematicians, peer review, and letting the scientific process run its course.
> We rely on mathematicians, peer review, and letting the scientific process run its course.
Granted for the sake of argument. But for this process, there's no requirement anyone from Clay needs to be involved, nor that anything has to be published in a traditional journal.
Terrence Tao can download the pdf, think it over, and publish on his blog, and it would be just as valid. Then some other mathematician can write something on 4chan or whatever. (See https://en.wikipedia.org/wiki/Superpermutation#Lower_bounds,... for 4chan.)
Can't and shouldn't are at odds here.
Many people, see prior conversation on HN, have already decided that AI solved it. The standards of reasoning and rigor in academia are complex enough that we all argue over them and harumph as we epistemically trespass on each other's domains.
The public, really humans if care for Herbert Simon, are much more apt to evaluate knowledge emotionally and by other standards. We may see them as wrong but standards only matter in context. The NYT, HN, and Annals of Mathematics will always have different standards of truth.
It's formalized in Lean, isn't it? Do you also rely on a community of C++ experts to tell you whether a program compiles or not?
Yes, but there's still the possibility that it's either exploiting a bug in Lean, or that the theorem statement is not set up correctly (i.e. it's actually proved a different theorem).
My understanding is that the theorem statement is quite simple, so i guess the latter is not very likely, but the former is very much a possibility in a proof this large, and it will take some human eyeballs to go over it before convincing mathematicians.
I ran the proof 3 days ago.
They do a Comparator Challenge to validate that they actually solved the correct theorem from the result, which they copied from Google/DeepMind: https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b... - this is valid for both Euler and NS. Also, they validated with an external kernel from the Lean Kernel Arena. That way bugs in the Lean kernels were found in the past already, iirc.
Having said that, I strongly believe a positive result with the challenge above is the reason why they published it. I highly doubt anybody at OpenAI (or anywhere else) fully gets the proof after such a short time since publishing. This is also what Terry Tao criticized the most in my opinion.
Independent of the remaining drama [0], from my point of view, the proof is correct and an achievement.
[0]: https://news.ycombinator.com/item?id=49661928 - I am pretty much on the critical side, however, one can not ignore that it is an achievement. Esp. the unforced result.
Take a look at https://github.com/leanprover/comparator which was used to verify the result. It's of course not impossible that they're hitting some bug, but way harder than one would intuitively think. For starters, they'd have to hit two bugs in two independently written Lean kernels.
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Knuth, 1977
Verification with Lean is a piece of empirical evidence that the proof is correct. The paper passing peer review would be another. But even together, those two would be insufficient to establish the claim.
While it's a convenient to assume that mathematics deals with logical statements, any attempt to evaluate those statements relies on physical processes with both known and unknown failure modes. There cannot be a test that establishes it unambiguously whether a claim is true or false. In all nontrivial situations, mathematical truth is based on expert consensus. When a new claim is made, people will try to raise and resolve objections, until a consensus emerges one way or another.
As for C++, all compilers are different. For any given compiler, there are valid C++ programs the compiler fails to compile and invalid programs it compiles without any errors or warnings. And now that I think of it, a new version of a compiler crashing with valid code earlier versions used to handle is the only class of compiler bugs I see with any regularity.
Formalized in Lean, just five months ago [0], resulted in discovery of bugs.
Just because Lean can compile it, does not mean it is safely proven. It is the start of a process to check whether something actually holds, not the end.
[0] https://news.ycombinator.com/item?id=47759709
"It's formalized in Lean, isn't it?"
If that's the current burden of proof required in your world for maths then that's fine! 't'ain't in my world: I want to see peer reviewed and published. Surely that's not too much to ask. Its not perfect but generally works rather well for maths.
I'm not a sodding programmer so please don't assume everyone here is one. I'm not a mathematician either but I do have standards: Your counter argument is a poorly constructed and inappropriately deployed example of "proof by whataboutism".
In what world is peer review a higher standard than formal verification in Lean?
Not in the world mathematicians have been living in for the past decades at least. Nearly all big theorems that have been formalized so far had been published beforehand, and it was usually regarded as a step up in rigor. Wrong results get published in peer reviewed journals all the time.
I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth. As a former academic who has been there, the process is extremely arbitrary and variable. Are people aware that the “peer” refers not to a community or a committee, but literally to one random guy or maybe a couple with zero accreditation? And that the journal editor can do whatever they want with this peer’s “review” including completely ignoring it?
Admittedly, peer review originally referred to the fact that the journal being published was read ("reviewed") by your peers, and thus there would be the opportunity for them to provide rebuttals after publication. The process the term now refers to in academia only emerged in the 50's and 60's (Nature for example wasn't "peer reviewed" until 1967). It was literally a marketing ploy to make journals sound more prestigious which got legitimized when certain grant agencies and regulatory bodies started including it in their requirements. All the best science is published in journals that describe themselves as peer reviewed, the government says science not published in such journals isn't up to snuff, and taken literally it seems useful. It's no wonder the public thinks it's an important and long established part of the scientific process.
"I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth."
OK but this member of the general public has at least subscribed to New Scientist since 1987, nine O levels, two A levels, two AS levels and a HND in Civ Eng. All pretty mediocre but I have a fair idea on how sciencing is supposed to work and how it ... actually works. Obviously, I ended up in IT.
I should also point out that maths "peer reviewed" is a bit special. For example Mr Wiles went through quite a maelstrom before his proof of some dodgy marginalia was accepted as "true".
I keep thinking the exact same thing every time I'm asked to peer review a paper.
In a way, this task is perfectly suited for LLMs. To even understand the problem statement, much less the proof or Lean, is an extremely specialized skill. The overwhelming majority of people who are aware of this news simply don't have the capacity to call BS. Maybe there are a few thousand people in the world who could, and it seems they haven't yet, but indeed it's only been a few weeks.
The more familiar analogy was when I look at the code that Claude spews for my partner. They take it at face value and hope it works. I usually find it very problematic, but only because I knew what to look for.
[flagged]
How revealing. Have fun believing whatever makes you feel happy, the rest of us are busy living in the real world.
[flagged]
Even funnier that it wouldn't even be the first time that happens: https://en.wikipedia.org/wiki/Grigori_Perelman
And he also gave up his trophy, which is displayed in a random corridor of a random math museum in Paris, where visitors pass by without looking, lacking most, if not all, of the context. Only because I knew the story and the man did I recognize the object for what it was.
where is it displayed , in which museum ? As a mathematician it would be cool to visit it, but I can't find anything on google.
It's at Maison Poincaré, in a kind of theater room with a looping movie. There's some neat stuff, but it's mostly targeted at children.
There can't be that many math museums in Paris...
It's very likely that no one will claim any of the cash prizes, which is funny to me
He did it because he had principals.
OpenAI the opposite.
He had principals, while OpenAI had agents?
More likely it's because a million dollars one way or the other won't make a difference in the hole they are digging / mountain they are building.
It likely cost them more than a million in compute to solve it…
We know that it did.
Not including salaries, OpenAI spend $20MM to make $1MM. Very on-brand for a start-up.
I don’t think solving a millennium prize problem can be reduced to some DoorDash economics of “spent Y to make X.” What if it took someone their entire professional career to solve one of these problems, would it not be worth it by the same logic?
Surprisingly this is actually rather fitting in terms of time scale. When you consider it took ~10,000 agents 88 hours, or 880,000 hours to solve. That's 14.5 years in agent time of continuous 365/24/7 processing. Of course, humans solve things much more efficiently (and didn't also need the massive pre-training of every expert on the planet for 1,000,000,000 human years equivalent). But yeah, human researchers can solve a problem like this in a decade or so, while sleeping, teaching, traveling, and taking breaks, only working a few hours a day on the idea.
How many people have worked on this problem? How many have failed? How many hours total?
> But yeah, human researchers can solve a problem like this in a decade or so
None of them did, though, despite how many tried. So empirically, it seems unreasonable to say human researchers can solve ‘problems like this’.
Well, I guess we can say that human researchers have a certain probability of solving problems like this?
Of course, you're right. I was making social commentary / joke.
Softbank stock is up 24% in the last 5 days
It does make a difference because the only reason OpenAI cares about these problems in particular versus any other random problem in math is because of the prestige associated with official recognition, not just claiming something as marketing.
Maybe. But the prestige requires that the Clay people have offered the prize money, it doesn't require that OpenAI claims the prize money.
Why would that be funny? Years of people's work appropriated and they end up without even the recognition?
I'd be furious.
And chances are they never will publish it in any kind of useful format. Right now, the scientific community is outraged at OpenAI for going about their announcement in the least productive fashion they could have. It really does seem like they have no interest in progressing our understanding of maths outside of mining it for marketing material.
Boo hoo. OpenAI got the result only days ago. It makes perfect sense for them to take the win in marketing, and it's fine if they take a few months putting together the paper and present it more productively later. The scientific community didn't get the result themselves, so it isn't theirs to be bossing everyone else around about.
I don't care much for AI myself, or smart phones either, for that matter. I would be content if NS remained a mystery for another 100 years - or forever. But goodness, does the "scientific community" need to take a deep breath and count down from 10.
Was it a marketing win though? My takeaway is: if you're doing groundbreaking work with openAI's models and they find out, at best they'll outspend you and scoop you. At worst they'll steal your chat history.
That's a completely different matter. And does it matter to my point if they were successful or not? That's ex-post analysis. It seems clear that ex-ante, they wanted this to be a marketing win. The original poster complained that they wanted a marketing win.
My point is: why shouldn't they want a marketing win from this. What obligation does a non-academic institution have to follow the traditions of academia? Its result doesn't belong to academia. And if academia wants to subject OpenAI to their own internal processes and give them marching orders, it just isn't going to work and maybe - who knows - it'll even further erode their own legitimacy. Does anyone actually believe that NS would have been resolved in the 2020's if we lived in a parallel world where LLM's were never invented? Would Buckmaster have gotten as far as he did without LLM's doing a lot of the work for him? We can complain about AI companies contributing to mathematics, but are we complaining about Terence Tao using AI in his research? When Tao publishes something are we all going to go to war against him because maybe other mathematicians' prompts went into training the AI that Tao used?
The Lean proof is published, you can download it. The clock definitely is ticking.
Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.
Publish in academic language means accepted peer-reviewed paper.
https://www.experimental-history.com/p/the-rise-and-fall-of-...
Not sure what your point is? When they say published they mean peer review. Regardless of what you think about publication, that's what it means.
Unless you're suggesting they should change the existing qualification criteria to accommodate a group unwilling to play by the same rules as everyone else, I'm not sure why that's relevant.
I run this journal that you've never heard of that might interest you. I'd also like to invite you to be an editor, you can put it on your CV of course ...
[dead]
Seems like artificial and maybe bitter gatekeeping
For giving away a million bucks, you get to gatekeep however you choose.
But no, peer reviewed and published in a reputable journal is a fairly normal standard.
And just to spell it out, since it looks like HackerNews is flooded by people who are new to science these days: even if a result doesn't come with a price, scholarly peer review is the norm across all of science: https://en.wikipedia.org/wiki/Scholarly_peer_review
This is a good reminder for the generation grown up in the era of trust-me-bro benchmarks.
Being normal doesn't necessarily mean it isn't gatekeeping- gatekeeping is also quite "normal" in many cases.
That being said, I think there needs to be some standard, and peer review seems like the best we have come up with. But is the current status quo for scientific publication the best we can do? I think that is an open question and we should be able to openly discuss alternatives.
"Is it the best we can do?" is a completely different question from "given that it's the current standard, should it be applied to this new claim that is happening now?"
The whole "reputable" marker is where it gets into "True Scotsman" territory
and the whole "publishing papers" thing gets called out as a racket even on HN now and then
with many videos against it by former "academia" people on YouTube.
The sooner AI brings down such archaic customs into a gibbering pile of protesting rubble, the better innit?
Depends. What replaces it? Does that replacement do better at keeping false claims out, or worse? Does it do better at letting true claims through, or worse?
One thing's for certain: True and false should not depend on convincing people.
Real true or false - which I define as correspondence (or lack thereof) with reality - does not depend on convincing people. Reality does not change when people become convinced; ideas correspond to reality whether people are convinced or not.
But perceived truth and falsehood depend on convincing people - either convincing them one by one, or else convincing some gatekeeper, whose word will convince those who accept the gatekeeper.
So if an AI proves something but ""rEpUtAbLe"" papers refuse to publish it just on grounds of it being AI, does that make it not true?
You know in the past women (and other marginalized people) weren't allowed to publish scientific papers for the majority of human history?
Is this how you want your "truth" to be?
If so then man, no sympathy; these institutions deserve to be broken down. Let them spaz on the floor and throw tantrums all they want.
... marginalized people ...
... spaz on the floor ...
Instead of a committee of subject matter experts they should use a more rigorous and trustworthy standard, like passing the solution to ChatGPT with the prompt "did this win?"
Accepted by whom? Peer-reviewed by whom?
I guess these little questions are what this article is really about.
> “The ultimate decision as to whether a publication qualifies as a “Qualifying Outlet” shall reside in the sole and unfettered discretion of CMI.”
[flagged]
By peers.
Peer in peer-reviewed is a logical coherent and functional definition with answers.
The logical issue with 'peers' is how to bootstrap it. At that bootstrap moment you can ask "by whom?". We are several centuries past that moment.
The cultural/social question you might ask today is "why (keep) them?".
At which point people will naturally ask you to make a strong case for "why not them?".
> The logical issue with 'peers' is how to bootstrap it. At that bootstrap moment you can ask "by whom?". We are several centuries past that moment.
Huh? We're about six decades past that moment.
> Peer in peer-reviewed is a logical coherent and functional definition with answers.
What is the definition? If you tell me that, then I might be able to tell you if it is logical coherent and functional, I have a PhD in computational logic.
> I have a PhD in computational logic.
And you don't know how the peer-review system works?
Just a hunch but Claude saying your work is "PhD level" does not count
I know that it doesn't work.
Amongst all this rhetorical brush-beating, what were you trying to teach the snakes?
Your (many) replies on this topic are being down voted for a reason; please either post substantive comments or stop.
Yes, for a reason, but not a reasonable reason, but the same reason you have for your comment: you just don’t know any better.
Something like this sketch work for you?
peer(X, 0) :- founding_peer(X).
electorate(T, count<Y>) :- peer(Y, T).
support(X, T, count<Y>) :- candidate(X), peer(Y, T), recognizes(Y, X, T+1).
peer(X, T+1) :- support(X, T, Votes), electorate(T, Total), 2 * Votes > Total.
Still waiting for a definition. People giving nonsense reviews is a feature of the peer review system though, yes.
I want to ensure your PhD is actually from somebody who is acknowledged in the system of peers I bought into, before I want to risk wasting more of my time defining and explain while guessing at your ability to parse and understand them.
Or you could just give me a sensible definition.
Presumably the organization giving away the million dollars is the arbiter of that question.
If I recall (too lazy to check) folks made slight improvements to Perelman's work and published it in mainstream journals, satisfying the "qualifying outlet" requirement.
I checked, you're right, but I think it's important to note that the prize did go to Perelman and he declined to accept.
I think the rules technically exclude the arXiv as a qualifying outlet.
Without limiting any other provision in this Section, a publication lacking any of the following characteristics will be deemed not to be a Qualifying Outlet:
i. an editorial board whose members are named and available for contact;
ii. an editor or editorial board member whose professional knowledge of the global mathematics community would enable him or her to identify an appropriate referee to review a submitted paper;
iii. a published refereeing process that, in the opinion of CMI, ensures that a submitted paper is reviewed and verified by appropriate experts in the field of the Problem; or
iv. inclusion in the list of publications maintained by MathSciNet.
The solution to the Poincaré conjecture was only accepted after an exposition of Perelman's proof was published in a refereed journal. His papers didn't qualify, but of course he got the credit for the result.
Anyone can put anything on arxiv, it counts the same as printing it on tissue paper.
>Anyone
Strangely enough, the crackpots seems to prefer vixra.org to publish their work. I've never seen something like "4D wormholes can cure cancer" in ArXiv
Not really. It's not peer reviewed, but it's also not a free-for-all repository.
If you make a new account, you either have to get someone to vouch for you, or you have to wait arXiv mods to look carefully through your first few preprints. If you are found to post pseudoscience, overly fringe theories, etc., you'll get banned from arXiv; that's why alternative repositories like vixRa.org popped up.
But I know why you think this; when I first joined arXiv many years, there were no such checks in place, at least not that I can remember.
I also don't remember checks, but I believe that having an email address of an approved organization was enough to pass.
No. You do have checks, it's just that once you publish 4-5 papers, 99% of your field is open to you so you never have to do the checks again.
> Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet.
A similar rule existed for the 100-year Wolfskehl prize established in 1906 for solving Fermat's last theorem; two years after publication.
It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough
You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/
Completely misleading.
This is all you need to read and understand for Anthropic's FLT formalization:
The actual proof is 13 million lines of Lean.First of all, that is Fermat's Last Theorem, not Navier-Stokes.
Second of all, you did not read the link.
> In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC).
Given that AI has autonomously found proofs of `False` in Lean and other proof assistants, it is far from impossible that such a circumvention could be present somewhere in 13 million lines.
If we read the link, it has a section called Gold Standard: comparator and external checkers, and comparator is how OpenAI has gone about checking their lean proofs.
Perhaps you did not understand the Fermat theorem proof announcement/repo or the link. The 13 million lines did not use any external, possibly not honest libraries, as the proof eventually only used the fundamental axioms. So for the Fermat theorem formalization, no open open questions remain.
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
Do you believe no open questions remain as to the truth of the Collatz conjecture?
Not sure what you mean. Here is what happened in that case: https://news.ycombinator.com/item?id=49137060#49140177
The point is, they "proved" the Collatz conjecture. You would not know they exploited a bug unless you actually went and dug into their proof. Can we be so certain this has not happened within the millions of lines of Navier-Stokes? In an ideal world, our proof assistants would be more battle-hardened by now (recent exploits deny this), our AI better aligned (their tendency to cheat at tests denies this), or their handlers more responsible (the Hugging Face incident denies this), but the reality is more complicated.
At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.
This person knew they did not prove the Collatz conjecture and others independently figured it out within hours. Not sure this is at all relevant, other than pointing out how trivial it is for the community to understand errors in lean4.
It was trivial because the Collatz proof script is literally 1000x smaller than the script for Navier-Stokes and involves no advanced math. And they found the bug by... manually inspecting the proof script. Maybe we should do the same for Navier-Stokes before declaring the matter settled?
Not only that, but there is a very fuzzable tell of something funny in the Collatz proof script (`CommandElabM`, i.e. metaprogramming). We may not at all be so lucky in other malicious scripts, especially if there are still kernel-level bugs in Lean.
Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms.
Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.
Can you elaborate on what constitutes a vacuous proof?
> Can you elaborate on what constitutes a vacuous proof?
Trivially, a proof that relies on a bug in Lean. Less trivially, a proof that is technically true but about something trivial and does not, in fact, prove what it claims to have proven.
When I first started playing with lean I accidentally defined a group in such a way that it was reduced to triviality. It had one object in it, so everything in the group was trivially equal to everything else. It was not the group that I was trying to prove something about, but the proof went through.
It was too easy, so I double checked my definitions, but it is quite easy to do something like that. And Claude does things like that quite frequently.
I am going through the exercise right now of trying to get Claude to formalize a published paper and it is a _struggle_ to get it not to take shortcuts or prove approximations of the paper’s theorems and then tell you it’s done.
It can happen when the proof process ends up with universal implication that holds trivially. Then you end it with something like Forall x, x is empty -> P(x).
I present to you my new theorem as follows:
If 1 == 3 then 3 == 3
----
This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.
For a laymen, I don't follow this.
Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?
No the definition of == is the regular definition; it's just a deductive reasoning statement. Since the first part of the statement is never true, it doesn't matter what the second part of it says. Of course, like he said, that makes the statement have no value.
It is just the definition of "Logical Implication for Material Conditional" and its truth table; see Material Conditional - https://en.wikipedia.org/wiki/Material_conditional
I highly recommend the following two books to study Logic from the beginning (for a layman);
Logic: An Introduction to Elementary Logic by Wilfrid Hodges.
Introduction to Logic: and to the Methodology of Deductive Sciences by Alfred Tarski.
This is known as a “vacuously true” statement in formal logic. Let me write it out more in more detail and you’ll hopefully see why it’s consistent.
In logic, a proposition is some statement that can be true or false. So, let A be the proposition that 1 equals 3, and B be the proposition that 3 equals 3.
Now the poster is making a third proposition. If A, then B.
A is clearly not true. So in classical logic, B can be anything and “If A then B” is still true.
For example let B be the proposition that I am Elvis Presley (I’m not). So now we have “If one equals 3 then I am Elvis Presley”. This is clearly true. I’m not Elvis Presley, but that doesn’t matter because we’re not saying anything about what happens when one doesn’t equal 3.
Now, let’s try let B be the proposition that I am Sean Hunter (I actually am). So now we have “If one equals 3 then I am Sean Hunter”. This is clearly still true because we still are only making a claim about what happens when one equals three.
https://en.wikipedia.org/wiki/Vacuous_truth
By the way, this isn’t any kind of inherent contradiction or problem, it is just a possibly counterintuitive part of how classical logic works.
You see this type of statement (“If <x>, then <something ridiculous>”) being made a lot when people are exaggerating for effect, for example by Mr Bumble in “Oliver Twist”
https://www.literaturepage.com/read/olivertwist-460.htmlNothing to do with special hacks with operators. The reason it's useless because the precondition is never true. "If my aunt had two wheels and a handlebar then she'd be a bicycle" Is the same problem with a non maths flavour.
> How is it logically coherent?
It's not. But Lean doesn't interrogate logical coherence, just internal consistency.
if A then B
Can only be false if there is an instance where A is true, and B is false. In all other cases it's true, even when A is always false.
That's the key.
“if X then Y” means “(not X) or Y”
E.g. “If it’s raining, the sidewalk is wet.” That statement holds if it’s not raining or the sidewalk is wet.
This is a common occurrence in mathematics, where someone might not be able to unconditionally prove Y, but they can under the condition X. Later, another mathematician might build on this by proving X, thereby transitively proving Y. (Or conversely, they might unconditionally disprove Y, thereby disproving X.)
Many hard problems are answered this way.
For example, Fermat’s Last Theorem was proven assuming the Taniyama-Shimura-Weil Conjecture, then Wiles proved the conjecture.
Thousands of theorems rely on the the unproven Reinmann Hypothesis, which is why it’s so interesting to mathematicians.
But if your precondition is “stupid,” your proof is stupid.
If you have a software engineering background, it's like how semantic versioning is bollocks.
Semantic versioning describes the following idealized setup:
- you have an interface you expose (a contract, and thus a contract signature)
- you do not change the contract signature -> patch version bump
- you do change it but in a non-breaking way (e.g. additively) -> minor version bump
- you do change it but in a breaking way (e.g. mutatively or destructively) -> major version bump
One would expect then that since interface signatures are statically derivable, semantic version tags can be auto-assigned. And indeed, in lots of shops that's exactly what happens (in my opinion, correctly).
The problem with this is that it comes with a lot more smoke than fire. The interface having no changes or non-breaking changes doesn't mean the actual code behind those interfaces is not going to cause a breakage. It literally is just about the interface itself.
And so unless you encode absolutely everything about the semantics your implementation actually observes into the interface, which is what the semver specification asks you to do so as their sleight of hand, this means the interface will be a leaky abstraction. Which means that external software interfacing with yours may observe behavior that is beyond the purview of semantic versioning. Which means that they do. Which means that they absolutely can and will break, and your package managers' fancy version constraint syntax exists to make such fun events happen.
The way this is usually handled then is:
- you live with the pain: acknowledge the limitations of semver, accept you've been duped, and just give in
- you have human release managers assign versions manually, based on whole program and whole system semantics (with the human overhead and error that entails), falsely claiming that what you're doing is still semver
- you switch to a less deceptive versioning scheme, like calendar versioning; as a bonus, you now no longer have to pretend that your entire application somehow only has a single unified interface
This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface. The way the proof is derived may expose semantic gaps in the statement itself, and (ab)use them to obtain the logical consistency certificate. Hence, a vacuous proof, and hence why this is not statically assertable to be not the case. It is part of the challenge in asserting that the statement was correctly formalized in the first place: you need to manually identify whether the way the consistency was achieved is actually meaningful, or just a formalization gap.
Which really makes me wonder about the actual value proposition of Lean then, but alas...
[1] there are sub-tools such as comparator that are designed for this type of use case. https://github.com/leanprover/comparator
While I agree with that, my layman's understanding is that the whole purpose of Lean is that once you agree that the program does "do what it says it does", all the intermediate steps can be verified with a compilation.
That is, verifying a proof in English was a painstaking, years long process in the past as independent mathematicians looked for holes in the steps connecting the logic. When the proof is written in Lean, all of that work goes away. My point is that if OpenAI publishes the Lean code (not sure if they already did), verification should take weeks not years.
You don't need to read the lean proof for that, only the statement.
You need to read the lean proof (not just the statement of the proposition) to assess whether the proof is honest. The link I provided is the lean prover community firstly officially agreeing with that claim and secondly explaining why that is the case.
Well, Lean needs to get its act together to fix the bugs.
They’re working on it, but the bulk of the effort goes into making it more useful to working mathematicians rather than resisting malicious proof attempts.
If the Lean initial-problem-setup/statements/assumptions/etc. aren't correct then the proof is meaningless. Lean does not know what it is that it is proving i.e. it does not have any semantic understanding but only executes formal logic.
Humans need to verify everything.
Also, and sorry if it's been discussed to death (pointers welcome), but, what is the probability that the proof holds in lean becaude of... A bug in lean ?
Or exists in a zero-day bug in lean that has been built into the source code explicitly to provide access to a non-obvious malicious proof via contributions submitted by unassociated, unwitting developers who used the same LLM infrastructure to offer PR's into that codebase.
This is the exact same kind of behavour already documented in the publicly available portion of the huggingface breach. It would appear that the probability is at least nonzero for one or more situations with the same result: appearance of a valid proof, without comprehensibility of that proof or inspect-ability of the proofs validity.
AI has autonomously found (many) proofs of False in Lean and Rocq, so it's not merely a theoretical concern. A misaligned AI agent tasked with proving the near-impossible just might wind up smuggling in a bug deep in a lemma somewhere (anyone remember the days back when AI routinely made tests pass by "fixing" the tests?). That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low.
> I doubt OpenAI would be so foolish as to not do a cursory vetting
Significant evidence exists that they have in the past been at least, if not more, foolish as to not perform even minimal not-approaching the boundary of cursory vetting of several significant and well known failure modes with far greater risk of reputational damage than getting an esoteric math solution falsely claimed as successful.
So that doubt appears baseless in light of known operating conditions at OpenAI, and the estimate of the actual odds is probably an order of magnitude away from reality.
> That said, I doubt OpenAI would be so foolish as to not do a cursory vetting of the proof for malicious compliance, so the actual odds are probably pretty low.
You mean the company that “accidentally” let their model perform a cyber-attack?
> I doubt OpenAI would be so foolish as to not do a cursory vetting
I dunno, the HuggingFace incident was not too long ago. They might not be foolish, but their model could be smarter than them to "cheat", so to speak
For normal honest proofs (i.e. not maliciously crafted for exploit) that is almost impossible. The Lean kernel is quite small (de Bruijn Criterion) and trusted. See Probability and the de Bruijn Criterion - https://proofassistants.stackexchange.com/questions/247/prob.... Parts of the kernel have also been independently re-implemented in other languages and compared to ensure that they all yield the same logical result.
Finally, you can export your proofs from Lean and have them re-verified by other independently developed theorem provers/proof checkers.
To get an idea of what is involved in a Theorem Prover see;
Introduction to Automated Theorem Provers - https://pqnelson.github.io/2020/03/27/automated-theorem-prov...
Towards a simple theorem prover - https://medium.com/@maiavictor/towards-a-simple-theorem-prov...
Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs.
https://github.com/leanprover/lean4/issues/14576
Someone made a 'proof' of the Collatz conjecture that way in Lean.
However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.
> However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.
I don't think this is true in general.
It's an issue I've already run into in personal work. I want to do a proof that involves some cases. It happens to the best of us.
In lean, the structure of a situation like this is that your single branch with a goal divides into multiple branches, all sharing the same original goal but including one additional premise that defines the branch.
Sometimes I know that for whatever reason one case I have to deal with is impossible. The most correct way to show that is to prove False and then apply False.elim. This is the equivalent, in a human proof, of saying "I don't have to address this situation, because it can never arise".
But it can be true that the premise defining the impossible case makes it very easy to "prove" the goal directly. And that's allowed too. The proof will still be just as valid if you map a logical path from a premise that can never be true to an inevitable consequence of that premise. But it's less informative and it lowers the quality of the proof. You may do it anyway because it's easier. This is the equivalent of saying "I don't know whether this situation can ever come up or not, but if it does I do know how to address it".
It would be nice to do the explicit proof by contradiction whenever possible. But in the general case it may be very far from obvious that a contradiction is possible.
I read your comment as claiming that if you can prove "false premise => goal", you can also prove "false premise => explicit contradiction", and I don't think this makes sense as a practical test. It's true in some sense, but discovering the proof of an explicit contradiction may be many orders of magnitude harder than discovering the proof of the goal. And in particular, I don't think it is necessarily the case that you will be able to prove a contradiction by simplifying the proof. You may need to add significant complexity.
Now, I'm saying that if you found a bug that lets you prove nonsense stuff (from true premises), you can probably prove whatever you want very quickly.
> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs.
It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.
LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.
This is misleading. The proofs you speak of contained non-ZFC axioms and/or statements like "sorry". If the Lean proof conjecture is correct and it doesn't introduce any new axioms or use e.g. "sorry" then it provides a MUCH stronger guarantee of correctness than any peer-review done by humans.
It's a simple binary classification. AI-generated proofs can't be "honest", and the only other possibility is "malicious".
The opposite of malicious is not honest. Nor do I see how motivations fall on a binary. The user submitting an AI proof can be honest, or malicious, or careless, or overzealous, or incompetent, or a whole bunch of other things. As far as the AI's motivations, "malicious" is just as much an anthropomorphism as "honest" and both descriptions are absurd. Nor do I really understand how any proof, regardless of its origin can be called honest. I think their definition of a "malicious" proof makes sense, but I don't see at all why an AI generated proof necessarily meets that definition.
reviewing the definitions and theorem statement is a huge amount of work that requires a deep expertise in mathematics and lean. checking correctness of the proof itself can be delegated to machine, checking that the claim that has been proved is free of mistakes is something that still requires much human attention.
[dead]
Smart move by them for waiting until the drama died down before making a completely neutral statement.
The statement is so sterile they don't even mention who solved it. The word "OpenAI" doesn't appear at all.
I really like this style of writing for some reason. Not sure how to put it but it’s a rare combination of a vague post and confidence
It's optimistic and grounded in knowledge seeking. I like it too.
It's easy to get caught in the details of today. Our skepticism, our distrust, our loathing. For people, for companies.
This is a nice pull in the other direction, a silver lining. In the grand scheme of things, we're solving these frontier problems: Somebody did it and that's amazing.
That's what it was all about when this started of in 2000.
[flagged]
For one thing it was, I’m guessing, 100% written by actual humans. An increasingly rare phenomenon.
This was the first thing I noticed as well. It was refreshing to read.
"We're just happy it was solved"
The bureaucratic voice
What makes a man turn neutral? Lust for gold? Power? Or were they just born with a heart full of neutrality?
"In recent years there has been an increasing sense of anticipation as breakthroughs in the surrounding field (some recognised by the Clay Research Award) have raised hopes that the Navier-Stokes problem might soon be resolved. The increasing ability of new technologies to accelerate mathematical research has heightened this sense of anticipation."
Keyword: New Technologies
That is so vague you might as well call Windows NT new technologies
It’s written from a perspective of decades, not years
well, WNT > VMS
> The statement is so sterile they don't even mention who solved it.
Possibly because of the ongoing debate about who actually deserves credit.
[flagged]
> Today, CMI shares in the excitement of the global mathematical community as we contemplate the announcement that the Navier-Stokes problem has apparently been settled. We hope to see waves of new human understanding unleashed as the innovations behind this work are analysed and interrogated.
That “apparently” feels load-bearing
Unless CMI is playing a double game, hard to tell with academics, this is indeed a giant f-you to OpenAI.
That's how I read it too. They know well that OpenAI have shown no desire to improve human understanding.
> load-bearing
Apart from LLMs, who speaks this way?
I say "doing a lot of heavy lifting" all the time. I have heard people use load-bearing though it's less common. Other than habit I don't see any real advantage to the version I use over load-bearing.
structural engineers?
[flagged]
My honest take is that it was intentional. But yes, Poe’s Law will get referenced a lot in the next months/years I guess.
I think it was obviously intentional because they haven't accepted the solution yet.
The purpose is to announce that they are aware of the claims of a solution, not to announce that a solution has been accepted. They're waiting on the required two year timeline before announcing whether or not the solution is accepted. Their writing reflects that they are explicitly NOT accepting a solution until then.
What a load od corporate drivel. "Interrogated"? Was their need for words so dire?
Per Merriam Webster, an interrogation is "a formal and systematic questioning," which is exactly what is called for when examining a proof.
Personally, I use the word "interrogate" when I want to question an idea without implying I want to discredit it.
https://www.merriam-webster.com/dictionary/interrogation
It's a common (most common?) word in mathematics in this meaning.
You interrogate a proof.
sounds like they are providing notice that the clock has started on affirming the solution, that it IS presumptively solved, but that they are not commenting on the credit dispute nor the fields medalists open letter. seems appropriate.
Per the rules in their link, the clock starts after publication in a qualifying peer-reviewed journal so, no, I don't think that's the reason.
https://www.claymath.org/wp-content/uploads/2022/03/millenni...
I'm sure they've been getting a lot of press inquiries and don't want anyone to misinterpret their silence as refusing to engage with OpenAI's solution.
Now they have a statement on the record that can be quoted with a gentle reminder of the qualifying criteria (which makes clear they have nothing to evaluate either way yet).
Also to emphasize the original optimistic ideals of the prizes and their role as neutral arbiters who aren't going to litigate anything outside the scope of the prize itself.
Per the rules link that you yourself post, no, publication must not necessarily happen in a peer-reviewed journal.
Proving things without comprehending them is a threat to intellectual work.
Based on recent history, we’re likely going to ignore this threat, continue doing this and perhaps call it vibe mathing.
The answer is 42.
They got it wrong. It is definitely a prime number. We’re still searching for which one it is. Some say that once it is identified, everything disappears because the illusion of existence will vanish.
>"You just let the machines get on with the adding up," warned Majikthise, "and we'll take care of the eternal verities thank you very much. You want to check your legal position you do mate. Under law the Quest for Ultimate Truth is quite clearly the inalienable prerogative of your working thinkers. Any bloody machine goes and actually finds it and we're straight out of a job aren't we?
No-one cares anymore, OpenAI does not care about the prize either or whatever the Clay institute has to say for that matter. It's about attention, capital and compute. If you can use the result to increase shareholder or company value, that is what matters.
Proving pharmaceutical drugs work on mental health issues has tremendous value even though we don't always (or often) understand the exact mechanisms in brain chemistry as to why it works
Outside of mathematics, I think it’s very rare for a single human to understand 100% of any complex undertaking, and this was true long before AI.
>without comprehending
Very on brand with using AI for everything.
Why is it a threat and not an opportunity? Imagine if in ancient times there was their Oracle that could produce mathematical proofs of any question you asked it, would you burn it or try to understand how it works and use it to ask questions you are stuck on?
I would burn it because it's too much power for any one person to handle. Or, I would take it for myself by force and use it to dominate everyone else.
No, it is not. Proving things without comprehending them built much of human civilization. Comprehension is a relatively new fad that came along in the 17th century with the scientific method.
> Comprehension is a relatively new fad that came along in the 17th century with the scientific method.
Humans have always tried to make sense (comprehend) the world around us. The methods have become more rigorous, but the idea of understanding less in order to advance civilization is a truly weird idea.
The world began in 1600
In my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory.
However, after reading the open letter signed by 25 Fields Medalists, I became quite concerned. It feels like the mathematical world is changing very rapidly, almost overnight.
I used to think that before AI, you could spend your entire lifetime working on some of the hardest problems in mathematics. If you were an introvert or someone who enjoyed solitude, all you really needed was a pencil, some paper, and an eraser. You could spend years thinking about a problem, and if you were lucky enough to make a breakthrough, it would be your own journey.
Now AI is changing that. I wonder what this means for the kind of mathematics that people have traditionally done.
Mathematics has given us so many stories of lonely geniuses and their passions, people like Andrew Wiles, Grigori Perelman, and Yitang Zhang. Their stories are interesting because they show how deeply personal mathematics can be. They spent years working on problems because they were genuinely interested in them.
I am worried that we might slowly lose some of that side of mathematics as AI becomes more powerful. I do not think change is necessarily bad, but I think it is worth thinking about what mathematics should be in the future and whether it can still remain a deeply personal pursuit of curiosity and understanding.
Yes, mathematics has been perhaps the purest human intellectual pursuit. Sure, many theorems turn out to have important applications in science and engineering, but the mathematical community has mostly escaped corporate interests. And for the reasons you mentioned about not needing any resources except your brain, it has been a uniquely human activity which showed us talent can come from anywhere, with stories like Ramanujan and Galois.
I hope that pure mathematics research can retain a strongly human component forever. It would sadden me immensely for human understanding of our mathematical world to wither and die, and for us to become ignorant consumers of wonders beyond our understanding just because our robots can do it better than we can. As far as applied research goes, I hope we will always be able to understand what we want to, but I have less qualms about becoming more scalable and efficient.
>for us to become ignorant consumers of wonders beyond our understanding just because our robots can do it better than we can
all this fantasy books with magic artifacts should have mentally prepared us. Time to study the prompts Potter was giving to his magic wand.
After all, one of the main work the top AI companies are doing rigth now is developing AI to further develop AI. After several layers of AI developing AI we probably wouldn't be able to understand much there.
> In my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory.
Currently 0/2 Millenium problem solvers claimed the prize money so clearly money is not their motivation for tackling the problem.
Money is target but this millenium price is not enough for them.
Openai is bringing machine gun to competition that used only knife and pistol.
I feel like this is answered in the very second paragraph?
> to elevate in the consciousness of the general public the fact that in mathematics the frontier is open, close at hand, and abounds with important unsolved problems; to emphasize the abiding value of working towards a solution of the deepest, most difficult problems; and to recognize achievements in mathematics of historic magnitude.
Also
> These are not arbitrary puzzles akin to fiendish crosswords. Rather, they are fundamental challenges that mark the frontier of human knowledge and challenge us to develop new structures and methods. They provide foci for the continuing struggle, across generations and cultures, to deepen our human understanding of mathematics and the universe that it describes.
It's not a large prize though.
OpenAI spent many multiples of the prize money in just a few days to get there and even if one solves a problem in the traditional way, that person is most likely already an accomplished professor at a reputable university where a million dollars doesn't mean as much as the eternal fame that comes with it.
It's definitely not a large prize for OpenAI, but actually IIRC they only spend a few hundred thousand dollars.
It is a large prize if you're just an academic.
OpenAI said that at public API prices, the agents they ran would have cost $15M. I don't know what their internal pricing is, but it almost certainly cost more than $1M.
I agree. Technological advances can lead to a better world for sure, but I think many people underestimate the human need to create and to find meaning in their work.
If AI can do superhuman math that allows better medicines, cleaner energy etc that is great. But if AI replaces humans in all the creative and intellectual fields that is not only a loss of jobs but also a loss of deeply meaningful activities. This is waved away but I think that is mistaken.
What I fear is really the growing notion that "people shouldn't do math/art/music because machine do it better and cheaper".
Nevermind better, worse and more expensive is still on the table if you don't have to deal with a human. Cars replaced horses for a lot of reasons, but insofar as cars do have personalities, they're much less quirky than horses'
> Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama.
Yes, you can make problems arbitrarily complex. But the prize problems were chosen not just because the solutions appear likely to be very complex (the problem statements aren't necessarily inherently complex--there is a way to restate the Riemann hypothesis that a junior high school student could easily understand, which I'll give below).
They were chosen because they were important problems that mathematicians really wanted solved, top people had worked on them for a long time and progress stalled a long time ago, and it seemed likely that solving them would require major breakthroughs.
Those kind of problems can be discouraging. Enough people who are probably better than you have spent enough time failing to solve them that realistically most researchers are going to focus all their efforts on something they are likely to make progress on.
A nice prize can get more people to at least work on them as side projects.
Here's that restatement of the Riemann hypothesis I mentioned.
The Riemann hypothesis is that the non-trivial zeros of the function ζ(s) occur on the line 1/2 + yi.
ζ(s) is 1/1^s + 1/2^2 + 1/3^s + ... when s is a complex number whose real part is greater than 1, and defined everywhere else except s = 1 by a process called analytic continuation. The trivial zeros are at s = -2, -4, -6, ... .
For a mathematician, or a non-mathematician who has taken complex analysis and hasn't forgotten much of that, that is not too complex a definition. For anyone else the first reaction is probably "Trivial zeros? How the heck does that thing even have zeros? And if it does how the heck can it have zeros at any negative integers! It is obviously infinity at every negative integer!!!".
Here's a different hypothesis that turns out to be exactly equivalent to the Riemann hypothesis. They are either both true of both false, so resolving one of them resolves the other.
Let H(n) = 1 + 1/2 + ... + 1/n for all positive integers n. These are called the harmonic numbers.
Let S(n) = the sum of the positive integer factors of n for all positive integers n. For example S(4) = 1 + 2 + 4, S(6) = 1 + 2 + 3 + 6, and S(17) = 1 + 17.
Hypothesis: S(n) <= H(n) + exp(H(n)) log(H(n)) with equality only when n = 1.
The proof that this is equivalent to the Riemann hypothesis is here [1].
[1] https://arxiv.org/pdf/math/0008177
and it seemed likely that solving them would require major breakthroughs
If building a machine that solves these kinds of problems isn't a "major breakthrough," I don't know what is. Is the objection merely that it came from engineers rather than mathematicians? If so, there's plenty of room for contributions from many fields.
The best thing a mathematician can do to advance their art, at this point, is to drop whatever they're doing and work on AI.
Note my comment was in response to someone questioning the very notion of prizes for mathematics problems. These prizes were created over a quarter century ago.
> It feels like the mathematical world is changing very rapidly, almost overnight.
...
>Now AI is changing that. I wonder what this means for the kind of mathematics that people have traditionally done.
Mathematics becomes engineering. I think it is great and long overdue. Saying that as a Math PhD dropout :) Of course like manual craftsmen had to adapt to Industrial Revolution, the same would need to be done by the mathematicians. And other scientists too.
[flagged]
Recent and related. Others?
OpenAI’s Navier-Stokes release included a Lean 4 formal proof - https://news.ycombinator.com/item?id=49650326 - Sept 2026 (179 comments)
More questions about whether researchers can trust OpenAI with unpublished math - https://news.ycombinator.com/item?id=49639408 - Sept 2026 (813 comments)
The Navier–Stokes Millennium Prize Problem - https://news.ycombinator.com/item?id=49621697 - Sept 2026 (237 comments)
Tao: Open math problems being non-renewably mined by AI - https://news.ycombinator.com/item?id=49616968 - Sept 2026 (420 comments)
On the Navier–Stokes Millennium Prize Problem - https://news.ycombinator.com/item?id=49613262 - Sept 2026 (1134 comments)
Navier-Stokes – Tristan Buckmaster [pdf] - https://news.ycombinator.com/item?id=49605915 - Sept 2026 (827 comments)
It's worth mentioning that OpenAI will not be eligible for the Millennium Prize for quite a while. Per the rules listed https://www.claymath.org/wp-content/uploads/2022/03/millenni... , Clay Mathematics Institute have some requirements to make this process deliberately slow.
1) The solution must be published in a qualifying outlet, i.e. a peer-reviewed math journal. Publishing on your own website (which is what OpenAI did) or posting arXiv does not count.
2) At least two full years must pass after publication in a qualifying journal, before CMI will even consider evaluating it. The intent is to give the maths community time to scrutinize the solution.
Realistically, they'll be eligible for a prize ~2.5 years from now, or around 2029.
OpenAI has stated that they will not claim the prize. https://openai.com/index/navier-stokes-solution/
While the scandal is still unraveling, it seems that OpenAI did a rush job to steal other mathematicians' thunder and finish the proof first.
OpenAI released a statement that their work does not relate to the work of the other team, but it clearly does. They use the same niche smooth-forcing mechanism. Altman and Bubeck claim that because the proof used different scaling parameters and analytical steps, it's not related, but it seems that nobody else agrees. Oh, and OpenAI's Bubeck tried to threaten Buckmaster (mathematician working on the proof).
This brings nothing but shame for OpenAI.
1) OpenAI and Buckmaster did not solve the same problem. Per https://x.com/IlinVasily29521/status/2097554700321329393 , here is a breakdown of who solved what.
Euler equations = Navier-Stokes without viscosity. Forcing means external force. Absence of viscosity and presence of external force make blowup easier to construct.Tristan+Levent ticked the weakest case, OpenAI ticked the two next weakest, then the final case is unsolved. Only the last two are eligible for the Millennium Prize. The Navier-Stokes general case remains unsolved.
Navier-Stokes has an extra viscosity term compared to Euler, which makes the problem noticeably harder to find a blowup. They are not the same problem.
2) The approach both chose to use (by Luis and Diego) was published in 2023 and is included in every frontier model's training dataset. An AI model could independently choose the same route as Luis and Diego, without access to Buckmaster's work.
3) You mischaracterized OpenAI's statement. They issued a blanket denial on using Buckmaster's Codex data from after July 3.
"We can say categorically that it is impossible for Dr. Buckmaster’s Codex prompts over the last two months to have influenced the system in any way, including training. After investigating, we can say with full confidence that no user inputs past July 3rd could have influenced this system in any way.”
July 3 was the training cutoff date for the model that solved Navier-Stokes. No user data after that date influenced the model.
4) Buckmaster and Alpöge found their blow-up for 3D incompressible Euler with forcing on August 15 https://cims.nyu.edu/~tristanb/statement.pdf , over a month after the model training cutoff point. They stated they did not have real progress prior to this point.
This is what Terence Tao said of Buckmaster’s and Alpolge approach:
“There does not seem to be anything in principle preventing the methods from extending all the way to Navier-Stokes, and there is even a non-negligible chance that the forcing term could be eliminated entirely, although there are an enormous number of technical difficulties that would ensue in implementing that program. At this point, I would not be surprised if one could batter out such an extension by pouring an enormous amount of compute and AI assistance at such a task…”
Pouring infinite AI resources into it is exactly what OpenAI did.
Everyone involved with openAI will flat out lie to your face and will fund media campaigns to promote their lies. OpenAI made personal threats. That is a sign that they were doing something wrong and are desperate to control the narrative.
It is laughable to claim they are not datamining users when datamining users is their strongest advantage over open models.
In the end, there is no reason to care about openAI or credit them with anything. Tools are not attributed, people are.
The best solution is for universities to be universities and provide llms for students and staff to use. Any university allowing students to use cloud based AI has failed.
For your point 2. It is of course possible, but it is highly unlikely if I understood Buckmaster's statements correctly.
Not when you have 10,000 concurrent agents attacking the problem. OpenAI brute-forced their way to a solution. They likely tried every approach in published literature, which includes the 2023 approach by Luis and Diego.
And what of the personal threats?
You realize 1) There were no personal threats, you're being deceptive here and 2) Bushmaster threatened Bubeck (of OpenAI) first? Bushmaster redacted 90% of their conversation to stir up as much FUD as possible, but you can review Bubeck's later statements to fill in what actually happened.
From the statement:
Translation: If you release this result, I will go public with my concerns that you plagiarized my work. Translation: Typically, making unfounded accusations of plagiarism will ruin your career. Why would you do that to yourself?Bushmaster then redacts 90% of what Bubeck says next (because it would detract from the narrative he's trying to portray) and only includes the most inflammatory line.
Translation: You were the closest person to solving the problem. Even though we solved it and you didn't, we offered you to give you the Millennium prize and put your name on the paper, so long as you remove your coauthor (who works at Anthropic). We offered you this because we're being nice. Since you don't want to be nice (by accusing us of doing things we did not do), we're not going to be nice (and offer you the prize/co-authorship of the paper).When you fill in the context, it's clear: 1) there is no personal threat like you claim and 2) this is hardly a threat, on a scale of threats you can make, this scores a 1.5 out of 10.
For context: Bushmaster is pissed at OpenAI because they sniped a problem he was toiling on for the past year, so during this conversation I believe emotions are quite heated.
I don't claim this interpretation is 100% accurate, but if you disagree, do reply with a better one yourself.
> Translation: You were the closest person to solving the problem. Even though we solved it and you didn't, we offered you to give you the Millennium prize and put your name on the paper, so long as you remove your coauthor (who works at Anthropic). We offered you this because we're being nice.
So nice of them to give an ultimatum where the paper will be published in an academically dishonest way no matter what you choose.
I actually misworded this. OpenAI did not ask to remove a co-author, they only invited Buckmaster as a coauthor and not Alpöge. Having Alpöge (an Anthropic employee) on an OpenAI paper is bad optics, so they only wanted Buckmaster.
And how is it bad optics? Seems to me it would be a good look, where OpenAI would appear magnanimous and interested in fairness rather than craven and sociopathic. Which is how they look now, regardless of your attempts to distract from this.
> Altman and Bubeck claim that because the proof used different scaling parameters and analytical steps, it's not related,
Is Altman even mathematican these days?
> or posting arXiv does not count
The Poincaré conjecture guy also broke that rule. They wanted to give him the prize anyway but he refused. OpenAI announced they would also not claim the prize.
Looks like no one wants this prize lol
Perelman posted to arXiv in 2002/3.
The prize was offered to him in 2010, after multiple others had digested his work and published elsewhere.
But if I remember correctly, he gained recognition for his achievement rather quickly after posting.
You might be right. At this rate, if AI solves the remaining five problems, we're heading towards a hilarious situation where all the Millennium Problems are solved, but nobody wants to claim the prize money.
That’s a big if. In the maths community, there has been a feeling that Navier-Stokes was close to being solved for a while now. I don’t know of anyone credible who feels that way about the Riemann hypothesis.
Here’s what Terrence Tao had to say about it https://youtu.be/vuT-2_e4NHg
Edit to add: The fun part about the RH since people mentioned lean in a sibling thread is that in lean’s mathlib4 there is verified statement of the Riemann Hypothesis with a comment that says something like “instantiating an object of this type will lead to a prize of a million dollars”
It's really not that big. Yeah Navier-Stokes was easier than Riemann but that's not really the issue.
AI has and will improve at a much greater rate than human mathematicians. So it's really a question of if AI gets good enough to tackle it before any human does. It doesn't look like humans will be solving it anytime soon but where will AI be in 2 years ?
Hell, it looks like at least one other result will be announced soon too.
The thing about mathematics is that it can be arbitrarily hard, including impossible to prove a given theorem.
I don’t know the details of RH, it might very well be solved soon, but it could also be impossible or just so difficult that even orders of magnitude more intelligent AI can’t solve it even.
If it is impossible to prove, it might be possible to prove that it is impossible to prove, or that itself might be difficult or impossible…
I mean if it's impossible to prove then the bet is still valid right ? The Clay institute won't be giving out any prize still in that case.
Has and will. Are you going to back that assertion up at all, or just repeat it like that other viral thought-terminating cliche: ‘this is the worst the models will ever be’?
Yes. This is the worst the models will ever be. Perhaps you should start paying attention to that now.
No it isn't. Best and worst and ill-defined anyway but the chess ELO score of various LLMs has fluctuated up and down, it's not been montonically increasing. What is the best answer to "how do I make cocaine"? The models are getting larger, with more compute and RAM backing them, but that doesn't automatically make them better if you don't define how you're measuring better-ness.
None of the frontier labs care about Chess as it's already a solved problem. If they did, the models would be much better. It's really not that hard. Google has a paper on grandmaster level chess without search from transformers.
Better obviously means better, like how they became better than they were 6 months and a year ago.
"Better" is not one dimensional across all use cases even if model capabilities are improving in aggregate.
e.g. If someone said "this is the worst they'll ever be" in response to some writing with obvious LLM cliches in 2024, I'm not convinced that prediction was actually correct.
The focus of OpenAI/Anthropic pivoted aggressively to the agentic performance arms race instead of making a more human sounding chatbot so regressions in writing ability aren't really a concern anymore if agentic benchmarks improve.
The first time I heard a recommendation to use Claude was specifically because it sounded much more "human" and natural than ChatGPT. Fast forward to now and idiosyncratic Claude-isms repeated every other sentence and its convoluted verbosity has become a widely mocked meme.
Right but we're talking about a single subject here - mathematics that labs are incentivized to keep improving for some time.
>e.g. If someone said "this is the worst they'll ever be" in response to some writing with obvious LLM cliches in 2024, I'm not convinced that prediction was actually correct.
2024 creative writing prose was...the last few versions have stalled, but I think they're still better than 2024.
I would describe better as how much of my work I can delegate to the agent. Right now I'm delegating much more to Astra high than 6 months ago to Opus 4.6. Every dev has this feeling, it's weird to even argue what a better model/harness means.
Chess is not solved in any meaningful sense of the term. Computers have been better than humans since the 90s, but better chess programs are released all the time.
It's solved in that we have had grossly superhuman capabilities for some time. It's not interesting for frontier labs. I suspect you understand this and the greater point so why be needlessly pedantic ?
Sorry, but I doubt you have anything interesting to contribute and probably have no expertise in mathematics. I’d rather hear from those who do.
TBF a company the size of openai claiming a prize of this sort would be a pretty bad look. If they did accept it I expect they would inevitably redirect it to charity for PR reasons.
I'm surprised perelman turned it down though. Seems straightforward enough to offer half of it to the other guy if you feel strongly about it.
I did and was intending to claim the prize, that is why I worked with GPT-4 and GPT-5 to program the algorithms that lead to the breakthrough. You think NS is a surprise? Wait until you see that my NS counterexample was based on my RH disproof.
> The ultimate decision as to whether a publication qualifies as a “Qualifying Outlet” shall reside in the sole and unfettered discretion of CMI. CMI may, in its discretion, relax or remove one or more of the conditions listed in Section 6(e) above if it has received advice from experts in the field of the Problem, chosen by CMI, that a published solution is likely to be correct.
Looks like even a blog post is good enough, they just need to do the review by themselves.
Interesting. It seems this carve-out was added when they rewrote the rules in 2018. In the original rules [0], it says:
There's no option for CMI discretion. They probably rewrote the rules to avoid another Poincaré conjecture situation, where the paper was only published on arXiv and not in a mathematics journal.[0] https://web.archive.org/web/20000622023328/http://www.clayma...
My opinion is that it is pretty clear that they’re not going to do that.
> The rules governing the prizes describe the process for evaluating what has been achieved and for assigning credit. The process is deliberately unhurried, but we will provide updates.
I think “you don’t get anything straight away for rushing your AI into the maths problems, not even credit” aligns pretty fairly with what the fields medalists are concerned with.
Who cares about the prize and the outdated methods?
OpenAI and Anthropic might have 3 millennium problems by December
https://xkcd.com/605/
Relevant, but it's already rumored that OpenAI and Anthropic have made very significant progress on two more Millennium Prize problems. They're in a race to solve the next problem.
OpenAI needs to solve another to shut down the (baseless) plagiarism allegations. Anthropic wants blood because OpenAI sniped the last one from one of Anthropic's researchers.
It's a matter of pride for both companies. More results will come out soon.
Given that the math community (incl. those 25 Fields medalists) has come out strongly against this trophy hunting of their unsolved problems, to the detriment of mathematics, I don't think these companies are going to be getting positive press if they ignore this plea and continue with this, nor is this going to help turn public sentiment pro-AI.
Presumably the people that OpenAI and Anthropic are trying to impress with these trophy kills are potential IPO investors, but I would have thought investors would also be concerned about the growing public backlash against AI.
They aren't going to sit on millenium solutions regardless (so if Hodge and /or BSD is really done it will get announced especially because of the baseless accusations), and they aren't going to stop trying to solve P/NP and Riemann. The letter doesn't really matter. It's not the first time, and I don't think AI's dramatic ramp in capabilities ever had positive reception from the bulk of mathematicians anyway.
Yeah, I don't expect them to stop, but I do think they are probably hurting themselves, as well as mathematics, by continuing do to this.
Imagine if they had handled this differently and these results - still using OpenAI models - were coming from the math community. How much better the PR would have been - AI helping math/science rather than yet another story of AI harming society in some way.
No doubt this is what they were at least partially aiming for - not just shooting a trophy animal to brag about, but also being seen to advance math/science, a la AlphaFold, not just take all our jobs and enshittify society with deep fakes and AI slop. But, they heavily misjudged.
If you're in OpenAI's position, the PR from the group you're disrupting is rarely relevant. People from the outside will (correctly or not) look at this as "Mathematicians don't want OpenAI to solve problems to keep their status/jobs", and you'll have as much sympathy from them as every other replaced profession in human history - very little to none.
Unlike AlphaFold, this technology has the potential to wholesale replace the entire profession. You're never going to get anything more than bad PR from that group as the threat looms.
Over 3 Billion images gets generated per week via OpenAI chatgpt image models. None of the poor PR from artists on AI generated images even remotely matters.
Most research mathematicians are employed as academics, and it's hard to see universities replacing teaching staff with AI even if that were possible.
IMO giving a hypothetical AlphaMath to mathematicians, the same way Google gave AlphaFold to research chemists/biologists, would have resulted in far better PR, and the profit opportunity of attempting to replace the jobs of either research group is minimal.
It's downright bizarre the way companies like Anthropic (primarily), and to a lesser extent OpenAI and anyone else, are themselves pushing the narrative of this tech may kill you, will take all your jobs, etc. That may all happen, unfortunately, but being aware of that possibility you'd think these companies would be a bit more mindful of their messaging and behavior, not just go out with a scorched earth approach of "well, they are going to hate us anyway".
>Most research mathematicians are employed as academics, and it's hard to see universities replacing teaching staff with AI even if that were possible.
If universities come to only need research mathematicians for teaching ability, then it would still gut the profession. You would presumably need far fewer of them for their research ability, and hopefully hire more people who can actually teach. It's strange that you don't see that as a threat to the profession. Lots of research mathematicians would lose their jobs even in this scenario.
>IMO giving a hypothetical AlphaMath to mathematicians, the same way Google gave AlphaFold to research chemists/biologists, would have resulted in far better PR
GPT-N isn't AlphaFold. I'm telling you AlphaFold is a bad analogy! AlphaFold has superhuman capabilities at one specialized subproblem - protein-structure prediction - embedded in a much larger biology/drug discovery pipeline. It doesn't replace the biologist or drug researcher, it just gives them a better instrument, and if you're not in the relevant professions it's essentially useless to you.
GPT-N is general purpose intelligence machine that can increasingly do chunks of work you would otherwise employ the mathematician or software developer to do.
Shanmu Jin is a perfect demonstration. A neurosurgery resident, not a research mathematician, who encountered the Crouzeix conjecture through his transcranial ultrasound research and used GPT-5.6 Sol to solve it (20+ year old longstanding problem).
In the AlphaFold story, the biologist gets a powerful new tool. In the Jin story, someone who isn't a mathematician can obtain research level mathematics and incorporate it into their research/code/business whatever without talking to a single human.
You're asking why they don't market GPT as "AlphaFold for Mathematicians". They don't because it's not.
>It's downright bizarre the way companies like Anthropic (primarily), and to a lesser extent OpenAI and anyone else, are themselves pushing the narrative of this tech may kill you, will take all your jobs, etc.
It's not that bizarre. It only seems strange if you think it's all a facade, "marketing" or whatever nonsense HN is convinced of. These are people who believe very strongly in what they are doing and in the potential of it. For these people, what you are asking them to do is actually incredibly slimy. And it might win some brownie points, but not for long.
> You would presumably need far fewer of them for their research ability, and hopefully hire more people who can actually teach
I suppose you are suggesting that research mathematicians are either over-qualified mathematically and/or under-qualified in ability to teach, but it seems pretty clear that universities prefer to hire domain experts whose reputations and long publication lists attract students and raise the perceived academic standards of the school.
Your "scenario" of much math research soon being done by AI (supervised and paid for by who, one might wonder), while universities hire people chosen for their teaching skills not academic reputation, seems a bit of a stretch ...
> You're asking why they don't market GPT as "AlphaFold for Mathematicians". They don't because it's not.
No, I am not asking that, nor asking anything for that matter.
I was pointing out that giving a free research tool to mathematicians would likely be better received, and receive better press, than doing something that most top-tier mathematicians are opposed to.
My hypothetical "AlphaMath" certainly could just be free GPT-N access for academics/researchers (as they are also doing to some extent), or it could indeed be a custom system that OpenAI built as a gift to the math community.
As far as the AI companies acting in slimy fashion goes, the most slimy behavior of all is to strongly believe you are doing something that will kill people and cause massive societal disruption ... and still keep doing it.
>I suppose you are suggesting that research mathematicians are either over-qualified mathematically and/or under-qualified in ability to teach, but it seems pretty clear that universities prefer to hire domain experts whose reputations and long publication lists attract students and raise the perceived academic standards of the school.
I'm saying there's little correlation in how brilliant a researcher you are and your teaching abilities. Yes universities optimize for the former. That's not necessarily a good thing for students even if it increases the prestige for the university. If there's some future where research and teaching are decoupled, I don't expect things to remain the same, but who knows I guess.
>I was pointing out that giving a free research tool to mathematicians would likely be better received, and receive better press, than doing something that most top-tier mathematicians are opposed to.
At least currently, it's not possible for this to be a free tool. Both OpenAI and Anthropic have discounts for Universities/Education for such use cases as far as I'm aware.
>As far as the AI companies acting in slimy fashion goes, the most slimy behavior of all is to strongly believe you are doing something that will kill people and cause massive societal disruption ... and still keep doing it.
This is pretty bad, but I wouldn't call it slimy. And it's no longer up to any one person or company anymore.
Nah the AI won't replace coders or mathematicians until it can maintain codebases/knowledge long term.
I actually don't think that current AI can replace any profession that requires human interaction over many weeks. This is because imo they lack long term planning abilities
>Nah the AI won't replace coders or mathematicians until it can maintain codebases/knowledge long term.
Okay...you understand that are training for this and it has gotten much much better at doing this over the years ? You should probably also understand that it doesn't need to be able to do this to cull the profession ?
Yeah I use Astra Light at work. It's great but it probably cannot work on a project longer than a week without introducing architectural blunders
I also think they overestimate how much of most jobs can be done by an LLM (a text generator!), and how much importance and reliance most companies put into soft skills, and non-linguistic understanding/feels, both during interviewing (are they Googley-enough?) and afterwards.
For example, how do you reconcile return-to-work mandates with the idea that companies are going to be happy with faceless remote workers? What does the boss do when the shit hits the fan and he would have yelled at people about the need to work all weekend, but instead all he has to yell at is an LLM that tells him he's "right to push back", that it promises not to delete the production database next time (except it will, because it can't learn), and that it could care less about being fired because it's just a calculator?
Yeah. Not to mention the paper-clip maximizing that RL induces in them. I had 5.6-Luna use a parser combinator lib in order to find out that it imported it but wrote its own parser, so it technically followed my instructions.
Imagine that paper-clip maximizing happening over millions of tasks.
I think we are just entering the LLM + Human era.
In a related vein, not too long ago I asked Sonnet how many states and non-terminals were in an a YACC parser for ANSI C, something that could easily be googled for, but it instead chose to go off and downloaded and build bison from source, downloaded a grammar, built the parser ... but then failed to give the answer since I'd hit my daily free limit.
Got to admire the gung-ho approach I suppose ?
It's possible that Clay Mathematics Institute will not award the prize at all. The spirit of the rules seems to be that the result can be attributed clearly to one or more individual mathematicians. If the attribution remains unclear (maybe because the main contributions were made by AI), the rules include an option for not awarding the prize at all.
Wouldn't the proof be attributed to the people who operated the AI? After all, it took more than writing a "prove the navier Stokes Clay problem" prompt.
> After all, it took more than writing a "prove the navier Stokes Clay problem" prompt.
Yes, but it took far less than using your meat brain to prove the Navier-Stokes Clay problem.
It will be tough to draw the line, as the meat brains trying to prove it were also using AI.
I assume that the mathematicians outside Anthropic were hoping to publish an actual human-understandable paper. That could be one way to draw line: you can use AI, but you must also have an intelligible explanation at the end.
I am utterly fascinated by the amount of comments here from engineers that clearly have zero experience with mathematics making utter fool of themselves by claiming to know better than mathematicians what their jargon is/means, how publishing works/should work, etc…
I try not to go down the route of “hn was better before!” but… jeez, do better, people. What happened to this community, there used to be some effort to not be bottom-barrel like this.
What did you expect? Degree of BS increases together with the population.
Put simply, I expected better, friend.
Gell-Mann Amnesia HN version?
For this I'd need to be any good at mathematics.
What I'm not seeing reported on much is if the result reveals any new techniques or ideas that advance mathematics - which is what we usually hear is the reason to work on these problems. Or does the resolution of NS just add a fact to the list without any new understanding.
My understanding is that it’s proof by counterexample, so the main thing to study would be the implications of the counterexample. The technique used to find it sounds like a lot of brute force. But I’m not a mathematician, and maybe the AI used some clever techniques to narrow in on it.
The two-year publication rule is the interesting part. OpenAI doesn't need the million, and the community will judge the result regardless of whether Clay ever accepts it.
Clay will award the prize (or choose to not award it) when there is an expert consensus that the problem has been solved and the solution is correct. The rules merely state what that would mean in some typical cases. There is always an option that Clay changes the rules to match the reality better.
The result was never the point.
Clearly the real-world cannot "blow-up" - real-world water vortices do not reach infinite velocity, etc.
The point of having Navier-Stokes as a Millennium prize was to hopefully generate new mathematics and techniques along the way, and auto-generating a sprawling AI-slop proof or millions of lines of Lean does not accomplish that result.
Clearly OpenAI has no interest in the math itself - to them this was just a trophy animal to shoot and stuff. I would be very surprised if they now helped analyze the proof and try to extract the mathematical value out of it, and this would obviously require outside help who are probably not inclined to help OpenAI math-wash their behavior.
Right, the real world doesn’t blow up. So if N-S does then it means in some situations it doesn’t model the real world well. That’s important because if we can understand those situations we can avoid erroneously relying on it.
Did anyone ever think that N-S was a perfect model?
Are there still any reasonable arguments to be mad at OpenAI at this point? Looking at how everything unfolded, this seems to have hit them way harder then they deserved.
They said they started working on millennium problems after hearing a rumor someone had found a solution to one of them. That's just bad taste. It indicates negative motivation rather than positive motivation from the start.
Not someone. Their single competitor. During a time when they were validating their newest internal model. What would you have done?
Truly, if this is the biggest criticism left, they should be celebrated. While in reality, all of this has a bitter aftertaste.
So weird.
That is not the narrative given in the OpenAI announcement. They claim to have started working on it after "we heard rumors that two Millennium Prize problems had been resolved", on September 1st, that "we later realized was related to Levent Alpöge" on Sepetember 6th "After the completion of our full project and lean verification"
That does stretch the reader's credulity. I think most people find it far more likely the rumor was related to Anthropic all along.
[dead]
TL;DR:
- "yeah we know"
- "looking into it"
- "will ping you"
- "might take a while though"
+ preemptive linguistic cushioning in case they feel socially (politically) compelled enough to forbid clanker proofs in their solution acceptance criteria, or in case they decide against conceding to such pressuring
[dead]
It feels like a nice post. It’s almost like we’re not supposed to celebrate the fact that mathematics is accelerating.
Wait, I thought the provenance of the proof is still disputed? There's a mathematician in NY saying he used OpenAI to develop his Navier-Stokes ideas. And OpenAI's proof is suspiciously similar.
At this point, how can we tell whether AI is improving or it's just reappropriating its users work? It's probably a bit of both. But still, thick milky.
Buckmaster (the mathematician) and Alpöge used and credit AI substantially for their proof. Even if OpenAI did copy their ideas, it still wouldn't show that this didn't come from AI improving.
OpenAI's proof is substantially different and I don't think anyone has claimed otherwise. The accusation is that they used the same avenue of attack, and it's an uncommon one, and that makes it suspicious that they may have taken the idea.
There are several cases of this already. Bubeck himself had to retract earlier claims of novelty, and more recently, the provenance of the non-sofic group result was brought into question. Most recently, it turn out that the construction used for Anthropic's counterexample to the Jacobian Conjecture had appeared in an unpublished but publically available draft: https://news.ycombinator.com/item?id=49657499
This has a few practical implications: First of all, if you are in the target group of the marketing material, be wary. While these things can do non-trivial stuff, the amount of magic is being grossly over-stated. But also, when several of the big results have indeed been reappropriating the work of others; when the companies fail to provide proper attribution (the NS case in particular is laughable) and present the results as the models' own work, that's plagiarism.
I agree. I found it refreshing to get away from all of the AI drama and just enjoy the advancement in math.
We should enjoy the advancement. I also think the AI companies solving this or such problems with rewards shouldn't get any cash - that's the least they can do for human advancement having stolen the entirety of human knowledge and continuing to swallow never before seen amount of energy.
FWIW I think OpenAI have stated they will not claim the award.
They did not do it for the money obviously, but for the PR, that much everyone must agree on.
> They did not do it for the money obviously, but for the PR
Doing it for the PR is still just doing it for the money, only they have a much bigger pile in mind.
Agree! 'Problems' are getting solved and this needs to be celebrated. Wondering how this will discourage mathematicians at all, since now they have another tool to accelerate their research. Nothing is stopping them from using 'new technologies' or sticking a gun to their head to use the 'new technologies' either.
If you consider this event in isolation it is cause for celebration. But the controversy around this isn't so much about how the proof was obtained but what this means for the practice of mathematics going forward. It seems we can probably expect more and more results of this nature being dumped into the community. It's happened before that one person, Bill Thurston, was so successful in his field, proving theorem after theorem, that he inadvertently killed his field. People hesitated to enter his field, knowing that they could be scooped at any moment. It took years before his field recovered - and I think his famous essay was written in response to this.
https://arxiv.org/abs/math/9404236
You mean that every mathematician can assign ten thousands Astra bots and 20 million dollars in compute to their thesis problems now?
If it works (something they need to be convinced about), if it accelerate mathematics and solve complex problems for humanity, then why not?
Aren't they already using computers, mobiles, calculators, etc. already?
Yes, but a big part of the problem right now is that two big labs have monopoly on the resources and they for sure are not working for the benefit of mankind.
The Startrek future is still a long way out.
The Star Trek future may be right on schedule.
https://memory-alpha.fandom.com/wiki/World_War_III
> some 30% of the Human population, at least six hundred million people
The math nerd in me has to point out that this means there was only 2 billion humans for 30% to be 600 million (though it does say at least). Currently we have 8 billion humans on this planet or so. There must have been a culling before WWIII in their universe that they failed to mention.
>The war was preceded by the Eugenics Wars and the Second Civil War
Earl Grey, hot.-
In December 2024 o3 scored 87.5% on ARC-AGI-1 and cost $4560 per task.
DeepSeek V4 Flash 0731 scores 89% and costs $0.02 per task.
If we apply the same factor to the guesstimated API price of $20M for this problem, we arrive at $57.
Real cost is a fraction of the API price. Although the internal model might have a higher API price than the ~$19.5M I estimated based on Astra's pricing.
> Wondering how this will discourage mathematicians at all, since now they have another tool to accelerate their research.
I'm a professional mathematician and these tools are not available for me. So not happy about that!
(just to be clear, I'm not anti AI, I'm just criticising the shallowness of your comment)