logoalt Hacker News

jrfloyesterday at 5:47 PM4 repliesview on HN

I'm so tired of this "It's just marketing!!" commentary. An AI model just proved one of the top 3 unsolved problems in mathematics, they have a Lean certificate showing it's valid. How much more evidence do you need that these models are actually highly capable?


Replies

mrbungieyesterday at 5:58 PM

They are highly capable, no doubt about that, but:

1) We don't really know how they arrived to this result except that they had a lead and that they threw millions of compute at the problem. The article is written in a way that makes you believe that it was just an agent loop with little human intervention, but without any evidence.

2) If the threats are to be believed, it is concerning how far they are willing to go to show how capable the model is. One would think their products and credibility would be enough to speak for themselves.

show 2 replies
danielmarkbruceyesterday at 9:13 PM

Highly capable of writing math proofs, no doubt.

It's really unclear that this entire line of work (training LLMs for proof writing) has much real value outside of writing math proofs. It is reasonably clear that, similar to Deep Blue at the time, people are extrapolating the results to general intelligence because the people who usually write proofs are insanely smart (just like world class chess players).

QuesnayJryesterday at 5:57 PM

Of the seven Millenium problems, Navier-Stokes was the one most thought to be in reach.

I'm not sure what the top 3 problems are. You can make a case for the Riemann Hypothesis and P != NP, but I'm not sure what #3 would be. Maybe the Langlands program? (That one is not as precisely stated as the other two.)

show 2 replies
andrepdyesterday at 7:18 PM

Lmao my friend, the whole "drama" is that there are allegations of plagiarism.