301–310 of 1000 posts
The GitHub repo with the Lean formalizations just came out a couple of hours ago: https://github.com/openai/ten-proofs It also links to a paper written by an LLM where the model "reconstructs how the proof came together" based on the unpublished reasoning traces: https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf I wish they'd publish the prompts though!
Earlier quoted context omitted.
> people that can't psychologically cope with the advances of AI Yes. And there are many of them. I wonder what would help them come to terms with it. Seriously, people are going to be grieving over this. Loss of identity, loss of social standing, ideas of entire future lives that will now never happen. The greatest crime people may hold AI guilty of is taking away their dreams.
People have had to deal with getting their jobs automated away for centuries. None of this is new, and perhaps reminding ourselves of this is the best way to cope.
Earlier quoted context omitted.
If the proofs are formally verified by a proof assistant (Agda, Roq, Lean, ⋯), I see no reason we would need to know how these came about. All the information needed is in the proof.
Unfortunately, we seem to already have an example of an LLM producing a proof in a week known open problem (the Collatz conjecture) in which it looks like it was sneaking a flawed proof through bugs in the proof checker. https://infosec.exchange/@0xabad1dea/117002106099986943
Another case I want to highlight is writing GPU kernels as illustrated by the following example: Say I want to generate random number with Normal (0, 1) distribution. Often times the AI written kernel will just generate the number 0. The tests often fail to catch these errors.
Earlier quoted context omitted.
Grad students on zero pay solve problems like this everyday. What exactly is your point here?
Zero pay? These would be PhD candidates; surely they have a stipend?
Earlier quoted context omitted.
Prompt quality should not matter. If a high-schooler operates the crane to lift a ton of weight 10 floors high, should the credit entirely go to the crane?
When I type 56789*23456 into my calculator and get the result I don't claim to have solved the problem, the calculator did it.
Not being an expert in any of the fields OpenAI has "advanced" I don't want to prematurely downplay the significance of this contribution. However, I am worried that the language they are using in this blog post is exaggerating for the sake of marketing. It is true there hasn't been a reliable computational approach to solving these problems before. But do these proofs contribute new ideas to the mathematical corpus,…
"Breakthrough research" can be defined (in the citation record) as research that both (1) becomes highly cited, and (2) brings together citation chains that were previously not showing up together. Mundane incremental research is cobbled from existing citations that already appear nearby in the record. Basically, innovative research is a measure of bridging thought and domains that were previously not bridged. It's q…
Not being an expert in any of the fields OpenAI has "advanced" I don't want to prematurely downplay the significance of this contribution. However, I am worried that the language they are using in this blog post is exaggerating for the sake of marketing. It is true there hasn't been a reliable computational approach to solving these problems before. But do these proofs contribute new ideas to the mathematical corpus,…
The problems from CS (CVP and circuit complexity) are very important problems that have been worked on by top researchers for 30-40 years. Some of these researchers include Turing Award winners. A solution to them would be a best-paper award at many top CS conferences.
But the wording of the result makes it sound like we don't know what the lowest possible complexity bound might be. So, prior to this result did we think there couldn't be a lower possible bound? Or did the arithmetic circuit community think there were lower possible bounds but didn't see it as a high value target for experts to tackle (maybe a problem that was instead regularly given to students to study).
Not being an expert in any of the fields OpenAI has "advanced" I don't want to prematurely downplay the significance of this contribution. However, I am worried that the language they are using in this blog post is exaggerating for the sake of marketing. It is true there hasn't been a reliable computational approach to solving these problems before. But do these proofs contribute new ideas to the mathematical corpus,…
> However, I am worried that the language they are using in this blog post is exaggerating for the sake of marketing Your worry.... is because they used the word advanced? For marketing? The word is used very appropriately here. There were PhD's who spent a big part of their career tackling these problems.
I'm trying to understand if these specific problems were the kinds of problems that would have justified an expert investing weeks or months to solve. Or if they were the kinds of problems that would normally have been given to students to investigate.
In a way the most remarkable thing about this is that it isn't even at the top of the HN homepage. Even if this is a step up from what we've seen before, we're no longer astonished by the idea that AI can make significant advances in mathematics and computer science.
This is not at the top as it is actively flagged by people that can't psychologically cope with the advances of AI. Hacker News is no longer a web site of an elite.
Is that possible or is everyone else too common to have those?