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.
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 ...
> 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.
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.
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.
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.
> 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.
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.
> 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.
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 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.
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).
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 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.
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.
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.
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 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'
> 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.
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.
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.
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.
As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.
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.
Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.
I guess these little questions are what this article is really about.
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?".
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.
Huh? We're about six decades past that moment.
A similar rule existed for the 100-year Wolfskehl prize established in 1906 for solving Fermat's last theorem; two years after publication.
This is all you need to read and understand for Anthropic's FLT formalization:
The actual proof is 13 million lines of Lean.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.
Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.
It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.
Humans need to verify everything.
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.
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.
https://github.com/leanprover/lean4/issues/14576
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.
The statement is so sterile they don't even mention who solved it. The word "OpenAI" doesn't appear at all.
Possibly because of the ongoing debate about who actually deserves credit.
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.
Keyword: New Technologies
That “apparently” feels load-bearing
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.
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
You interrogate a proof.
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).
This brings nothing but shame for OpenAI.
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
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”
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.
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 might be difficult or impossible…
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.
The prize was offered to him in 2010, after multiple others had digested his work and published elsewhere.
Looks like even a blog post is good enough, they just need to do the review by themselves.
[0] https://web.archive.org/web/20000622023328/http://www.clayma...
> 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.
Yes, but it took far less than using your meat brain to prove the Navier-Stokes Clay problem.
OpenAI and Anthropic might have 3 millennium problems by December
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.
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.
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.
Currently 0/2 Millenium problem solvers claimed the prize money so clearly money is not their motivation for tackling the problem.
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".
...
>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.
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.
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.
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.
They did not do it for the money obviously, but for the PR, that much everyone must agree on.
https://arxiv.org/abs/math/9404236
Aren't they already using computers, mobiles, calculators, etc. already?
The Startrek future is still a long way out.
https://memory-alpha.fandom.com/wiki/World_War_III
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.
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.