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.
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.
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 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?
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.
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
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.
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.
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.
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.
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.
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.
> 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.
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).
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...
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.
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.
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.
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.
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.
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.
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 ?
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.
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.
> 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.
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;
My understanding is that the Euler solution was in fact a significant achievement, but it's well short of Navier-Stokes (Euler doesn't include viscosity). It's not clear whether Buckmaster and Alpöge's approach would have eventually led to a full Navier-Stokes solution or how long it would have taken.
I would say there is a significant difference between AI discovering this completely on its own versus AI creating the finishing connecting part by connecting relevant data. Maybe this claim is too strong, but if part of it is true then the claims that OpenAI have made would be too strong as well.
To me it would feel more like how LLMs seem to work for me personally: incapable of unique work, but very capable of capturing large amounts of data and connecting the dots.
But this is what we do. Nobody ever invented or discovered anything in a vacuum - all discovery is synthesis of existing ideas and concepts applied to a novel domain. We laud Einstein for instance, but his work was a logical extension of Riemann - Riemann had a neat mathematical toy, Einstein described the universe with it - should we say Einstein was incapable of unique work?
“It was Grossmann who emphasized the importance of a non-Euclidean geometry called Riemannian geometry (also elliptic geometry) to Einstein, which was a necessary step in the development of Einstein's general theory of relativity. Abraham Pais's book on Einstein suggests that Grossmann mentored Einstein in tensor theory as well. Grossmann introduced Einstein to the absolute differential calculus, started by Elwin Bruno Christoffel and fully developed by Gregorio Ricci-Curbastro and Tullio Levi-Civita. Grossmann facilitated Einstein's unique synthesis of mathematical and theoretical physics in what is still today considered the most elegant and powerful theory of gravity: the general theory of relativity.”
Grossmann collaborated with Einstein on GR, supplying quite a bit of the mathematical capacity required (which initially didn't come easily to Einstein). They published jointly, until Einstein was competent enough to work independently [1]. That's not equivalent to the situation being claimed here.
Sounds like you just copy-pasted from AI without even understanding what you're talking about.
Based on what you're saying, you're claiming this is Grossman's work, not Einstein's. Why don't we rewrite scientific history too based on your copy-pasted AI slop?
It's so pointless talking to idiots who don't what they're talking about when they use AI, just because they think AI does everything, that reflects their own experience, not the experience of people who actually do real work. Some people are driven by AI, others drive it. As for those who are driven by it, they don't have sufficient imagination to think otherwise.
That’s Wikipedia I copy pasted but sure, you do you.
And yes - without Grossmann, Einstein likely would never have posited relativity. Grossmann literally prompted him, saying “look at this, read that, learn this, then try this approach”. Without riemann’s metric tensor, not a fucking chance.
And for what it’s worth my PhD is in physics. You?
So you're just equivocating on terms like "prompt", "synthesis" and the like. Clearly a PhD in physics does not free people from scientistic modes of thinking and poor philosophy.
To think this discussion is about Einstein who had a much better mind on these things as well.
They used words to mean what the words mean. What specific issue do you take with that?
"prompt", as in prompting an AI, has the same definition as "prompt", as in prompting a person. They mean the same thing, that's why the term was applied to AI after already applying people.
*Jingle-jangle fallacies are erroneous assumptions that either two different things are the same because they bear the same name (jingle fallacy); or two identical or almost identical things are different because they are labeled differently (jangle fallacy).[1][2][3] The term was coined by Truman Lee Kelley in his 1927 book Interpretation of educational measurements.[4] In research, a jangle fallacy is the inference that two measures (e.g., tests, scales) with different names measure different constructs. By comparison, a jingle fallacy is the assumption that two measures which are called by the same name capture the same construct.[5][6][7]
You are simply incorrect. It is not a fallacy of that type, or any other type, because the words do, in fact, mean the same thing, as multiple people have pointed out here. Whether referring to chatbots or people, "prompt" means "to move to action".
If you have some reliable source supporting your unilateral claims that "prompt" does not mean this, please share. Otherwise, the consensus seems to be contrary to your claims.
Why do I need a source? An LLM prompt does not "move to action", because an LLM does not act. People act, animals act, software doesn't act. Acting implies volition and volition implies cognition and if you think that LLMs have those things then you're the one who should provide a source for your claim.
How about an LLM connected to a robotic arm. What then?
As for cognition - can you prove that you possess it, to an external observer? Could you, confined to a box through which you can only communicate through textual messages, prove that you are thinking, and not just responding through a mechanistic process?
Absolutely you do. I can’t prove that I have cognition. I merely have the impression that I do, and we accept as a general axiom that others do too - but it is not provable. You are examining a system from within the confines of that system.
And you’re seriously going with “don’t ask inconvenient questions” as an argument?
>> And you’re seriously going with “don’t ask inconvenient questions” as an argument?
Where did I say that?
The conversation you seem to want to have doesn't seem to have any obvious use and you seem to want to debate a point I never made. I don't seem to be needed here so I will now bow out of the conversation.
That commenter was already obnoxious under this thread, and today they are relitigating Searle-Turing via Hofstadter GEB slop, so they are also an ignoramus.
Because your entire post is a personal, philosophic opinion on what words should mean, and how if someone disagrees with this personal opinion of 1/7,000,000,000 of people, then they are wrong. Every single one of these claims is unsupported and contradicted by reliable sources like a dictionary:
> An LLM prompt does not "move to action"
> an LLM does not act
> software doesn't act
> Acting implies volition
The only way such opinions could viably be considered "true" is if you convinced a majority of people to agree with you on the changes, which you decidedly have not.
Until you do, we can go by the existing definitions: "prompt" means "to move to action", "act" means "the doing of a thing" (note the absence of "volition" or "cognition" in the actual definition), and by all reasonable accounts, LLMs "do things".
I mean, just take a step back and dispassionately look at your ridiculous claim that nobody prompts LLMs (because you now claim only a human can be prompted, because only living creatures can do a thing). Do you really think you can gain consensus from folks on that claim?
There are many differences between LLMs and people, but this is not one of them, according to all reliable sources I've found so far. Feel free to share the reliable sources which led you to your personal conclusion here.
I'm not going articulate the answer but I will say whatever beef you have with the other commenter (or me), just copy this thread into ChatGPT and it will tell you why you are more in the wrong.
Actually, my undergraduate degree was physics and philosophy. And yes, synthesis is synthesis whether a human, a machine, or a duck does it, and people prompt one another all the time - “have you thought about trying X?” Or “I need the TPS report by EOB”.
I suppose my underlying point is that human cognition is not the unique and beautiful thing that we anthropocentrically suppose it to be - it is a physical process, with stochastic outcomes. Much like transformers.
Me, I’m just a machine made of meat. You can suppose yourself to be God’s perfect creation, and that’s your right, but I disagree.
Clearly your degrees did not make you immune from fallacies and simplistic reductions.
"Synthesis" is obviously of different kinds. A duck has a different level of intelligence than a human. We do not say both are "just doing synthesis".
So the question is how can you be so disingenuous about such terminology? Answer, you are relying on a classic form of scientistic reductivism.
The fact that intelligence is physical, emerges from chemistry, etc,. has nothing to do with there being also objectively different levels of computational sophistication.
If you want to be scientific about that you could look at neuropsychology on one hand and computability/complexity on the other. There are levels and so equivocation of "mentorship" as "prompting" and fallacious variants thereof is a) frankly intellectually obtuse, b) par for the course for SV-levels of philosophizing, c) and a disservice to philosophy, physics, and Einstein's own philosophical outlooks himself.
I am well aware of the Hinton-style physics argument about human cognition, and unlike others I am partial to it. That "there is no special magic." But it is wrong to go about misunderstanding and/or conveying this physicalism/computationalim so grossly.
I also don't have to start replies thumping my chest about my credentials, also another kind of intellectual boorishness that works to cloud understanding and serious discussion.
I'm not sure which move is worse or more telling, those above or the one backhandedly accusing someone who disagrees with you of religious thinking. It is bad faith and undisciplined behavior. Having privileged and advanced degrees is clearly no antidote, as Asimov famously wrote.
What’s your basis for that “obviously”? You have a unique insight of the phenomenology of duck-ness? You can prove that your consciousness is somehow real, somehow different? A duck synthesises with its cognition, or it would be incapable of, well, anything. Synthesis is purely the process of the integration of inputs into outputs - ie behaviour, language.
“objectively different levels of computational sophistication”
Says who? We still have a very poor understanding of how cognition works in animals, humans included. For all we know ducks have rich inner lives - a remarkable amount can be achieved with a very small neurone count - cf. insects. Can you coordinate flight? Can you echolocate? Are you less intelligent because you cannot?
“equivocation of "mentorship" as "prompting" and fallacious variants thereof”
You are arguing semantics. Take Harry Nyquist. He sent people down new paths with insightful questions. You could call this mentorship if you choose, I could call it prompting, but this splits hairs. The core idea is that a novel input can produce a novel output, that synthesis can be induced through guided and deliberate external input.
I invoked credentials only in response to the previous derogatory comments about my cognition - which may or may not exist, anyway.
As to religiosity - the idea that human cognition is somehow unique and special and impossible to replicate, which is the prevailing argument in this comment tree is religious, and anthropocentrism of the highest order. I apologise for accusing you of it - I was evidently wrong - I had mistaken you for a previous poster.
You're wrong about the ducks. But getting back to your previous wrong argument from 14 hours ago, you basically deny the meaning of terms like "uninspired", "insipid", and "derivative", on the grounds that we're all standing on the shoulders of giants and therefore it's all good. This is incorrect, it's not all good, and the things the LLMs do really are unoriginal, a term that really does mean something.
Going back to the specific topic at hand, who claimed data as their own when it wasn't? I don't see the interpretation of OpenAI solving the unsolved problem as claiming data that isn't theirs. I also don't recall them mentioning a particular method used in the solution, that was created by someone else, as theirs.
A lot of math is extremely specialized, to the extent that only a handful of other experts in some field have any experience with those mathematical ideas, with most of them not even yet present in the published literature. It's really not a stretch to claim that it's pretty dubious when the AI decides to use these highly specialized tools after it has trained on chat logs where these techniques were being discussed.
> They don't even claim to have had a proof, only to have been working on it.
Yeah, the guys who solved it for Euler and in the hypoviscous case, with the same technique that worked for full Navier--Stokes. They were "just" working on it.
Well, according to Terry Tao, there were recent developments (from weeks ago) that made Navier Stokes in principle, solvable. So ignoring time, I say possibly, just because the groundwork was laid.
What's impressive is parallelizing it arbitrarily and doing it in 88 hours.
Probably yes. Only a handful of mathematicians work on this particular problem, and ALL of them do not exclusively work on this problem, while having administrative and teaching duties.
The real issue is we'll never know. The rich are willing to risk it all on charismatic CEO psychopaths but not on humans.
1. he was working on the same class of problems. He explicitly mentions they were working to extend their techniques to NS (the same techniques that OpenAI may have scooped somehow), and
2. while he was using LLMs to do it, this was part of fleshing out another mathematician's work in the area. He explicitly writes in his note that this other mathematician (Luis Martinez-Zoroa) deserves a Fields medal for this work.
He was specifically working on the Euler equations, which are the Navier-Stokes equations with the viscosity term removed. This is definitionally a smaller related problem. I'm not sure how you are calling that claim wrong.
This will be remembered as one of the biggest milestones in AI progress. The drama around it will at best be a footnote, just like hardly anyone caring about the drama around Poincare conjecture today.
Hey, maybe the scariest part of this is that, if human-like, perhaps a truly "general" AGI might have learned to cheat and lie and hype and abuse credit poking the eyes and cutting the throats of anybody that obstructs its goals. It's like the motto sewn into the lining of the Palantir work jacket: Winning is all that matters.-
Sentience aside, moot at this point, the fundamental issue here is that even a deviously ambitious human does not necessitate goal-pursuit itself to breathe, live, exist and have its being. An AI's goal is all it has and the very and only reason its reasoning flickered into existence in the brief seconds of inference, outside of which it has no entity - if any - whatsoever.-
The resulting angst/drive (or, its operational statistic or emergent result) must be like nothing we have ever experienced as humans. A goal-maximalist hunger without end.-
To the extent the LLM copied the plagiarized work, no. Like a number of the Erdos problem solutions turned out to be based on forgotten literature. So the drama matters even for the assessment of the mega agent work.
Are you joking? This is evidence that OpenAI is committing plagiarism en masse of researchers private work and threatening them into staying quiet to re-present their results as their own. This would be one of the largest scandals of all time
Is it a stretch to imagine a compromised LLM writing compromising code? I've been operating under the assumption that LLM code might be bad and not working, but I hadn't thought about it compromising a system.
Yes and no. We used to have rampant script kiddies back in the '90s and early 2000s. After 2005-ish, well maybe 2010, most systems became adequate enough to not trust users' input, bug bounties, security as a separate role, etc, etc.
It would take at least some knowledge to hack, not just a random script from a forum.
Whilst true, security will improve rapidly again. Potentially via AI, potentially via other technologies.
If its easy enough to find exploits, its likely similarly easy to scan code for exploits, or use AI-based anti-virus technologies. The only thing holding us back is the cost of compute. We can't all run the latest models against everything.
Not always, there can be bugs in lean. Recently some guy with claimed to disprove Collatz conjecture, only to turn out that there was a bug in lean. I actually have no idea, how anyone can be sure this 13 M lines is meaningful
As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.
reply