181–190 of 292 posts
Earlier quoted context omitted.
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 co…
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 w…
Earlier quoted context omitted.
Completely misleading. 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 fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_o…
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…
Earlier quoted context omitted.
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.
Even funnier that it wouldn't even be the first time that happens: https://en.wikipedia.org/wiki/Grigori_Perelman
OpenAI the opposite.
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.
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 itse…
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…
Earlier quoted context omitted.
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.
Earlier quoted context omitted.
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.
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.
Earlier quoted context omitted.
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 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?
Proving things without comprehending them is a threat to intellectual work.